Making programming with dependent types practical through better tools

EDIC candidacy exam
Exam president: Prof. Arjen Lenstra
Thesis advisor: Prof. Martin Odersky
Co-examiner: Prof. Viktor Kuncak

Abstract
Traditionally, programming languages with more powerful type systems have been considered less user-friendly, as using them require developers to familiarize themselves with many non-intuitive concepts. In this report we survey
dependently- typed languages, a particularly advanced category of languages.
We show the practical benefits that dependent types bring, the trade-offs associated with them, and the powerful interactive programming experience they enable. Finally, we discuss how these systems can serve as a source of inspiration for our work on Scala, guiding us to improve both the static guarantees and user experience of the language

Background papers
Why Dependent Types Matter, by Thorsten Altenkirch, Conor McBridge and James McKinna
A Tool for Automated Theorem Proving in Agda, by Fredrik Lindblad and Marcin Benke
Elaborator Reflection: Extending Idris in Idris, by David Christiansen and Edwin Brady