Master class Logic 2006-2007: Type theory and Proof Assistants

Organization

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

Material

• 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.

Contents

• 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.

Assumed knowledge

• 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 .

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?

• 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
  • 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 also allow for some time during your lecture to make an exercise.
• 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.

Coq assignements

• 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 relation).

Examination

1. The presentation of their chapter
2. The final written exam at the end: May 30, 11.00 -- 14.00, HG 03.045 (The exam will be about all the presented material.)
3. 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.)