Masterpraktikum: Software Foundations
- Lecturer
- Prof. Dr. Peter Thiemann
- Time and Place
- Wed. 14:00 – 16:00, Geb 79 SR 00-019
- Assistant
- Luminous Fennell
Kick-Off Meeting
Wed. 2012-10-24 at 14:00, SR 079-00-019 (Building 79,
upstairs, on the right-hand side).
The room is reserved, so please send a mail to Luminous Fennell as
soon as possible if there are problems with this date.
Dates
| Date | |
|---|---|
| 2012-10-24 14:00 | Kick-Off Meeting |
Chapters
Auxiliary Material
| AutomationIntro.v | Short intro to Coq automation and Ltac |
Graded Exercises
| Sheet | Distribution | Submission |
|---|---|---|
| SfLib.v | ||
| ImpUtils.v | ||
| ImpFUtils.v | ||
| Sheet1.v | 2012-11-14 | 2012-11-30, 23:59 |
| Sheet2.v | 2012-12-12 | 2013-01-06, 23:59 |
| Sheet3.v | 2013-01-16 | 2013-01-31, 23:59 |
| Sheet4.v | 2013-02-13 | 2013-03-06, 23:59 |
Description
The purpose of this Praktikum is to introduce the participants to interactive theorem proving with the Coq proof assistant. The participants will work on selected chapters from the self-study course Software Foundations of Benjamin Pierce et al. There will be periodical lab-sessions where questions, exercises and specific topics will be discussed in detail.
Covered Topics
- Basic acquaintance with the Coq proof assistant and its underlying theory
- Stating and proving formal mathematical theorems in Coq
- Proof automation/proof search
- Formalization of simple programming languages (i.e. precise definition of their behavior and proofs of their important properties)
- Implementation of certified functional programs (i.e. programs that are correct by construction)
Grading
There will be four graded exercises throughout the semester, each of which counts 25% for the final grade.
Requirements
As all concepts needed for the course and the exercises will be introduced, no specific previous knowledge of the topic is required. However, participants should have taken some basic logic (or logic-related) course in the past (as is mandatory in e.g. Bachelor's degree program here in Freiburg), and should have some interest in logic, formal methods, programming languages or related topics.
The required software should be installable on all major operating systems. Also, a VM image will be provided and there is the possibility to use the Proglang-Pool (079-00-018) for participants without a laptop.