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