Master class Logic 2006-2007: Type theory and Proof Assistants
This forms part of the MRI organised Master class
Logic. Teachers: Herman
Geuvers, [herman at cs dot ru dot nl] and Bas Spitters [spitters at cs dot ru dot nl]
Period: February 14 -- March 14 and March 28 -- May 02
Time: Wednesday 10.30 -- 13.30
Location: HG03.054 (Huygens Building, Radboud University Nijmegen). From February 21 until May 2 there will be Coq (computer) exercise classes from 11.00 to 12.00:
- HG01.329 Feb 21 -- April 4
- HG00.075 April 11 -- April 18
- HG01.329 May 2
The relevant chapters of the two mentioned books will be handed out at the lectures.
M.H. Sorensen and P. Urzyczyn, Lectures on the Curry-Howard
Isomorphism, Studies in Logic and the Foundations of Mathematics, vol
149, Elsevier 2006.
T. Coquand, P. Dybjer, E. Palmgren, Type-theoretic Foundations of
Constructive Mathematics, to appear, preliminary version of 2007.
The Coq proof assistant, tutorial and reference
manual. We will be using Coq through a web interface.
The course consists of:
A seminar, where students present a chapter of one of the
books listed above. This will take place every week 10.30 -- 11.00 and
12.00 -- 13.30. For the distribution of the chapters over the
participants, see below.
An exercise class in Coq. This will start of with an introduction,
working through the tutorial. There is no need to install Coq, as it
is accessible on our server through a web interface. All students will
receive a login on our server.
We assume that students are familiar with the following concepts:
- Type free lambda calculus (e.g. as treated in the first semester course by Barendregt and Capretta)
- Simply typed lambda calculus (e.g. as treated in the first semester course by Barendregt and Capretta)
- The rules fo Natural Deduction, as defined by Gentzen and Prawitz. For the rules see e.g. these presentation sheets .
You have 110 minutes for your presentation. The
time breakdown is as follows:
List of presentations:
- 10.30-11.00 presentation
- 11.00-12.00 Coq exercise class
- 12.00-12.40 presentation
- 12.40-12.50 break
- 12.50-13.30 presentation
- S-U ch 4, Feb 21, Andrew Polonsky; Exercises for chapter 4.
- S-U ch 5, Feb 28, Wouter Stekelenburg Exercises for chapter 5.
- S-U ch 10, March 7, Danko Ilik. Exercises: 10.7.9 and 10.7.10
- S-U ch 11, March 14, Fomatati Baudelaire. Exercises: 11.8.1, 11.8.6 and 11.8.9
- S-U ch 12, March 28, Herman Geuvers Slides in postscript, Slides, 4 slides on one page in postscript. Exercises: 12.7.4, 12.7.5, 12.7.8, 12.7.11.
- April 4, No Class because of "Arithmetic days"
- C-D-P ch 1, April 11, Johany Suarez. Exercises: Ex.1 on page 14, Ex. 2 on page 17, Ex. 7 on page 24, Ex. in Example 1.4.11 on page 35.
- C-D-P ch 2, April 18, Takako Nemoto. Exercises: Exercise 1 and 2 on page 46; Verify the last half of page 54.
- C-D-P ch 3, April 25, Gideon Wormeester. Exercise: Define the functions on page 60
- C-D-P ch 4,5, May 2, Grant Passmore. Exercises: page 73 ex1, page 71 4.1.11.
- May 9, No Class
- C-D-P ch 6,7,8, May 16, Bas Spitters, page 98 Ex2 (Hint: use ex1), page 100 Ex1,2,3, page 106 Ex2, page 110 Ex1,3,4, page 117 Ex2.
How to present a chapter?
You have to explain the chapter that has been assigned to you to your
fellow students. You may use any
kind of medium: black board, overhead projector (let us know in
advance; there is no overhead projector in the room!), beamer,
hand-outs. Some remarks and suggestions
Stay within time limits.
Keep in mind that your fellow students have a copy of the chapter, so
you don't have to literally repeat definitions, lemmas etc. (But of course you may do it if you feel it's necessary.)
Writing on the blackboard takes a lot of time. On the other hand,
presentations using overhead sheets or beamer tend to go too
fast. Choose the appropriate medium.
Allow your fellow students to ask questions. Ask questions to the
audience to check if they are still following you.
Prepare some exercises that your fellow students can take home. The goal of these exercises is
You may also allow for some time during your lecture to make an exercise.
- to give an overview of the material of the chapter,
- to help your fellos students to verify whether they've understood what you've been talking about.
You may choose to focus on a specific part of your chapter and treat
the rest only superficially. Often that will be more interesting than
trying to treat everything in little detail. You can discuss these
choices with the teachers.
Please consult Herman or Bas in case of questions or difficulties.
The following Coq formalizations have been planned. If you're name does not yet have a description behind it, please let me (Herman) know asap what you plan to do.
- Andrew Polonsky
- Wouter Stekelenburg: The undefinability of truth in arithmetic
- Danko Ilik: The construction of reals a
la Stolzenberg (up to the point of computing the number e)
- Fomatati Baudelaire: Wedderburn's theorem (based on the proof by Dick van Leijenhorst)
- Johany Suarez: Ackermann's function grows faster than any primitive recursive function
- Takako Nemoto: Koenig's Lemma
- Gideon Wormeester: partial functions in Bishop's set theory.
- Grant Passmore: Matiyasevich's proof that exponentiation is
diophantine (that is, definable via an existential-diophantine
The students will receive a grade for each of the following three parts of the course:
The presentation of their chapter
The final written exam at the end: May 30, 11.00 -- 14.00, HG 03.045 (The exam will be about all the
The Coq assignment delivered at the end: Deadline Thursday June 14, send your Coq files both to Bas and Herman. (Halfway the course, each
student receives an individual Coq assignment.)
Last modified: Fri May 25 18:44:20 CEST 2007