Saarland University Computer Science


Advanced Coq Programming Prof. Gert Smolka, Yannick Forster, Fabian Kunze

Advanced Course, 6 credit points, Summer Semester 2020

Registration for this course is open until Friday, 09.10.2020 23:59.

News

15.07.2020

New dates: October 12 - October 23rd

Dear students,

we have fixed new dates for the lecture: October 12th - October 23rd.

Your ACP team

12.03.2020

Postponement of ACP

Dear students,

as a general measure to contain the spreading of the Corona virus and in line with recent actions by the university we decided to postpone the lecture indefinitely for now. Most likely we will reschedule for the next semester break in... Read more

Dear students,

as a general measure to contain the spreading of the Corona virus and in line with recent actions by the university we decided to postpone the lecture indefinitely for now. Most likely we will reschedule for the next semester break in September/October after consultation with you on which dates work best.

We're still very much looking forward to the lecture!

Your ACP team

28.02.2020

Dates Block Phase

The block phase will be from the 16th of March to the 27th of March.
So there is one week between the end of the block phase and the start of the other lectures in the new semester.

31.01.2020

Information Meeting

There will be an information meeting fixing the dates of the block lecture on Thursday, February 6th in Rm 528 at 16:15 in building E1 3. We will also talk about expectations you have on the course, planned topics, and the format of the course. If you are interested... Read more

There will be an information meeting fixing the dates of the block lecture on Thursday, February 6th in Rm 528 at 16:15 in building E1 3. We will also talk about expectations you have on the course, planned topics, and the format of the course. If you are interested to join but can't make it send us an email.


 

 

Advanced Coq Programming

All information on this website is preliminary and subject to change.

This advanced course is a practical, "hands-on" course on the Coq proof assistant.

First phase

The first part is a block course, with lectures in the morning and tutorials or office hours in the afternoon. Attendance in lectures is expected.

We plan to cover (a subset of) the following topics in the lectures:

  • Advanced automation: Tactics, Hints and Ltac
  • Dependent and nested inductive types
  • Type classes
  • Setoid rewriting
  • ssreflect and mathcomp
  • Foundations and Implementation of Coq
  • Useful Coq plugins, projects, and libraries
    • Autosubst
    • CertiCoq
    • CoqHammer
    • Equations
    • Extraction
    • Iris
    • MetaCoq
    • Mtac 2
    • Program Package
    • QuickChick
    • ...

The first lecture is on October 12th, the last lecture on October 23rd.

Second Phase

The second part of the course is a project phase of 5 weeks, lasting until TBA. Students work on their own on an interesting mechanisation topic with an advisor. We have a list of interesting topics, but are open to suggestions. Credit and grades will be based on the project. We do not expect a mathematical writeup. However, a well-documented and well-readable mechanisation may improve the grade.

Presentation

In the TBA, students will give a short, 5-10 minute presentation on their project. The presentation should give an overview of the mechanisation and point out the most interesting details.

Participation Requirements

We require familiarity with the proof assistant Coq. Students who have not taken a Coq-related lecture (Introduction to Computational Logic, Semantics, Computational Logic 2 or a similar course at another university) may have to prove their familiarity in order to participate.