Foundations of Modern Type Systems

Auxiliary readings

• Lambda Calculi With Types, by Barendregt

Links

• Typeful Programming, by Cardelli
• Phase Distinction in Type Theory, by Cardelli

• Cayenne - A language with dependent types, by Augustsson
• An exercise in dependent types: A well-typed interpreter, by Augustsson

• An algorithm for type-checking dependent types, by Coquand

• Facilitating Program Verification with Dependent Types, by Xi (overview)
• Dependent Types in Practical Programming, by Xi (PhD Thesis)
• Dependent Types in Practical Programming, by Xi (article)
• Some Practical Aspects of  Dependent Datatypes, by Xi
• Imperative Programming with Dependent Types, by Xi
• Towards Array Bound Check Elimination in Java Virtual Machine Language, by Xi
• A Dependently Typed Assembly Language, by Xi

Home pages

• Lennart Augustsson
• Thierry Coquand
• Hongwei Xi