 Tutorials by Simon Castellan.
 The evaluation form.

The final exam will be
Wednesday 7th January 2015, 9:00  12:00, Amphi B.
 Final exams of previous years: [20122013] [20132014].
 Allowed documents: handwritten or typesetted notes, no article, no book.
Contents

Foundations of interactive theorem proving
 The Coq System
 CurryHoward Correspondance:
 Propositional Logic
 Arithmetic
 Polymorphism

Foundations of automatic theorem proving
 Sequent calculus
 Herbrand's theorem
 The resolution method
Useful stuff
 A colored presentation of the λcalculus.

On the proof assistant Coq:
 To get some convenient shortcuts in coqide, you can use this configuration file .coqiderc
 The reference manual.
 The standard library documentation.
 More documentation.
 The official web page of Coq.
 A reference card of GNU Emacs.
Courses

Course 1 (12th Sept. 2014)
Pure λcalculus.
Bibliography:
Chapter 1 of
Sørensen, M. H. et Urzyczyn, P., Lectures on the CurryHoward Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006. 
See also Chapter 1 of
Krivine, J.L. (traduction de Cori, R.) Lambdacalculus, types and models, Ellis Horwood, 1993. 
For an introduction to pure λcalculus,
we can also have a look at Section 2 of
Barendregt, H. P., Lambda calculi with types. In Handbook of logic in computer science, Volume 2, Oxford, New York: Oxford University Press, 117–309, 1992. 
For more advanced material:
Barendregt, H. P., The Lambda Calculus, Its Syntax and Semantics, Volume 103 de Studies in Logic and the Foundations of Mathematics

Chapter 1 of

Course 2 (19th Sept. 2014)
[slides].
Intuitionistic Propositional Logic (definition & basic properties).
SimplyTyped LambdaCalculus (definition & basic properties).
CurryHoward Correspondence (beginning).
Bibliography:
Chapters 2, 3 and 4 of
Sørensen, M. H. et Urzyczyn, P., Lectures on the CurryHoward Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.

Chapters 2, 3 and 4 of

Course 3 (26th Sept. 2014)
CurryHoward Correspondence: Proof of the correspondence for Minimal Intuitionistic Logic.
λCalculus with products, sums and units: Typing rules and their correspondence with Natural Deduction Rules (summary in these [slides])

Course 4 (3rd Oct. 2014)
[slides].
CurryHoward Correspondence (full system & basic properties).
Heyting Arithmetic (definition and basic properties).
Bibliography:
Chapter 9 of
Sørensen, M. H. et Urzyczyn, P., Lectures on the CurryHoward Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006. 
See also Chapter 3 (and 4) of
Troelstra, A.S. et van Dalen, D., Constructivism in Mathematics, An Introduction (Vol. 1), volume 121 de Studies in Logic and the Foundations of Mathematics, NorthHolland, Elsevier, 1988.

Chapter 9 of

Course 5 (10th Oct. 2014)
[slides].
CurryHoward Correspondence for Intuitionistic Predicate Logic.
Bibliography:
Chapter 8 of
Sørensen, M. H. et Urzyczyn, P., Lectures on the CurryHoward Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.
Gödel's System T (part 1: definition).
Bibliography:
Chapter 10 of
Sørensen, M. H. et Urzyczyn, P., Lectures on the CurryHoward Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.

Chapter 8 of

Course 6 (17th Oct. 2014).
Gödel's System T (part 2: basic properties and weak normalization).
Bibliography:
Chapter 10 of
Sørensen, M. H. et Urzyczyn, P., Lectures on the CurryHoward Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.

Chapter 10 of

Course 7 (24th Oct. 2014)
Representation of functions in Arithmetic & Modified Realizability.
Definition of HA* and PA* in these [notes].
 31st Oct. 2014: All Saints holiday
 7th Nov. 2014: No course

Course 8 (14th Nov. 2014)
Solutions to the homework on Friedman's translation.
Secondorder Logic: Henkin models, the comprehension scheme and Takeuti's comprehension scheme.
Bibliography: Chapter 4 of van Dalen, D., Logic and Structure, Universitext, Springer.

See also
Chapter 11 of
Sørensen, M. H. et Urzyczyn, P., Lectures on the CurryHoward Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.

Course 9 (21st Nov. 2014)
Secondorder logic: Takeuti's comprehension scheme and impredicative codings.
Currystyle System F: definition, codings of basic datatypes and strong normalization.
Bibliography:
Chapter 11 of
Sørensen, M. H. et Urzyczyn, P., Lectures on the CurryHoward Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.

Chapter 11 of
 28th Nov. 2014: no course

Course 10 (5th Dec. 2014)
Sequent Calculus for Propositional Logic, part 1: definition and main properties (definitions in these [notes]).
Bibliography:
Chapter 7 of
Sørensen, M. H. et Urzyczyn, P., Lectures on the CurryHoward Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.  Course notes of Laurent, O. (in french) Théorie de la démonstration.

Chapter 7 of

Course 11 (12th Dec. 2014)
 Sequent Calculus for Propositional Logic, part. 2: proof sketch of cut elimination.
 Sequent Calculus for Predicate Logic: definition and statment of the main properties.
 Herbrand's Theorem, part. 1: definition of the Herbrand normal forms.

Chapter 7 of
Sørensen, M. H. et Urzyczyn, P., Lectures on the CurryHoward Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.  Course notes of Laurent, O. (in french) Théorie de la démonstration.

Course 12 (19th Dec. 2014):
Herbrand's Theorem: full statment.
The Resolution Method.
Back home.