Master class Logic 20062007: Type theory and Proof Assistants
Organization
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
Material

M.H. Sorensen and P. Urzyczyn, Lectures on the CurryHoward
Isomorphism, Studies in Logic and the Foundations of Mathematics, vol
149, Elsevier 2006.

T. Coquand, P. Dybjer, E. Palmgren, Typetheoretic 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 relevant chapters of the two mentioned books will be handed out at the lectures.
Contents
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.
Assumed knowledge
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 .
Presentations
You have 110 minutes for your presentation. The
time breakdown is as follows:
 10.3011.00 presentation
 11.0012.00 Coq exercise class
 12.0012.40 presentation
 12.4012.50 break
 12.5013.30 presentation
List of presentations:
 SU ch 4, Feb 21, Andrew Polonsky; Exercises for chapter 4.
 SU ch 5, Feb 28, Wouter Stekelenburg Exercises for chapter 5.
 SU ch 10, March 7, Danko Ilik. Exercises: 10.7.9 and 10.7.10
 SU ch 11, March 14, Fomatati Baudelaire. Exercises: 11.8.1, 11.8.6 and 11.8.9
 SU 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"
 CDP 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.
 CDP ch 2, April 18, Takako Nemoto. Exercises: Exercise 1 and 2 on page 46; Verify the last half of page 54.
 CDP ch 3, April 25, Gideon Wormeester. Exercise: Define the functions on page 60
 CDP ch 4,5, May 2, Grant Passmore. Exercises: page 73 ex1, page 71 4.1.11.
 May 9, No Class
 CDP 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,
handouts. 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
 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
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 existentialdiophantine
relation).
Examination
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
presented material.)

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.)
herman
Last modified: Fri May 25 18:44:20 CEST 2007