Lecture Material and Schedule

Week 1

• Introduction and Outline
  Slides: [pdf] [pdf 2x2] (updated 20/7/2009)
  
  
• What is a Programming Language?
  Slides: [pdf] [pdf 2x2]
  Extra Material:
  • Source for the Colossal Cave Adventure
  • Fortran for the IBM 704, 1956
  • The Next 700 Programming Languages, Landin, 1966
  
  
• Haskell by Example
  In this lecture I'll construct and demonstrate an interpreter for the lambda calculus, in Haskell.
  There are no formal slides, but check out the Haskell Resources
  Source code for the interpreter: lambda.tgz
  

Week 2

• More on the Lambda Calculus
  These will also be useful for the Haskell by Example lecture. Some of this material overlaps with COMP2600 from last year, but not everyone has done that course. I'll also be going into greater detail this time around.
  Slides:
  • [lambda-pdf] [lambda-pdf2x2] (typos on slide 11 fixed 22/7/2009)
  • [church-pdf] [church-pdf2x2]
  Notes: [lambdanotes-pdf] [lambdanotes-pdf2x1]
  Extra material:
  • The lambda calculus reduction workbench
  • Source for the lambda interpreter: reduce.tgz
  
  
• Reduction Strategies
  Slides: [pdf] [pdf 2x2]
  Extra material:
  • Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2002
  • A Natural Semantics for Lazy Evaluation, John Launchbury, 1993
  
  
• The Typed Lambda Calculus
  Slides: [pdf] [pdf 2x2]
  

Week 3

• Programs are Proofs
  Slides: [pdf] [pdf 2x2]
  
  
• Compilation by Transformation
  Slides: [pdf] [pdf 2x2] (typos on slide 30 fixed 4/8/2009)
  Extra Material:
  • A transformation based optimiser for Haskell, Simon Peyton Jones and Andre Santos, 1997
  • Unboxed values as first class citizens, Simon Peyton Jones and John Launchbury, 1991
  
  
• No lecture on Wednesday (5th August)
  

Week 4

• Lexical Analysis
  Slides: [pdf] [pdf 2x2] (diagram on slide 18 fixed 10/9/2009)
  
  
• Top Down Parsing
  This will be a tutorial style lecture, working through the material on the board.
  The week 4 practical is also on top down parsing.
  Notes: [pdf] [pdf 2x1]
  Example code: code.tgz
  
  
• Polymorphic Type Inference
  Slides: [pdf] [pdf 2x2]
  Extra Material:
  • A theory of type polymorphism in programming, Robin Milner, 1978
    Note that the constraint based inference algorithm presented in the lecture has a different form to algorithm W, which is used in the paper.
  
  

Week 5

• System-F and the Lambda Cube
  Slides: [pdf] [pdf 2x2]
  Extra Material:
  • The Glasgow Haskell compiler: A technical overview, Simon Peyton Jones et al, 1992
  • Introduction to generalized type systems, Henk Barendregt, 1991
  • Henk: a typed intermediate language, Simon Peyton Jones and Erik Meijer, 1997
  
  
• Bison and Flex
  Notes: [pdf]
  We will also use these notes for next week's lectures on bottom-up parsing.
  
  
• No Lecture on Wednesday (19th August)
  
  

Week 6

• Bottom-up Parsing (1)
• Bottom-up Parsing (2)
• Introduction to Assignment 2

Weeks 7 - 8

• No lectures in weeks 7-8

Week 9

• No lecture on Monday
  
  
• Fixpoint Theory
  Notes: [pdf] [pdf 2x1]
  
  
• Fixpoint Theory (2)
  

Week 10

• Operational Semantics
  Notes: [pdf] [pdf 2x1]
  These will also be used for next week's lectures.
  
  
• Rule Induction
  Notes: [pdf] [pdf 2x2] (typos fixed 13:30pm 22/9/2009)
  Extra Material:
  • Mechanising Metatheory in a Logical Framework, Robert Harper and Dan Licata, 2006
  
  
  
• A Syntactic Approach to Type Soundness
  Notes: [pdf] [pdf 2x2]
  Extra Material:
  • A Syntactic Approach to Type Soundness, Andrew Wright and Matthias Felleisen, 1991

Mid-semester break week 1

Mid-semester break week 2

Week 11

• No lecture on Monday
• Operational Semantics of Blocks and Procedures
• Denotational Semantics

Week 12

• No lecture on Monday
• .. of Continuations and Control
  
  
• Strictness Analysis
  Notes: [pdf] [pdf 2x2]

Week 13

• No lecture on Monday
  
  
• Effect Typing the DDC
  Notes: [pdf] [pdf 2x2]
  Extra material:
  • The Type and Effect Discipline, Jean-Pierre Talpin and Pierre Jouvelot, 1994
  • Witnessing Purity Constancy and Mutability, Ben Lippmeier, 2009
  
  
• Summary and Exam Revision
  Notes: [pdf] [pdf 2x2]