Date 
Topic 
Notes 
Homework

1/14

Introduction
Dependent Types in Haskell
via "Phantom Types"

Haskell examples
Hinze, Fun
with Phantom Types (Sections 13,7)
"Haskell" higherorder polymorphism

Fun with Phantom Types
#3 & #17

1/19 & 1/21*

no class

MLK day and POPL


1/26

Kindless higherorder polymorphism & BVC
Hinzestyle Phantom Types

Kindless language
Higherorder polymorphic language
(revised)
PhantomTypes.hs
SList.hs
SListTest.hs

Show type substitution
lemma for T_ABS & T_APP for hopoly language

1/28

GADT examples

SList.hs
NList.hs
interp2.hs
interp3.hs

Exercises in interp3.hs

2/2 and 2/4

GADT metatheory

interphint.hs
gadt.pdf

Show preservation for
T_Case for GADT language

2/9 and 2/11

Type family examples

interphint.hs
interptrans.hs
cpsclass.hs

interpassochw.hs
cpshw.hs
think about project ideas

2/16
and 2/18

Generic programming with type families

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

Fomega progress

TAPL ch. 30

TAPL 30.3.8 [Singlestep
diamond property of reduction]

3/9 & 3/11

no class

Spring break


3/16 & 3/18

Kinddirected equivalence in Fomega

ATTAPL Chapter 6
fomega.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


