News
|
28.05.2018
|
GradesHi all, grades are entered into the system now. Your points do not really matter, we just needed to enter some to get the grades. If you want feedback, feel free to contact your advisor. Best regards Your ACP team |
|
25.04.2018
|
Evaluation resultsThe results of the evaluation are now available under Materials. Thank you very much for your feedback! |
|
27.03.2018
|
Registration for projectIf you want to do a project in this course (required to take the course for credit), please sign up for the project on you personal status page as soon as possible. |
|
14.03.2018
|
Exercise submission and talk on FridayDear all, you can now submit the solutions for the warm-up exercises on your personal status page in order to receive feedback. Submission is open until Monday, 09:59. The exercises are meant as warm-up, which means that if you find something difficult, you... Read more Dear all, you can now submit the solutions for the warm-up exercises on your personal status page in order to receive feedback. Submission is open until Monday, 09:59. The exercises are meant as warm-up, which means that if you find something difficult, you should come to the office hour or ask in the forum. It's not time to spend hours on hard problems (yet)! Also, please don't forget that lectures start on Monday, March 19th, 10:00 in Rm 528 in E1 3. This Friday, March 16th, Sarah Mameche will give the first talk of her Bachelor seminar phase titled "Autosubst: Automation for de Bruijn Substitutions in Lean" at 14:15 in Rm 528. If you're interested in the research that's happening in our group, you're cordially invited to attend. The talk will last 15 minutes plus discussion, which means we should be done by 15:00. We're looking forward to the start of the course! Your ACP team |
|
06.03.2018
|
Warm-up phaseDear all, the lecture phase of the course starts in less than two weeks, and we are all really excited! In order to use the 9 days of lectures as efficiently as possible, we would like you to warm-up in the week before the lectures, i.e. from March 12th to... Read more Dear all, the lecture phase of the course starts in less than two weeks, and we are all really excited! In order to use the 9 days of lectures as efficiently as possible, we would like you to warm-up in the week before the lectures, i.e. from March 12th to March 16th. In the warm-up phase you...
We're all looking forward to the next weeks! Best, your ACP Team |
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
- Type classes, canonical structures
- Setoid rewriting
- ssreflect and mathcomp
- Coinduction and coinductive definitions
- Implementation of Coq
Additionally, we will have tutorials on some Coq tools and libraries.
The first lecture is on March 19th, the last lecture on March 29th.
Second Phase
The second part of the course is a project phase of 5 weeks, lasting until May 4th. Students work on their own on an interesting formalisation 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 formalisation may improve the grade.
Presentation
In the second week of May, students will give a short, 5-10 minute presentation on their project. The presentation should give an overview of the formalisation 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.