Logical Verification

Course Objective

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; (Knowledge and understanding) (Applying
knowledge and understanding)
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)
4. develop some practical skills that they can apply on a larger project
(as a hobby, for an MSc or PhD, or in the industry); (Applying knowledge
and understanding) (Lifelong 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) (Communication) (Lifelong learning skills)

Course Content

Proof assistants can be used to check the correctness of a 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.

Additional Information Teaching Methods

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

Method of Assessment

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, including the project, must be done
individually.

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

Literature

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

Additional Information Target Audience

MSc Computational Science
MSc Computer Science
MSc Computer Security

Recommended background knowledge

The main prerequisites for this course are an introductory course in
logic and familiarity with equational programming or functional
programming (e.g., Haskell, OCaml, Scala, Standard ML). Good command of
universal algebra can serve as a substitute for functional programming
for mathematically oriented students.