### Schedule

The following schedule is approximate and subject to change. Please listen for announcements in class; also see Blog.

Readings: P = Pierce; FFF = Felleisen, Findler, Flatt.

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

There will be no class on the dates in red.