General Information

Schedule

Date

Lecture

Notes

Beluga Code

Assignments

Wed

Jan 9

Overview

Ch 1, Ch 2, Ch 3

Fr

Jan 11

Simple types

Ch 8


Wed

Jan 16

Simple Programming in Beluga

HW1 out

Fr

Jan 18

Programming with dependent types in Beluga


Wed

Jan 23

No Class

Fr

Jan 25

No Class


Wed

Jan 30

Lambda Calculus

Ch 5

HW1 due
HW2 out

Fr

Febn 1

Simply typed lambda calculus

Ch 9


Wed

Feb 6

Representing binders

Ch 6

Fr

Feb 8

Programming with binders and contexts


Wed

Feb 13

Let, Pairs, etc

CH 11

HW2 due
HW3 out

Fr

Feb 15

Sums, Recursion

Ch 11


Wed

Feb 20

References

Ch 13

Fr

Feb 22

Excursion

Ch 14


Wed

Feb 27

Review

HW3 due

Fr

Mar 1

Midterm Exam


Wed

Mar 6

Break

Fr

Mar 8

Break


Wed

Mar 13

Recursive Types

Ch 20

HW4 out

Fr

Mar 15

Polymorphism

CH 23


Wed

Mar 20

Dependently typed Lambda-Calculus

Fr

Mar 22

Dependently typed programming


Wed

Mar 27

Logic:Curry-Howard Isomorphism

CH 12

HW4 due
HW5 out

Fr

Mar 29

No Class: Good Friday


Wed

Apr 3

No class

Fr

Apr 5

Normalization


Wed

Apr 10

Subtyping

HW 5 due

Fr

Apr 12

Subtyping


Tue

Apr 16

Review