Logical Verification

Doel vak

The course introduces interactive theorem proving via the proof assistant Lean. We study its logical foundations and its applications to

computer science and mathematics. The course's goals are that the students:

1. learn fundamental theory and techniques in interactive theorem proving; (Knowledge and understanding)

2. learn how to use logic as a precise language for modeling systems and stating properties about them; (Applying knowledge and understanding) (Making judgements)

3. familiarize themselves with selected areas in which proof assistants are successfully applied, such as functional programming, the semantics

of programming languages, and mathematics; (Knowledge and understanding) (Applying knowledge and understanding)

4. develop some practical skills which they can apply on a larger project (as a hobby, for an MSc or PhD, or in industry); (Applying knowledge and understanding) (Learning skills)

5. get to understand the domain well enough to start reading relevant scientific papers published at international conferences such as CPP and

ITP or in the Journal of Automated Reasoning. (Applying knowledge and understanding) (Learning skills) (Communication skills)

Inhoud vak

Proof assistants can be used to check the correctness of the specification of a program or the proof of a mathematical theorem. The course is built around the proof assistant Lean, a system that is developed primarily at Microsoft Research. In the practical work, we learn to use Lean version 3. We use the system to prove mathematical theorems in a precise, formal way, and see how to verify small programs.

The course consists of four parts. Part I introduces the notions of propositions and proofs. Part II is about functional programming (datatypes and recursive functions) and logic programming (Prolog-style predicates). Part III explains how to apply what we have learned to specify and reason about the semantics of imperative programming languages, reviewing the three main types of semantics (operational, axiomatic, and denotational). Finally, Part IV focuses on basic mathematical applications of proof assistants, culminating with the construction of the real numbers in Lean and a guest lecture.

Aanvullende informatie onderwijsvormen

2 times 2 hours theory class, 2 times 2 hours practical work.

Toetsvorm

The written exam counts for 75%, and the Lean assignments count for 25% of the final mark. There are 10 Lean assignments to do out of a set of 11 possibilities. Two of the assignments can be replaced by a student project. The assignments must be done individually.

All students may take the final exam and the resit exam. If both exams are taken, the score at the resit is the one that counts.

Literatuur

The course notes "The Hitchhiker's Guide to Logical Verification", by Baanen, Bentkamp, Blanchette, Hölzl, and Limperg, available as a PDF on

the course's web site.

Aanvullende informatie doelgroep

MSc Computer Science

Aanbevolen voorkennis

The main prerequisites for this course are an introduction course in logic and familiarity with equational programming or functional

programming (e.g., Haskell, OCaml, Scala, Standard ML). A good command of universal algebra can serve as a substitute for functional

programming for mathematically-oriented students.