Princeton University
Computer Science Department

Computer Science 441
Programming Languages

David Walker

Fall 2011

Home Page                                         Notes & Assignments


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


[fri sep 16]

Syntactic Definitions

  slides 1 -- mathematical notation for syntax


[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


[sep 26-30]

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
[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
[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
[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
[oct 24-28]
Midterm Review


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!      
[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
[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
[Nov 21-23]
Implementing Operational Semantics

Learn You a Haskell For Great Good, Chap 13:  A Fistful of Monads slides 16: Monads

slides 17: Monads 2
[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
[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.
[Dec 12-16]
Curry-Howard Isomorphism

Typing Lists


  Notes on the whiteboard

slides 18:  Software Transactional Memory

Assignment 5:  Monads and Monad Laws.  Due 1pm Friday Dec 16.  ExplanationCode.