Introduction to Functional Programming

Bring your computer

Teacher

Bas Spitters

Teaching assistant

Andreas Lynge

Contact

We will be using the discussion board on Blackboard for general discussions about the exercises, projects, and Coq. Your posts are anonymized, so do not feel hesitant against using it.

Course material

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. Information on installing Coq is available here. The Windows installer is available here, but using WSL seems to work better..

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 mandatory exercises. The exercises should be handed in each Monday following the lecture before 9: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

Tuesday 8:00-9:00: TA-session
Thursday 12:00-14:00: Lectures

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
Week 43	lambda-calculus and combinators	Notes
Week 44	Simple type theory and System F	Notes, Slides
Week 45	Programming with Dependent types (guest lecture by Matthieu Sozeau)	Equations manual, Equations introduction Other material
Week 46	F-omega and Calculus of Constructions	Notes, Slides, More Slides
Week 47	Monads	v-file, Exercises
Week 48	Type Classes
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 teacher.

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 blackboard. This deliverable is due on Wed 4 December 2019. 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 Sat 21 Dec 2019.

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

The grade of the course is computed as follows:

([grade of the Coq project] + [grade of the oral exam]) / 2.

Both grades have to be at least 02 (adequate).

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!