General Information
| Course Code | XM_0167 |
|---|---|
| Credits | 6 EC |
| Period | P2 |
| Course Level | 400 |
| Language of Tuition | English |
| Faculty | Faculty of Science |
| Course Coordinator | dr. K. Sojakova |
| Examiner | dr. K. Sojakova |
| Teaching Staff |
dr. K. Sojakova |
|
Part of programme(s)
Use the arrow keys to navigate the list, Enter to select, and Escape to close.
|
|
Practical Information
You need to register for this course yourself. The (de)registration deadlines can be found on VU.nl
Late placement is not possible for this course.
| Teaching Methods | Seminar, Lecture |
|---|
Target audiences
This course is also available as:
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; (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)
Course Content
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.
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 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.
Literature
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.
Additional Information Target Audience
MSc Computer Science
Recommended background knowledge
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.