Lecture Notes and Exercises

• Syntax.
  • Handout 0: Syntax, 13 Jan, 2010
  • Exercise Sheet 0, 15 Jan, 2010 Solutions
• Lambda Calculus.
  • Handout 10 from Models of Computation, 20 Jan
  • Handout 1: Conceptual introduction to lambda calculus, 20 Jan
  • Handout 2: Lambda Calculus Examples, 27 Jan
  • Handout 3: Pure and Applied Lambda Calculi, 1 Feb
  • Handout 4: Reduction Semantics, 8 Feb
  • Exercise Sheet 1, 22 Jan. Solutions
  • Exercise Sheet 2, 29 Jan. Solutions
  • Exercise Sheet 3, 5 Feb. Solutions
  • Exercise Sheet 4, 12 Feb. Solutions
• Type systems
  • Handout 5: Simply typed lambda calculus, 15 Feb.
    (Note a small correction in paragraph 10, table, step 7. The justification should be "from 5 and 6, using ->Elim".)
  • Handout 6 : Polymorphic type systems, 15 Feb.
  • Additional reading: Generics in the Java Programming Language by Gilad Bracha
  • Exercise Sheet 5, 19 Feb. Solutions
  • Unassessed Exercise Sheet 5+, 26 Feb. Solutions
  • Class Test 1, 16 Feb. Solutions
• Operational Semantics
  • Handout 7: Call by Name and Call by Value.
  • Handout 8: Environment Model of Evaluation, 19 Mar.
  • Environment Model of Evaluation, from the online edition of Structure and Interpretation of Computer Programs, by Abelson and Sussman.
  • Handout 9: Abstract Machine Semantics , 19 Mar. (Not covered in detail.)
  • Exercise Sheet 6, 12 Mar. Solutions
  • Exercise Sheet 7, 19 Mar. Solutions
  • Exercise Sheet 8, 26 Mar. Solutions and a diagram.
• Computational Effects
  • Handout 10: Computational effects, 22 Mar.
• Revision
  • Revision lectures: Part 1, Part 2, Part 3

  ---

• Abstract Machines
  • Handout : Compilation issues , 26 Feb. Revised 9 Mar.

Resources

• Current issues in Programming Languages
  • Grand Challenges in Programming Languages (Notes from a conference session: 2009 ACM Symposium on Principles of Programming Languages)
• Wikipedia pages on topics
  • Lambda calculus
  • Evaluation strategy (including call-by-name, call-by-value and call-by-need)
  • Free variables and bound variables
  • SECD Machine
  • Closure
  • Variable
  • Type polymorphism
  • Subtyping
  • Covariance and contravariance
  • Scheme programming language
  • ML programming language
  • Algol 60
  • Algol 68
  • Simula
  • Pizza
• Wikipedia pages on scientists:
  • Alonzo Church
  • Peter Landin
  • Christopher Strachey
  • Dana Scott
  • Gordon Plotkin
  • John Reynolds
  • Jean-Yves Girard
• Mathematical Geneology: Alonzo Church, Christopher Strachey
• Lambda calculus tutorials
  • Peter Selinger's lecture notes on lambda calculus.
  • Barendregt and Barendsen's "Introduction to Lambda Calculus" (a bit advanced).
  • Chris Barker's lambda calculus tutorial.
  • Benjamin Pierce's Foundational calculi for programming languages
• Fundamental concepts in programming languages by Christopher Strachey (Local access in Birmingham)
• Abelson and Sussman's 'Structure and and Interpretation of Computer Programs' (online edition from MIT Press)

Staff Details

Teaching Assistant: Roly Perera
Room 145
Email: rnp 'at' cs.bham.ac.uk
Office hour: Tuesdays, 2:00-3:00pm

Lectures

Exercise Class

Module Description and Syllabus

General Information about the Module