Date

Topic

Readings

Problem Set

01/10 T

Welcome; syntax; reduction; structural operational semantics

P 1,2; FFF I.1

01/13 F

Redex

FFF II.A, II.11, II.12

01/17 T

no class

01/20 F

no class

01/24 T

More Redex

Quote, Unquote

PS1 due 1/23

01/27 F

Lambda calculus; CBV vs. CBN; recursion; encodings

P 3,5; FFF I.2, I.3

01/31 T

Evaluation contexts; reduction; equivalence; normal forms

P 5.2

02/03 F

Semantics by translation

02/07 T

Imperative languages: small-step and big-step SOS

P 3.2,3.3

02/10 F

Inductive definitions, well-founded induction, rule induction

02/14 T

Proofs by structural and rule induction

Project Topic due

02/17 F

uML, strong typing, run-time type checking

02/21 T

State and memory; Naming and scope

02/24 F

Abstract machines

FFF I.6

02/28 T

Continuation-passing style; CPS conversion

03/03 F

Compiling with continuations

Project Proposal due

03/07 T

Spring break

03/10 F

Spring break

03/14 T

Simply typed lambda calculus

P 8.1,8.2, 9.1.,9.2

03/16 Th

MIDTERM: 5pm-6:40pm

03/17 F

no class: PhD open house

03/21 T

Type safety

P 8.2,9.3-9.5

03/24 F

Products, sums, recursion, and more

P 11

03/28 T

References

P 13

03/31 F

Exceptions

P 14

04/04 T

Subtyping

P 15.1-15.6

04/07 F

Parametric polymorphism

P 23

04/11 T

Strong normalization and logical relations

P 12

04/14 F

Existential types

P 24

Project Report due Thursday 04/13, 5pm

04/17 M

Project Presentations (11:00-12:40)

04/18 T

Project Presentations (3:25-5:05)

04/19 W

Project Presentations (11:00-12:40)

04/21 F

Project Presentations (3:25-5:05)