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
|
|
|
|
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 |
|
|