Princeton University

Computer Science 441


FINAL EXAM: once you download the final exam files final.lhs and examsemantics.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 examsemantics.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.13.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 2630] 
Types! Higherorder programming 
Learn You a
Haskell for Great Good: Read Chapers 25 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  higherorder programming, abstraction over recursive definitions. Hakyll. Literate Haskell: lec06.lhs Assignment 2 Due 1pm Tuesday Oct 11 
3 [oct 37] 
Qualified types & type classes Case Study: A domainspecific 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 1014] 
Higherorder type classes, Higher Kinds Reasoning about imperative programs 
Read handout on Hoare Logic  slides 9  Higherorder
Type Classes, Kinds and Functors slides 10  Hoare Logic Intro Assignment 3 a3typeclasses.lhs a3solar.lhs Parts IIV Due 1pm Friday Oct 21; Part V Due 1pm Friday Nov 11 
5 [oct 1721] 
Judgements and Proofs Weakest PreConditions Reasoning about the Heap 
slides 10b  Hoare
Logic Rules slides 11  Judgements and Proofs slides 12  Hoare Logic: Loops 

6 [oct 2428] 
Midterm Review Midterm Case Study: A domainspecific language for computing with financial contracts 
additional type classes proof midterm: In class; Oct 26. You may bring in 1 CheatSheet 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 711] 
Operational Semantics Untyped Lambda Calculus Proving Properties of Operational Semantics CallbyValue vs. CallbyName 
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 HigherOrder Abstract Syntax: Lambda.hs Lambdaeg.hs Implementing the Lambda Calculus with FirstOrder Abstract Syntax: LambdaFA.hs LambdaFAeg.hs slides 15  Lambda Calculus implementation & a proof Assignment 3, Part V due 1pm Friday Nov 11 
8 [Nov 1418] 
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 2123] (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 28Dec 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 59] 
Proof of Progress, Preservation Continued Sum types, pair types, unit and void CurryHoward Isomorphism 
Read Pierce Chap 11  Notes on the whiteboard. 
12 [Dec 1216] 
CurryHoward 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. 