Q1 20152016, Tuesday 14:0017:00, Location: ny184 (5335184).
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 
Higherorder 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  
2628 October  Oral exams 
The firstyear course on programming languages in general and its lecture notes in particular.