Semantics Derek Dreyer and Gert Smolka

Lecture Notes    

• Untyped Lambda Calculus
• Confluence and Normalization
• Substitution in Lambda Calculus
• Typed Lambda Calculi
• Semantics of Type Systems

You may also check the material of the 2013/14 edition of this course.

Coq Developments

• Abstract Reduction Systems (ARS.v)
• Confluence of L reduction (L.v)
• Confluence of SK reduction (SK.v)
• Untyped Lambda Calculus
  • Substitution (UntypedLambda.v)
  • Reduction (Reduction.v)
  • Confluence (Confluence.v)

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, 2014
• M.H. Sorensosen and P. Urzyczyn,
  Lectures on the Curry-Howard Isomorphism.
  Elsevier, 2006.
• Rob Nederpelt and Herman Geuvers,
  Type Theory and Formal Proof, An Introduction.
  Cambridge University Press, 2014.
• 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.
• 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.
• 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.
• Robert Harper,
  Practical Foundations for Programming Languages.
  Cambridge University Press, 2013.
• Xavier Leroy
  Mechanized semantics, with applications to program proof and compiler verification
• Tobias Nipkow, Gerwin Klein,
  Concrete Semantics.  With Isabelle HOL.
  Springer, 2014
• 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.
• Dana S. Scott, Lambda Calculus: Then and Now, Slides, 2013.