Date 
Topic 
Notes 
Homework

9/9

What are
dependent types?



9/14
and
9/16
and
9/21

A
polymorphic
lambdacalculus 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 MishraLinger 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




11/4

Ur: StaticallyTyped
Metaprogramming with TypeLevel 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
DomainSpecific 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 LowLevel 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 FirstClass 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 

