Advanced Programming Languages meets 10:10-11:00 on Mon & Wed in Upson 315.
| Date | Topic | Notes | Assignments |
|---|---|---|---|
| Week 1 | |||
| Jan 23 | Goals of the Course Operational Semantics Introduction for functional languages |
Student Survey | |
| Jan 25 | Lambda Calculus Reduction Rules Operator Notation |
||
| Jan 27 | PL Lab - Intro to Lab, student survey | ||
| Week 2 | |||
| Jan 30 | What do λ-terms mean? | ||
| Feb 1 | Primitive Recursion - as a PL and foundation for mathematics. Math Preliminaries Classic ML |
Lec5 Notes |
assignment 1 |
| Feb 3 | PL Lab - Applied λ-calculus | CS6110 sp2010 Lect3 Gordon, Milner, Wadsworth: Edinburgh LCF Martin-Lof: Informal Notes on Foundations | |
| Week 3 | |||
| Feb 6 | Evaluation in λ-calculus with environments | ||
| Feb 8 | Evaluation in the λ-calculus with closures and capsules |
Lect8 - Highlights from Kozen & Jeannin's Scoping - note Constable's highlights in Introduction |
|
| Feb 10 | PL Lab - Closures at work in the ML and Nuprl evaluators Comparing Primitive Recursion and ML's recursion as a basis for math | Evaluation Function Using Closures | |
| Week 4 | |||
| Feb 13 | Comparing Evaluators | Lect10 Notes | |
| Feb 15 | Continuations | assignment 2 | |
| Feb 17 | PL Lab - Continuations at work in Primitive Recursive Arithmetic (PRA), Logical rules for Goodstein's PRA, Assertions in Programming Languages | Lect12 Notes | |
| Week 5 | |||
| Feb 20 | Brief Review -- where we stand Introduction to a Simple Imperative Language (IMP) |
IMP-simple imperative language Supplemental: Winskel-IMP |
|
| Feb 22 | Program Schemas (Schemes) |
||
| Feb 24 | PL Lab - Imperative languages for primitive recursive functions (Loop) Subrecursive languages and logics Assertions in programs-prelude to Hoare Logics |
||
| Week 6 | |||
| Feb 27 | Intro to Axiomatic Semantics and Hoare Logic |
||
| Feb 29 | Guest Lecturer: David Gries Asserted Programs |
Gries Lecture on Algorithms |
assignment 3 |
| Mar 2 | PL Lab - Why logic is important for PL. Proofs as Programs. Programming Logics. |
||
| Week 7 | |||
| Mar 5 | Explaining continuations as while loops | Lec19 Notes | |
| Mar 7 | Revisiting continuations. Defunctionalization. | Lect20 Notes (updated p3) | |
| Mar 9 | PL Lab - Godel's system T Introduction to Simple Types |
||
| Week 8 | |||
| Mar 12 | Godel system T. Tait's Method (Logical Relations). | Lect22 Notes- updated 3/14 | |
| Mar 14 | Strong Normalization Prelim Review |
Pierce-Ch12 | |
| Mar 16 | PL Lab - | CMU Lecture Notes | |
| Spring Break: March 19-23 | |||
| Week 9 | |||
| Mar 26 | Typed Lambda Calculus and Recursive Procedures in IMP | An Upper Bound for Reduction Sequences in the Typed λ-calculus. By Schwichtenberg Procedures and Paramteres: An axiomatic Approach. By Hoare The Typed λ-calculus is not Elementary Recursive. By Statman |
|
| Mar 28 | In class Prelim. There will not be a take home part, only in-class. | ||
| Mar 30 | PL Lab - Functions in Imperative Languages | LNCS-PL/CV pages 160-168 | assignment 4 |
| Week 10 | |||
| Apr 2 | Applied Lambda Calculus (products, sums, void) |
Types for Applied Lambda Calculus supplemental: Curry - Historical Analogies with Propositional Algebra |
|
| Apr 4 | Compiling with continuations - Lecture by Andrew Myers | Lect27 Notes | |
| Apr 6 | PL Lab - Evidence Semantics for Propositions | Semantics of Evidence | |
| Week 11 | |||
| Apr 9 | Propositional Logic and the Typed Lambda Calculus |
Refinement rules for FOL | |
| Apr 11 | Proofs and Evidence | See April 9 notes | assignment 5
updated 4/18 |
| Apr 13 | PL Lab - Dependent Types and First-Order Logic | See April 9 notes |
|
| Week 12 | |||
| Apr 16 | Proof Rules for Dependent Types | ||
| Apr 18 | Specification Languages (Lecture 33) | Products, Sums, and Other Datatypes | |
| Apr 20 | PL Lab - Defining Types | Part 1 of Martin-Löf: Constructive Mathematics and Computer Programming | |
| Week 13 | |||
| Apr 23 | Proofs as Programs | ||
| Apr 25 | What is a Type? | assignment 6 updated 5/1 with problem 7 added Due May 4 |
|
| Apr 27 | PL Lab - Birth of Constructive Type Theory & Recursive Types |
Full article from Martin-Löf: Constructive Mathematics and Computer Programming |
|
| Week 14 | |||
| Apr 30 | Type Theory | ||
| May 2 | Distributed Computing | ||
| May 4 | Last Class | Lect 40 Notes | |
| May 14 | Final Exam: 9:30-12:30 in Upson 315 | Exam Review Notes | |