Responsible Instructor 

Contact Hours / Week x/x/x/x 
0/0/0/6

Education Period 

Start Education 

Exam Period 

Course Language 

Course Contents 
How can we ensure that software cannot crash and is guaranteed to be correct? In this course we tackle this question by viewing programs and programming languages as mathematical objects. That way we can use logic to prove properties about programs and thereby guarantee that software is correct. To make reasoning about actual programs and programming languages feasible, we will not be doing these proofs by hand, but instead use a tool called a proof assistant to build proofs that can be checked by a computer. The proof assistant that we will be using is called Coq. As we will show during this course, proof assistants turn doing proofs and logic into programming.
This course assumes familiarity with functional programming and elementary logic.
This course is a specialization course for programming languages and software engineering

Study Goals 
After this course students will be able to:
 State and prove properties of functional programs in logic.  Specify the semantics of an (imperative) programming language in logic.  State and prove the correctness of program transformations.  Use Hoare logic to prove properties of imperative programs.  Use the Coq proof assistant to specify and prove correct a nontrivial program.

Education Method 
This course consists of a weekly lecture of 2 hours and a lab session of 4 hours. During the lab sessions students will work on proving simple theorems. Towards the end of the course students will carry out research projects that apply the ideas of the course.

Literature and Study Materials 
Main course material:
Software Foundations Benjamin C. Pierce et al. Freely available online at http://www.cis.upenn.edu/~bcpierce/sf/current/
Supplementary material:
Types and Programming Languages Benjamin C. Pierce MIT Press ISBN 0262162091

Assessment 
The final grade consists of the following parts:
 A programming project in the Coq proof assistant.  A written exam
Both have weight 50% and both should be 5.8 or higher. The weighted average should be 5.8 or higher. There is an oral resit for the written exam.
The research project and homework should be done individually.

Coinstructor 
