Module Number

INFO-4248 		Module Title

Interactive Theorem Proving 		Lecture Type(s)

Lecture
ECTS 9
Work load
- Contact time
- Self study
Workload:
270 h
Class time:
90 h / 6 SWS
Self study:
180 h
Duration 1 Semester
Frequency Irregular
Language of instruction German and English
Type of Exam

Written or oral examination. Participation in exercises is required for exam participation.
Content

This course is an introduction to interactive theorem programming and advanced functional programming, mostly using the Coq proof assistant.
This course is for students interested in:
1. The foundational theories of mathematics, most notably type theory and logic
2. Practical interactive theorem proving in a state-of-the-art proof assistant
3. Advanced functional programming languages and their relation to constructive mathematics via the “Curry-Howard Isomorphism”
4. Program verification and “certified programming”
5. Programming Language Semantics
Objectives

Students will be able to write programs and prove theorems in the Coq proof assistant.
Students understand the theoretical underpinnings of interactive theorem
provers and get basic insights into the semantics and formal properties of
programming languages.
Allocation of credits / grading
Type of Class
Status
SWS
Credits
Type of Exam
Exam duration
Evaluation
Calculation
of Module (%)
Prerequisite for participation There are no specific prerequisites.
Lecturer / Other Ostermann
Literature

Volume 1 and 2 of the “Software Foundations” series available at https://
softwarefoundations.cis.upenn.edu/.
A. Chlipala, Certified Programming with Dependent Types, MIT Press / A background in functional programming is helpful. Experience with mathematical
proofs is helpful.
Last offered unknown
Planned for currently not planned
Assigned Study Areas INFO-INFO, INFO-PRAK, INFO-THEO, MEDI-APPL, MEDI-INFO, ML-CS