Semantics: Resources

Programming Systems

Teaching

Main page

Timetable

Resources

Registration

Services

Exams and Grade

Login

Discussion Board

We will mainly follow the ebook Software Foundations by Benjamin Pierce and others. We will also rely on the textbook Types and Programming Languages, again written by Benjamin Pierce. Throughout the course we will use the proof assistant Coq.

Lecture Notes

There are rudimentary

• lecture notes

• Expression Compiler
• Basic Imp
• Compiler Imp -> Reg
• Small-step semantics of Imp
• Evaluation semantics of Imp
• Small-step semantics of Imp using a stack
• Hoare logic for Imp
• PCF(no proofs)
• E with typed-indexed syntax
• Simply Typed Lambda Calculus
• Termination of Simply Typed Lambda Calculus
• Simply Typed Lambda Calculus in de Bruijn Representation
• Calculus of Constructions

Coq code used in lectures:

• 2011-11-14
• 2011-11-16
• 2011-11-21
• 2011-11-30
• Termination of Simply Typed Lambda Calculus

Main Texts

• Software Foundations by Benjamin Pierce and others
• Types and Programming Languages by Benjamin Pierce

Coq

• Coq Home Page (download system here, we are using version 8.3)
• Coq Documentation

Further Reading

• Gert Smolka and Chad Brown,
  Lecture notes of the course Introduction to Computational Logic
• Robert Harper,
  Practical Foundations for Programming Languages
• Adam Chlipala,
  Certified programming with dependent types using Coq
• Glynn Winskel,
  The Formal Semantics of Programming Languages: An Introduction.
  MIT Press, 1993.
• Franz Baader and Tobias Nipkow,
  Term Rewriting and All That.
  Cambridge University Press, 1998.
• Nick Benton, Chung-Kil Hur, Andrew Kennedy, and Conor McBride,
  Strongly Typed Term Representations in Coq.
  Journal of Automated Reasoning, March 2011.
  Contains simply typed lambda calculus with type-indexed syntax.
• Zhaohui Luo,
  Computation and Reasoning: A Type Theory for Computer Science.
  Oxford University Press, 1994.