Systems
Dependent Types
"Dependent types are useful not only because they help you express correctness properties in types. Dependent types also often let you write certified programs without writing anything that looks like a proof. Even with subset types, which for many contexts can be used to express any relevant property with enough acrobatics, the human driving the proof assistant usually has to build some proofs explicitly. Writing formal proofs is hard, so we want to avoid it as far as possible. Dependent types are invaluable for this purpose."
Books
- Types and Programming Languages aka TaPL (2002) by Benjamin C. Pierce (Goodreads)
- Advanced Topics in Types and Programming Languages aka ATTaPL (2004) by Benjamin C. Pierce et al. (Goodreads)
- Software Foundations (2011+) by Benjamin C. Pierce et al. (Goodreads)
- Practical Foundations for Programming Languages aka PFPL (2nd Ed; 2016) by Robert Harper (Goodreads)
- Programming Languages: Application and Interpretation aka PLAI (2nd Ed) by Shriram Krishnamurthi (Goodreads, Wikipedia)
Readings
- Basic Simple Type Theory (1997) by Hindley