Semantics : Resources

Lecture Notes

• Lecture notes (appear as the lectures proceed)
  last modified at:
• Accompanying Coq developments (HTML movies powered by Proviola).
  • Church numerals
  • Inductive predicates
  • Base library
  • Abstract reduction systems
  • Combinatory logic
  • Untyped lambda calculus, Basis
  • Church-Rosser theorem for ULC

Coq

• Coq Home Page (download system here, we are using version 8.4)
• There are two user interfaces for Coq: CoqIDE and Proof General. You can choose which one you want to use.
  • CoqIDE: You can download and install CoqIDE along with the rest of Coq from the Coq Home Page. Documentation about CoqIDE can be found here.
  • Proof General: Proof General is an emacs mode that supports many theorem provers, including Coq. You can download Proof General from this link.
• Coq Documentation
• An online book on software foundations starting with an introduction to Coq
  (by Benjamin Pierce and others)
• A book on certified programming with dependent types using Coq
  (by Adam Chlipala)

Literature

• Gert Smolka and Chad Brown,
  Lecture notes of the course Introduction to Computational Logic
• Xavier Leroy
  Mechanized semantics, with applications to program proof and compiler verification
• Tobias Nipkow, Gerwin Klein
  Concrete Semantics
• Zhaohui Luo,
  Computation and Reasoning: A Type Theory for Computer Science.
  Oxford University Press, 1994.
• Jean-Yves Girard,
  Proofs and Types.
  Cambridge University Press, 1990.
• J. Roger Hindley and Jonathan P. Seldin,
  Lambda Calculus and Combinators: An Introduction.
  Cambridge University Press, 2008.
• Henk Barendregt
  The Lambda Calculus, Its Syntax and Semantics
  North-Holland Publishing Company, 1981
• Henk Barendregt, Wil Dekkers, Richard Statman,
  Lambda Calculus with Types.
  Cambridge University Press, 2013.
• Henk Barendregt and Herman Geuvers,
  Proof-checking using Dependent Type Systems.
  Handbook of Automated Reasoning, Volume II, 1149--1240.
  Elsevier 2001.
• Robert Harper,
  Practical Foundations for Programming Languages
• Per Martin-Löf,
  An Intuitionistic Theory of Types, original version from 1972.
  Appears in Giovanni Sambin and Jan Smith (editors), Twenty-Five Years of Constructive Type Theory, Proceedings of a Congress Held in Venice, October 1995; Clarendon Press, Oxford, 1998.
• Per Martin-Löf,
  Intuitionistic Type Theory, Volume1 of Studies in Proof Theory, Bibliopolis, 1984.
• 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.

Slides

• Dana S. Scott
  Lambda Calculus: Then and Now