Proving with Computer Assistance 2IMF15
Teacher
Herman Geuvers:
- 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
The course will be given live on
- Thursdays, 10:45-12:30 in Metaforum 06 (with exceptions, see below) and 13:30-15:15 in Atlas 2.225
Prerequisites
We assume that you are familiar with a bit of logic, especially natural deduction and preferably (untyped) lambda calculus.
- 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 Rocq Proof Assistant (renamed from "Coq" since version 9.0): you may find one of the following useful:
System we will use
We will be using the Proof Assistant Rocq in this course. (The Rocq system was renamed from "Coq" since verion 9.0, so from now on I will use the new name. Old urls from the Rocq team at INRIA using the name "Coq" should redirect to the new website. I will use Rocq everywhere in the course material where it used to say "Coq". In case you find omissions, please let me know.)
- You have to download and install Rocq yourself.
- Throughout the course we will be showing a number of Rocq files and
for some you will need to fill in the proofs yourself as an
exercise. Your assignment is a formalization in Rocq.
Some useful links
The course by week
The course will not be recorded. Recordings of a previous year are
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, Rocq.
Short recapitulation of
lambda calculus.
- 13/2, 13:30--15:15 Lecture 2
Simple Type theory and
"Formulas-as-Types" for propositional logic.
- 20/2, 10:45-12:30 Lecture 3
Dependent Type Theory.
- 20/2, 13:30-15:15 Lecture 4
Natural Deduction in
Rocq: proposition logic and predicate logic.
Be sure to have Rocq 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 Rocq 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.
- Here is the proposition_logic file with
some answers filled in. Or if you prefer in html .
- Predicate logic: Here is a file with
the predicate logic Rocq
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.
- Here is the predicate logic file with
some answers filled in, also
of the "Challenge problem". Or if you prefer in html.
- 27/2, 10:45--12:30 Lecture 5
The Curry variant of Simple Type Theory:
principal type algorithm.
- 27/2, 13:30-15:15 Lecture 6
Polymorphic Types: ML style and full polymorphism
- 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.
- Here are some answers to the exercises.
- For some more handwritten answers to exercises showing how to find these terms and derivations, see Canvas.
- You can also make the exercises with Rocq. Here is the Rocq .v file.Here is the html version.
- Here is a Rocq .v file with answers. Here is the html version.
- 13/3, 13:30-15:15 Lecture 8
Inductive Types.
- Here are
the
slides
- Here are two files that have been shown at the lecture and you
can load into Rocq:
- Finish the file nat_ex.v
(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.
Here is the worked out file:
nat_ex_answers.v, or in the html version.
- Finish the file list_ex.v and send
your solutions to the teacher by mail by March 21. Here is the html version.
Here is the worked out file:
list_ex_answers.v, or in the html version.
- 20/3, 10:45--12:30 Lecture 9
More inductive types; Presentation of the Rocq assignment.
- More list programming and the option type: list and option. Here is the html version. Send your solution to the
teacher by mail by March 28.
- Do the exercises on trees from the tree_ex file. Here is the html version. Send your solution to the
teacher by mail by March 28.
- Here is the presentation of the Rocq assignment. Alternative suggestions for the Rocq assignment can be found here .
- 20/3, 13:30-15:15 Lecture 10
Programming with dependent inductive types; Examples of useful Rocq features.
- 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
- 3/4, 10:45--12:30 Lecture 13, as an exception in Atlas 10.330
Work on Rocq 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 Rocq assignment.
Examination
The mark for the course is determined by the 2
marks you will get for the two items listed below.
- Final mark = (Written Exam mark + Rocq 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 Rocq 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.)
For the retake exam ("Hertentamen"), all guidelines above apply with the following dates/deadlines:
- Written exam: Monday June 23, 18:00-21:00.
- Rocq assignment deadline: Tuesday June 24.
NB. You can choose to only retake one part of the exam, so only the Written exam, or only the Rocq assignment. In any case: register for the retake!
Rocq 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 Rocq
assignment. (Look here
for some additional comments regarding the use of lists.) To complete
the Rocq assignment follow these steps:
- Solve the assignment and write a report (more on that below).
- Deliver your solution (Report + separate Rocq .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 Rocq code as an appendix. (But note that
you should deliver the Rocq .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.
herman at cs dot ru dot nl