Q1 2015-2016, Tuesday 14:00-17:00, Location: ny184 (5335-184).
Bring your computer
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
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
|Preface and Basics
|1 September||Induction on natural numbers
Proofs within proofs
Formal vs. informal proofs
|8 September||More inductive types (products, lists and options)
Induction on lists
Polymorphic inductive types
Poly (Section 'Polymorphism')
Partial application and currying
Additional Coq tactics (apply, symmetry and inversion)
Varying the induction hypothesis
|Poly and MoreCoq
|22 September||Curry Howard correspondence
Inductively defined propositions
Induction over evidence
Inversion over evidence
|Logic and Prop (up to, but not including 'Relations')
Optional: constructive logic, additional exercises and
|29 September||Semantics as a function
Semantics as a relation
|Imp (we are using a modified version,
which can be obtained here)
|6 October||Introduction of the 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.