Resources
Lecture Notes and Coq Developments
- Arithmetic expressions (Coq: exp-compile.v)
- Abstract Imp (Coq: imp.v)
- Abstract reduction systems (Coq: star.v,confluencePart1.v, confluence.v, abstractLambdaBeta.v)
- Introduction to lambda calculus
- De Bruijn terms (Coq: deBruijn.v)
- Abstract lambda calculus (Coq: abstractLambdaBeta.v)
- De Bruijn substitution (Coq: subst.v)
- Environment semantics (Coq: lambda_bigstep.v, lambda_env.v)
- Additional reading
- Call-by-Value Lambda Calculus as a Model of Computation in Coq
(Journal of Automated Reasoning 2019) - Untyped lambda calculus (lecture notes from 2015)
- Call-by-Value Lambda Calculus as a Model of Computation in Coq
- Lecture notes for the second half of the course
You may also check the material of previous editions of this course (2017/18 edition).
Coq
- There are two ways to install Coq:
- 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 via opam and it is included in the Windows installer. Documentation about CoqIDE can be found here.
- Proof General: Proof General is an emacs mode that supports many theorem provers, including Coq. Using Proof General, Company Coq is an extension allowing you to look up lemmas and the Coq Documentation. Both Proof General and Company Coq can be installed via the emacs package archive melpa.
- 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,
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.
- Benjamin Pierce, Types and Programming languages. The MIT Press, Cambridge, Massachusetts 2002