Advanced Topics in Programming Languages:
Dependent Type Systems

CIS 670-301
University of Pennsylvania

Spring 2009


Location: Towne 303
Time: MW 12:00-1:30 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.


Date Topic Notes Homework
1/14
Introduction
Dependent Types in Haskell
via "Phantom Types"
Haskell examples
Hinze, Fun with Phantom Types (Sections 1-3,7)
"Haskell" higher-order polymorphism
Fun with Phantom Types
#3 & #17
1/19 & 1/21*
no class
MLK day and POPL

1/26
Kindless higher-order polymorphism & BVC
Hinze-style Phantom Types
Kindless language
Higher-order polymorphic language (revised)

PhantomTypes.hs

SList.hs
SListTest.hs
Show type substitution lemma for T_ABS & T_APP for ho-poly language
1/28
GADT examples
SList.hs
NList.hs
interp2.hs
interp3.hs
Exercises in interp3.hs
2/2 and 2/4
GADT metatheory
interp-hint.hs
gadt.pdf
Show preservation for T_Case for GADT language
2/9 and 2/11
Type family examples
interp-hint.hs
interp-trans.hs
cps-class.hs
interp-assoc-hw.hs
cps-hw.hs
think about project ideas
2/16
and 2/18
Generic programming with type families
FMap-class.hs
Read System F with Type Equality Coercions
2/23 and 2/25
FC lifting theorem
FC paper

2/25
FC preservation theorem


3/2
FC progress and consistency
ICFP deadline

3/4
F-omega progress
TAPL ch. 30
TAPL 30.3.8 [Single-step diamond property of reduction]
3/9 & 3/11
no class
Spring break

3/16 & 3/18
Kind-directed equivalence in F-omega
ATTAPL Chapter 6
f-omega.pdf
Soundness of algorithmic equivalence.
3/23 & 3/25
no class


3/30
Haskell -> Agda
interp3a.hs interp3a.agda
interp4.agda
SList.hs SList.agda
FMap.hs FMap.agda

4/1
More Agda examples
cps.agda
BSTskel.agda
Finish BST implementation
4/6
UTT_Sigma

Read Chapter 1 of Ulf Norell. Towards a practial programming language based on dependent type theory.
4/8
More Agda examples
BSTskel2.agda version 2

4/13
UTT_Sigma algorithmic rules

Read Chapter 2 of Norell's dissertation
4/15*
no class


4/20
Agda pattern matching


4/22
More Agda pattern matching
pos.adga
Typecheck pred2
4/27
Project presentations


*indicates dates when Prof. Weirich will be away