Proving with Computer Assistance 2IMF15

Teacher

• home page
• Room number MF6.103 (only on Thursdays)
• For contact, please use the e-mail address herman at cs dot ru dot nl and please use 2IMF15 in your Subject header

Location and time

• Thursdays, 10:45-12:30 in Metaforum 06 (with exceptions, see below) and 13:30-15:15 in Atlas 2.225

Prerequisites

• For those not familiar with untyped lambda calculus:
  I will do a short recapitulation in hour 2 of the Lecture 1. Furthermore, read the selected pages of Introduction to Lambda Calculus of Barendregt and Barendsen, Chapter 1, Chapter 4 pp. 22-26, Chapter 2 pp. 12-14 (read = as beta-equality =_{\beta}) As exercises, please make 2.5 -- 2.10.

Material

• On Type Theory: Introduction to Type Theory by Herman Geuvers, notes of a summer school course given in Uruguay in 2008. The material of lectures 2, 3, 5, 6, 12 is covered in these notes.
• The book Type Theory and Formal Proof -- An Introduction (Rob Nederpelt and Herman Geuvers) has appeared in November 2014 with Cambridge University Press. The course basically covers the material in the book with a "hands on experience": using the proof assistant Coq. The link above gives background material. You can order the book with CUP, or via the teacher.
• On lambda calculus: Introduction to Lambda Calculus - selected pages by Barendregt and Barendsen. (This is a selection of pages from the full Introduction to Lambda Calculus.)
• The slides of the course, please find the pdfs below.
• On the Coq Proof Assistant (soon to be renamed to "Rocq"): you may find one of the following useful:
  • Coq in a Hurry by Yves Bertot. A quick introduction to Coq, notably read Section 3.
  • A quick reference page with a list of simple useful Coq tactics.
  • A short and convenient cheatsheet with a list of useful Coq goodies by Jules Jacobs.
  • A short introduction to Coq by the developers.
  • The starting page for Coq documentation.

System we will use

• You have to download and install Coq yourself.
• Throughout the course we will be showing a number of Coq files and for some you will need to fill in the proofs yourself as an exercise. Your assignment is a formalization in Coq.

Some useful links

• The Coq standard library.
• The Coq tactic index.
• The Coq command index.
• The Coq automation page.
• The Coq online reference manual.
• The Coq home page

The course by week

I am not yet sure if the course will be recorded. If not, recordings of a previous year will provided on Canvas. This year's course will roughly have the same content. NB. The schedule may be subject to changes! Especially the slides and exercises may be adapted as we go along the course.

• 13/2, 10:45--12:30 Lecture 1
  Overview and Introduction: Proof Assistants, Verification, Logic, Type Theory, Formulas-as-types, Coq.
  Short recapitulation of lambda calculus.
  • Here are the slides of the first hour.
  • Here are the slides of the second hour, on untyped lambda calculus.
  • Make exercises 2.5 -- 2.10 of Introduction to Lambda Calculus - selected pages by Barendregt and Barendsen. See Canvas for some answers.
• 13/2, 13:30--15:15 Lecture 2
  Simple Type theory and "Formulas-as-Types" for propositional logic.
  • Here are the slides of the lecture.
  • See Section 3 of Introduction to Type Theory.
  • Make the theory exercises.
• 20/2, 10:45-12:30 Lecture 3
  Dependent Type Theory.
  • Here are the slides of the lecture.
  • See Section 6 of Introduction to Type Theory.
  • Make the exercises.
• 20/2, 13:30-15:15 Lecture 4
  Natural Deduction in Coq: proposition logic and predicate logic. Be sure to have Coq installed on your laptop/computer
  • Here is a page with a list of simple useful tactics
  • Proposition Logic: Here is the file with the proposition logic Coq exercises of the lecture, or if you prefer in html. Complete this at home and send it to the teacher by mail by February 28.
  • Predicate logic: Here is a file with the predicate logic Coq exercises or if you prefer in html. Complete this (you can skip the "Challenge problem") at home and send it to the teacher by mail by February 28.
• 27/2, 10:45--12:30 Lecture 5
  The Curry variant of Simple Type Theory: principal type algorithm.
  • Here are the slides of the lecture.
  • The first three pages of this document describe the principal type algorithm in detail.
  • See Sections 4.1-4.3 of Introduction to Type Theory.
  • Make the exercises.
• 27/2, 13:30-15:15 Lecture 6
  Polymorphic Types: ML style and full polymorphism
  • Here are the slides of the lecture.
  • See Section 5.1-5.5 of Introduction to Type Theory.
  • Make the exercises.
• 6/3, No Lecture because of Carnaval holiday.
• 13/3, 10:45--12:30 Lecture 7
  Higher order logic, Calculus of Constructions
  • Here are the slides of the lecture.
  • Make the exercises.
  • You can also make the exercises with Coq. Here is the Coq .v file.
• 13/3, 13:30-15:15 Lecture 8
  Inductive Types.
  • Here are the slides
  • Here are three files that have been shown at the lecture and you can load into Coq:
    • simple inductive examples from the lecture
    • coq_nat_base.v, and here is the html version.
  • Do the file coq_nat.v from the (only the final exercise if you want a challenge) and send your solutions to the teacher by mail by March 21. Here is the html version.
• 20/3, 10:45--12:30 Lecture 9
  More inductive types; Presentation of the Coq assignment.
  • Read slides on lists of the slides of last week on inductive types.
  • Do the files on lists coq_list_03.v up to coq_list_06.v from the zip file and send your solution to the teacher by mail by March 28.
  • More list programming.
  • The Coq file on head and tail of lists and the "option" type.
  • Here are the example files, showing how to do the first exercises on lists in Coq: coq_list_01.v and coq_list_02.v.
  • Do the exercises on trees coq_tree_03.v up to coq_tree_05.v from the zip file and send your solution to the teacher by mail by March 28.
  • Here is an example file, showing how to do the first exercise on trees in Coq. Look here for the htm-ized file and look here for the Coq source file.
  • Here is the presentation of the Coq assignment. Alternative suggestions for the Coq assignment can be found here .
• 20/3, 13:30-15:15 Lecture 10
  Programming with inductive types and dependent inductive types; Examples of cool and useful Coq features.
  
  • The slides on dependently typed programming.
  • Lots of examples of inductive types and their induction and recursion principles (thanks to Freek Wiedijk for the overview).
  • The Coq examples on dependently typed programming.
  • Inversion: slides and Coq file on inversion
  • Some automation and goodies: automation and nat_compare
• 27/3, 10:45--12:30 Lecture 11
  Some meta-theory of Type Systems (I): Church-Rosser property
  • Here are the slides of the lecture.
  • Here are the exercises for the lecture.
• 27/3, 13:30-15:15 Lecture 12
  Some meta-theory of Type Systems (II): Normalization
  • Here are the slides of the lecture.
  • See Sections 4.4 and 5.6 of Introduction to Type Theory.
  • Here are the exercises for the lecture.
• 3/4, 10:45--12:30 Lecture 13, as an exception in Atlas 10.330
  Work on Coq assignment
  • Here is a page where an earlier example assignment has been worked out. It has been created from a coq .v file .
  • We have used the "Proviola" system (by Carst Tankink) to produce this documented page.
• 3/4, 13:30-15:15 Lecture 14
  Recap of exercises and treatment of old exams and possibility to ask questions about the Coq assignment.
  • Here are some extra exercises relating to normalization and Church-Rosser.
  • The exam of July 2010.
  • Retake exam of 2015 .
  • Exam of 2019
  • The exam of April 2021.

Examination

• Final mark = (Written Exam mark + Coq Assignment mark)/2 with the condition that your Written Exam mark should be 5 or higher.
• You don't receive a mark (so I will write "NV") if you haven't completed all parts of the course.
• Deadline Coq Assignment: Sunday April 13
• In case your Written Exam mark is below 5, this is also your Final mark.
• Written exam Monday April 7, Time: 9:00--12:00
• The written exam will consist of questions comparable to the ones that were given during the lectures: see above for the pdf files.
• It is an open book exam, so you can bring any paper material you want
• Exam consultation that is: you can see your graded work, on Thursday April 24, 15:00- 16:00 in MF6.103.
• Older exams:
  • The exam of July 2010.
  • Here is the exam of 2008. (NB: the original version, which may still be at the Gewis website, contained a mistake; this is the corrected version.)

• Written exam: Monday June 23, 18:00-21:00.
• Coq assignment deadline: Tuesday June 24.

Coq Assignments

Deadline: Sunday April 13; do the assignment in couples deliver your assignment by mail to the teacher.

Here is a page about the of Coq assignment. (Look here for some additional comments regarding the use of lists.) To complete the Coq assignment follow these steps:

• Solve the assignment and write a report (more on that below).
• Deliver your solution (Report + separate Coq .v files) via mail.

A couple of remarks concerning the report:

• Do not make it too long. 15 pages is the absolute maximum but normally it should be much shorter. Keep in mind that longer does not mean better!
• What you should write:
  • Names and student numbers.
  • Explanation of the problem and your approach to it.
  • Description of the main definitions and the line of your proofs (e.g. sublemmas you used). If you had some alternative ideas to solve those problems describe them and explain your choice for the solution to this problem.
  • Write about your experience with the prover. What did you like, what you did not like etc.
  • Possibly add the Coq code as an appendix. (But note that you should deliver the Coq .v files separately anyway.)
• What you should not write
  • Do not unnecessarily repeat the code. Refer to appendix and quote the code only to illustrate something.
  • Do not write obvious things! Description of the proofs of the shape: "the goal is as follows so we apply this tactic and that is what we get..." are useless.