Bring your computer
Bas Spitters
We will be using the discussion board on brightspace for general discussions about the exercises, projects, and Coq.
During this course we will be using the Coq proof
assistant.
Coq is both a functional programming language, as well as a system that allows
one to reason using formal proofs about one's programs.
The easiest installation uses docker and vscode.
Alternatively, information on installing Coq is
available here. We use version 2022.04.1 of Coq Platform for 8.15.2.
Choose an IDE. I recommend either vscode or emacs.
One can read logical foundations in the browser using jscoq and even use it for collaborative editing. This is still experimental though.
We will be using part of the online textbook Software Foundations by Benjamin C. Pierce et al.
The course includes a track of weekly exercises.
Submission and approval of 10 mandatory assignments is required.
Five assignments from the first seven weeks and five from the second.
Work in groups of two (maximally three) is encouraged.
The exercises should be handed in each Wednesday before 9:00..
Please come prepared to the QA meetings so you can ask questions in person.
Coq should accept the homework handed in as a .v file in its entirety. The exercise will not be graded if Coq does not accept the file. Use Admitted to make Coq accept incomplete proofs.
You are not allowed to use Coq tactics in the homework that we have not yet discussed (for example tauto, eauto and lia are forbidden).Date  Topics  Course material 

week 35  Installing Coq Basic inductive types Proving using computation Rewriting 
Preface
and Basics
and Induction 
week 36  Lists and Polymorphic functions  Lists
and
Polymorphic functions

week 37  Tactics and Logic  Tactics
and
Logic

Week 38  Inductively defined propositions  IndProp

Week 39  ProofObjects, IndPrinciples 
Maps,
ProofObjects,
Rel,
IndPrinciples

Week 40  Imp  Imp

Week 41  Auto  Auto, AltAuto

Week 43  SmallStep  SmallStep,
Types

Week 44  Simple Type Theory  Stlc,
StlcProp

Week 45  Type Checking  More Stlc,
TypeChecking

Week 46  Programming with Dependent types  Lecture (Coq file),
Equations
manual, Equations
introduction,
Slides,
Exercises

Week 47  Type Classes  
Week 48  Monads  Lecture, Exercises

Week 49  QuickChick 
The course finishes with a Coq project, a list of suggestions can be found here and here. You may also invent a Coq project yourself or do a variation or extension of one of our suggested projects. If you invent a project yourself or use a variation of the suggestions, you have to discuss it with the lecturer.
You are allowed to work in groups. You may also write the report together. However, you are fully responsible for the code and the report. The oral exam will test your understanding.
In order to complete the Coq project, you have to make the following deliverables:
The written report has to be 5 to 10 pages, should be in academic style, and should include:
You should not include unnecessarily long excerpts of Coq code, just use small fragments to illustrate a point. Informal proofs should be formulated in the way taught during the course. Do not paraphrase Coq proofs in natural language by writing: and now we apply tactic X so our goals becomes Y.
Grade reflects an overall assessment of:
Only students with approved exercises can attend the oral exam and thus pass the course.
The grade of the Coq project is based on the following items:
During the oral exam we will test your understanding of the
project. E.g. by asking you to create a small
extension of the project, to explain proofs of the project in an
informal way, to query you about the contents of your report, or ask general
questions about the contents of the course.
Bring your laptop!