Semantics Derek Dreyer and Gert Smolka

Lecture Notes and Coq Developments 

1. Compiling arithmetic expressions (Coq)
2. Small-step and big-step semantics of abstract Imp (Coq)
3. Small-step evaluation of abstract expressions (Coq)
4. Call-by-value lambda calculus (Coq)
5. Confluence (Coq1, Coq2)
6. From L to Lambda-Beta
7. Substitution (Coq)
8. Untyped lambda calculus (from 2015)
9. Paper on call-by-value lambda calculus as a model of computation (ITP 2017)
10. Semantics of Type Systems

You may also check the material of previous editions of this course (2015/16 edition).

Coq

• Coq Home Page (download system here, we are using version 8.7)
• 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. Using Proof General, Company Coq is an extension allowing you to look up lemmas and the Coq Documentation.
• Coq Documentation

Literature

• Gert Smolka, 
  Lecture notes of the course Introduction to Computational Logic
• Benjamin Pierce et al,
  An online book on software foundations starting with an introduction to Coq
• Adam Chlipala,
  Certified programming with dependent types using Coq
• 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
• Franz Baader and Tobias Nipkow,
  Term Rewriting and All That.
  Cambridge University Press, 1998.
• Xavier Leroy
  Mechanized semantics, with applications to program proof and compiler verification
• 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.
• 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.
• Tobias Nipkow, Gerwin Klein,
  Concrete Semantics.  With Isabelle HOL.
  Springer, 2014
• 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.