Introduction to Functional Programming (dIFP)

Q1 2015-2016, Tuesday 14:00-17:00, Location: ny184 (5335-184).
Bring your computer


Robbert Krebbers
Email: robbert AT cs DOT au DOT dk
Office: Turing 213

Teaching assistants

Kristoffer Just Andersen
Email: kja AT cs DOT au DOT dk
Office: Turing 217

Kent Grigo
Email: kentg AT cs DOT au DOT dk
Office: Turing 214


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.

We will be using part of the online textbook Software Foundations by Benjamin C. Pierce et al. It is freely available on the web.


The course includes a track of weekly mandatory exercises. The exercises should be handed in each Friday before 23:59 following the lecture.

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.

The homework will be graded on the scale [inadequate, fair, good]. We will give comments following the grading rules for the term project as listed below. 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).

Coq project

The course finishes with a Coq project, a list of suggestions can be found 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.

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:

  1. Name and student number.
  2. 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.
  3. 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.
  4. 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.


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:

  1. Correctness: whether the Coq definitions and lemmas correctly model the problem.
  2. Completeness: whether all lemmas are proven (e.g. no lemmas omitted and proofs finished with admit or Admitted).
  3. Style: whether the Coq code follows the style guidelines (e.g. use of Case tactic, sensible variable names and use of implicit arguments).
  4. 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).
  5. Report: style, presentation, language and correctness of the report.

During the oral exam we will test whether you are able to create a small extension of the project, ask you to explain proofs of the project in an informal way, query you about the contents of your report, and ask general questions about the contents of the course.

Preliminary schedule

DateTopics Course material and homework
25 August Installing Coq
Basic inductive types
Proving using computation
Preface and Basics
Optional: andb_eq_orb, binary and decreasing
1 September Induction on natural numbers
Proofs within proofs
Formal vs. informal proofs
Optional: evenb_n__oddb_Sn, plus_swap', binary_commute and binary_inverse
8 September More inductive types (products, lists and options)
Induction on lists
Polymorphic inductive types
Lists and Poly (Section 'Polymorphism')
Optional: bag_count_sum, dictionary_invariant1 and dictionary_invariant2
15 September Higher-order functions
Partial application and currying
Anonymous functions
Additional Coq tactics (apply, symmetry and inversion)
Varying the induction hypothesis
Poly and MoreCoq
Optional: church_numerals
22 September Curry Howard correspondence
Propositional logic
Inductively defined propositions
Induction over evidence
Inversion over evidence
Existential quantification
Logic and Prop (up to, but not including 'Relations')
Optional: constructive logic, additional exercises and palindrome_converse
29 September Semantics as a function
Coq automation
Semantics as a relation
Imp (we are using a modified version, which can be obtained here)
Optional: optimizer, no_whiles_terminating and additional exercises
6 October Introduction of the Coq projects
Coq projects
Choose a Coq project
9 October Registration Coq project due before 23:59
13 October Question session Coq project
21 October Coq project due before 23:59
26-28 October Oral exams


The first-year course on programming languages in general and its lecture notes in particular.