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
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.
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).
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:
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:
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.
Date | Topics | Course material and homework |
---|---|---|
25 August | Installing Coq Basic inductive types Proving using computation Rewriting |
Preface and Basics Optional: andb_eq_orb , binary and
decreasing |
1 September | Induction on natural numbers Proofs within proofs Formal vs. informal proofs |
Induction 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 Optimization Coq automation Semantics as a relation State |
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 Recap |
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.