Foundations of Modern Type Systems
G22.3033.10 Spring 2000
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
[Last change: 03/08/2000]