Princeton University
|
Computer Science 441
|
|
FINAL EXAM: once you download the final exam files final.lhs and exam-semantics.txt, you have 3 hours (plus a 20 minute grace period) to complete it. You must begin the exam between 12:01am Wednesday Jan 18 and 11:59pm Wednesday Jan 18. Other instructions are included with the exam.
final.lhs exam-semantics.txt <<<-- DOWNLOAD THESE TO START THE EXAM!
Here is an approximate schedule for COS 441. This schedule is only approximate and may be changed at any time.
| Week | Topics | Reading | Notes/Assignments |
|
0 [fri sep 16] |
Syntactic Definitions |
slides 1 -- mathematical notation for syntax | |
|
1 [sep 19 -23] |
Inductive functions Denotational semantics Inductive proofs Haskell intro Proofs about Haskell programs |
Pierce Text Chapter 2.4, 3.1-3.3 Learn You a Haskell for Great Good: Read the Intro, Getting Started |
slides 2 --
denotational semantics and proofs by induction Assignment 1.pdf or Assignment1.docx Due 1pm Tuesday Sept 27 Download and install the Haskell platform and SOE libraries. See here for instructions. slides3A -- introducing Haskell, functional abstraction and computation by calculation, reasoning about functional programs |
|
2 [sep 26-30] |
Types! Higher-order programming |
Learn You a
Haskell for Great Good: Read Chapers 2-5 Read Chapter 7, up to but not including the section on "type classes 102" |
slides3B -- more
Haskell basics & proofs by induction about Haskell programs slides 4 -- data types, type synonyms & type abstraction slides 5 -- I/O and referential transparency. sierpinski.hs slides 6 -- higher-order programming, abstraction over recursive definitions. Hakyll. Literate Haskell: lec06.lhs Assignment 2 Due 1pm Tuesday Oct 11 |
|
3 [oct 3-7] |
Qualified types & type classes Case Study: A domain-specific language for functional animation |
Learn You a
Haskell for Great Good: Read Chapter 2 on "type classes 101", Chapter 7 on "type classes 102" Read handout on functional animation |
slides 7 -- ad hoc polymorphism and type classes.
Hakyll. Literate
Haskell: lec07.lhs slides 7b -- proofs about type classes; induction on the structure of types slides 8 -- functional animation. Hakyll. Literate Haskell: lec08.lhs |
|
4 [oct 10-14] |
Higher-order type classes, Higher Kinds Reasoning about imperative programs |
Read handout on Hoare Logic | slides 9 -- Higher-order
Type Classes, Kinds and Functors slides 10 -- Hoare Logic Intro Assignment 3 a3-typeclasses.lhs a3-solar.lhs Parts I-IV Due 1pm Friday Oct 21; Part V Due 1pm Friday Nov 11 |
|
5 [oct 17-21] |
Judgements and Proofs Weakest Pre-Conditions Reasoning about the Heap |
slides 10b -- Hoare
Logic Rules slides 11 -- Judgements and Proofs slides 12 -- Hoare Logic: Loops |
|
|
6 [oct 24-28] |
Midterm Review Midterm Case Study: A domain-specific language for computing with financial contracts |
additional type classes proof midterm: In class; Oct 26. You may bring in 1 Cheat-Sheet in to the exam with writing on both sides. Write anything you want, however you want. No magnifying glasses or microscopes allowed. (Conventional glasses and contact lenses are ok! :-) midterm solutions |
|
| Fall Break! | |||
|
7 [Nov 7-11] |
Operational Semantics Untyped Lambda Calculus Proving Properties of Operational Semantics Call-by-Value vs. Call-by-Name |
Read Pierce Text Chap 3.4, 3.5 Read Pierce Text Chap 5.1, 5.2 |
slides 13 -- Lambda
Calculus 1 slides 14 -- Lambda Calculus 2 Implementing the Lambda Calculus with Higher-Order Abstract Syntax: Lambda.hs Lambda-eg.hs Implementing the Lambda Calculus with First-Order Abstract Syntax: LambdaFA.hs LambdaFA-eg.hs slides 15 -- Lambda Calculus implementation & a proof Assignment 3, Part V due 1pm Friday Nov 11 |
|
8 [Nov 14-18] |
More Operational Semantics Extended Lambda Calculus Operational Semantics for Languages with State |
Assignment 4 Explanation
Code due 1pm
Tuesday Nov 29 Monday: Assignment 4 Tutorial (whiteboard/demo) Wednesday: Proof that closedness is preserved by operational semantics, operational semantics for recursive functions, if and integers (whiteboard) Friday: More operational semantics: sums, pairs, stateful languages (Imp), languages with printing |
|
|
9 [Nov 21-23] (Thanksgiving) |
Implementing Operational Semantics Monads |
Learn You a Haskell For Great Good, Chap 13: A Fistful of Monads | slides 16: Monads slides 17: Monads 2 |
|
10 [Nov 28-Dec 2] |
Simple Type Systems with function types, integers and
booleans Typing Rules Proof of Progress, Preservation and Type Safety |
Read Pierce Chap 8, 9 | Assignment 4: Hoare Logic due 1pm Tuesday Nov 29 lambda calculus safety proof part 1 lambda calculus safety proof part 2 |
|
11 [Dec 5-9] |
Proof of Progress, Preservation Continued Sum types, pair types, unit and void Curry-Howard Isomorphism |
Read Pierce Chap 11 | Notes on the whiteboard. |
|
12 [Dec 12-16] |
Curry-Howard Isomorphism Typing Lists Polymorphism Parallelism |
Notes on the whiteboard slides 18: Software Transactional Memory Assignment 5: Monads and Monad Laws. Due 1pm Friday Dec 16. Explanation. Code. |