Next meeting:
The seminar is now over
Robert Recorde Room
Seminar Series on Foundations of Theorem Proving
- This series focuses on type theory as foundation of
mechanised theorem proving, and should provide a theoretical
introduction to the use of proof assistants such as Coq, Agda
and Isabelle. Both the articles we would like to cover ([1]
and [2]) are essentially overviews of dependent type systems.
Literature
- [1] Proof-Assistants using Dependent Type Systems, by Henk Barendregt and Herman Geuvers, included as chapter 1 in Handbook of Automated Reasoning, edited by A. Robinson and A. Voronkov, published in 2001
- [2] Dependent Types, by David Aspinall and Martin Hofmann, included as chapter 2 in Advanced Topics in Type Theory and Programming Languages, edited by B. C. Pierce, published in 2005.
Time Plan
- Thursday 20th Feb: sections 1 and 2 of [1] - Paolo
- Thursday 27th Feb: section 3 of [1] - Paolo
- Thursday 6th March: sections 2.1 and 2.2 of [2] (including the exercises) - Alison
- Tuesday 11th March: sections 2.3, 2.4 and 2.5 of [2] (excluding the exercises) - Greg
- Tuesday 18th March: exercises in sections 2.3, 2.4 and
2.5 of [2], related to the following properties:
- Strong normalisation of beta reduction (theorem 2.3.5)
- Confluence of beta reduction (theorem 2.3.6): Tait-Martin-Loef proof (see sup. read. [A] and [E]), proof through Newman's lemma (see [D], appendix)
- Soundness (lemma 2.4.2) and completeness (lemma 2.4.4) of Algorithmic Lambda LF
- Termination of type checking in Algorithmic Lambda LF (theorem 2.4.7)
- Type preservation of beta reduction in Lambda LF (theorem 2.4.10)
- Extension to Sigma types (exercise 2.5.1) - Friday 21th March: exercises in sections 2.3, 2.4 and 2.5 of [2] (continued)
- Tuesday 25th March: sections 2.6 and 2.7 of [2] (excluding the exercises) - Casper
- Thursday 27th March: exercises in section 2.6 [2]
- Tuesday 1th April: sections 2.8 and 2.9 of [2] - Ferdinand
Supplemenary reading
- [A] Lambda Calculi with Types, by Henk Barendregt, included in Volume 2 of Handbook of Logic in Computer Science, edited by S. Abramsky, D. M. Gabbay and T. S. E. Maibaum, published in 1992
- [B] Logical Frameworks, by Frank Pfenning, included in Proof Systems and Reliability, edited by H. Schwichtenberg and R. Steinbruegger, published in 2002
- [C] Intuitionistic Type Theory, by Per Martin-Loef, notes by G. Sambin of lectures given in Padua in 1980
- [D] Lambda Calculus, by Tobias Nipkow, lecture notes, 2012
- [E] Lambda Calculus and Types, by Andrew D. Ker, lecture notes, 2009
- [F] The Coq theorem prover webpage
- [G] Coq in a hurry, tutorial, by Yves Bertot, 2010
- [H] Software Foundations, by Benjamin C. Pierce et at., 2013 [J] Introduction to generalized type systems , by Henk Barendregt, in Journal of Functional Programming vol. 1(2), pp. 125-154, 1991