Bring your computer
Lecturer
Bas Spitters
Contact
We will be using the discussion board on brightspace for general discussions
about the exercises, projects, and Coq.
Links
Course material
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.
Information on installing Coq is
available here. I recommend a recent version of Coq (8.13) and Coq Platform, especially on windows.
Choose an IDE. I recommend either vscode or emacs.
One can read logical foundations in the browser and use jscoq 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.
Homework
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 Friday following the TA session before 10:00.
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 omega
are forbidden).
Preliminary schedule
Monday 9:00-11:00 5427-140: Feedback and Lecture
Thursday 9:00-10:00 5427-140: Questions about homework
| 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,
Equations
manual, Equations
introduction,
Slides
|
| Week 47 |
Type Classes
|
| Week 48 |
Monads
| v-file, Exercises
|
| Week 49 |
QuickChick
|
Coq project
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:
- Register the choice of your final project on brightspace.
This deliverable is due on
Fri 5 November 2021.
Make sure you have discussed your choice before that time with the
lecturer. Especially, when you are proposing a project of your own design.
- A set of Coq .v files containing the solution
to your project and a corresponding written report.
This deliverable is due on
Thu 6 Jan 2022.
The written report has to be 5 to 10 pages, should be in academic style,
and should include:
- Name and student number.
- A small introduction with at least a description of the project you have
chosen. You should not just copy the description from the projects file.
- A description of the problems you have encountered during the project and
how you have solved these.
If you had multiple solutions in mind, describe these, and explain why you
have picked the one you have used.
- A conclusion with at least your experience using Coq: what did you like
and what you did not like.
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.
Grading
Grade reflects an overall assessment of:
- group project
- individual oral examination
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:
- Correctness: whether the Coq definitions and lemmas
correctly model the problem.
- Completeness: whether all lemmas are proven (e.g. no
lemmas omitted and proofs finished with admit
or Admitted).
- Style: whether the Coq code follows the style
guidelines (e.g. use of Case tactic,
sensible variable names and use of implicit arguments).
- Effectiveness: whether the definitions and proofs are
given in an effective way (e.g. no useless proof steps and
the induction tactic not used blindly).
- Report: style, presentation, language and
correctness of the report.
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!