Advanced Topics in Programming Languages:
Dependent Type Systems

CIS 670
University of Pennsylvania

Fall 2010


Location: Moore 212
Time: TR 1:30-3:00 PM
Instructor: Stephanie Weirich
Prerequisites: CIS 500 (Software foundations) or permission of the instructor


Dependent type systems blend programming and program verification. At their simplest, they permit lightweight program verification through a form of compile-time computation. Despite their attraction in modern programming languages, the metatheory of various forms of dependently-typed programming languages is not straightforward. Furthermore, is also not clear what limitations of expressiveness occur with various changes to the language design. We will study these two topics in parallel, discussing both the formalization and expressiveness of several variants of dependent type systems throughout the semester.

The course material will be based on classic research papers and new research results. Grades will be based on semester-long group projects as well as course participation. Although this course has the same title and topic as the Spring 09 version, the content will be substantially different.


Date Topic Notes Homework
9/9
What are dependent types?


9/14
and
9/16
and
9/21
A polymorphic lambda-calculus with Type:Type.Luca Cardelli. SRC Research Report 10, Digital Equipment Corporation Systems Research Center, May 1, 1986.
Type system overview. Encodings. Erasure. Type soundness.

Can you encode dependent if?
Can you finish the alternate encoding of  the equality type?
9/23
David Baelde


9/28*
ICFP


9/30*
ICFP


10/5
 The Implicit Calculus of Constructions as a Programming Language with Dependent Types. Bruno Barras and Bruno Bernardo. (also, Erasure and Polymorphism in Pure Type Systems. Nathan Mishra-Linger and Tim Sheard.)
Is there a formal correspondence between these two systems?
10/7
Singleton types here, singleton types there, singleton types everywhere
Stefan Monnier and David Haguenauer


10/12*
Fall Break


10/14
More Singleton Types

Can you translate Cardelli's language into SHE/Haskell?
10/19
A Formulation of Dependent ML with Explicit Equality Proofs. Dan Licata and Robert Harper.
What does the phase distinction really mean?
10/21 and 10/26
Consistency of CC by CC
A short and flexible proof of Strong Normalization for the Calculus of Constructions. Herman Guevers


10/28
Dependent Types in Practical Programming. Hongwei Xi. (DML homepage).


11/2
Semantic Subtyping with an SMT Solver. Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, and David Langworthy


11/4
Ur: Statically-Typed Metaprogramming with Type-Level Record Computation. Adam Chlipala

11/9
Observational Equality, Now! Thorsten Altenkirch, Conor McBride and Wouter Swierstra
Vilhelm

11/11
Scrapping your Inefficient Engine: using Partial Evaluation to Improve Domain-Specific Language Implementation, Edwin Brady and Kevin Hammond Brent

11/16

PiSigma: Dependent Types Without the Sugar. Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh and Nicolas Oury
Loris

11/18
Liquid Types Patrick Rondon, Ming Kawaguchi and Ranjit Jhala Jianzhao

11/23
Dependent Types for Low-Level Programming. Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George Necula. Ben

11/25*
Thanksgiving


11/30
Verified Programming in Guru. Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, and Timothy Simpson. Daniel

12/2
Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic . Kenneth Knowles, Aaron Tomb, Jessica Gronski, Stephen N. Freund, Cormac Flanagan Michael

12/7
Dynamic Typing with Dependent Types Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker Peter Michael

12/9
Trellys core language

*indicates dates when class will not be held