Date

Topic

Readings

Problem Set

01/06 M

Welcome; syntax; reduction; structural operational semantics

P 1,2; FFF I.1

01/08 W

Redex

FFF II.A, II.11, II.12 Quote, Unquote

01/13 M

Lambda calculus; CBV vs. CBN; recursion; encodings

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

01/15 W

Evaluation contexts; reduction; equivalence; normal forms

P 5.2

PS1 due 01/16

01/20 M

no class: MLK day

01/22 W

no class: POPL

01/27 M

cancelled

PS2 due 01/27

01/29 W

Semantics by translation

02/03 M

Imperative languages: small-step and big-step SOS

P 3.2,3.3

02/05 W

Inductive definitions, well-founded induction, rule induction

02/07 F

Proofs by structural and rule induction

Project Topic due

02/10 M

uML, strong typing, run-time type checking

PS3 due

02/12 W

State and memory; Naming and scope

02/14 F

Abstract machines

FFF I.6

02/17 M

no class: Presidents' day

02/19 W

Continuation-passing style; CPS conversion

02/21 F

Compiling with continuations

02/24 M

Simply typed lambda calculus

P 8.1,8.2, 9.1.,9.2

Project Proposal due, PS4 due 02/25

02/26 W

Type safety

P 8.2,9.3-9.5

02/27 Th

MIDTERM: 5pm-6:40pm

03/02 M

Spring break

03/04 W

Spring break

03/09 M

Products, sums, recursion, and more

P 11

03/11 W

References

P 13

03/16 M

Exceptions

P 14

03/18 W

Subtyping

P 15.1-15.6

PS5 due 03/20

03/23 M

Recursive Types

P 20

03/25 W

Parametric polymorphism

P 23

03/30 M

Strong normalization and logical relations

P 12

PS6 due 03/30

04/01 W

Existential types

P 24

04/06 M

Propositions as Types/Linear Types

P 9.4

Project Report due

04/08 W

Project Presentations (2:50-?:??)

04/10 F

Project Presentations (?:00-?:00)

04/13 M

Project Presentations (2:50-?:??)

04/14 Tu

Project Presentations (tbd)

04/15 W

Project Presentations (2:50-?:??)

04/16 Th

Project Presentations (tbd)

04/17 F

Project Presentations (tbd)