Logical Verification

2019-2020

Course Objective

Introduction to the proof assistant Lean, its type-theoretic
foundations, and its applications to mathematics and computer science

Course Content

A proof assistant is used to check the correctness of a specification of
a program or the proof of a mathematical theorem. The course is build
around the proof assistant Lean, a system that is developed primarily at
Microsoft Research. In the practical work, we learn to use Lean. We use
the system to prove mathematical theorems in a precise, formal way, and
how to verify small programs. In the lectures, we focus on Lean's
dependent type theory and on the Curry-Howard-De Bruijn correspondence
between proofs and functional programs (lambda-terms). These concepts
are the basis of Lean but also of other popular proof assistants,
including Agda, Coq, and Matita.

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.

Entry Requirements

An introduction course in logic and some familiarity with
equational/functional programming (or universal algebra for
mathematicians).

Literature

Course notes

Target Audience

mCS, mAI, mMath, mPDCS

General Information

Course Code X_400115
Credits 6 EC
Period P2
Course Level 500
Language of Tuition English
Faculty Faculty of Science
Course Coordinator dr. J.C. Blanchette
Examiner dr. J.C. Blanchette
Teaching Staff A. Bentkamp
dr. J.C. Blanchette

Practical Information

You need to register for this course yourself

Last-minute registration is available for this course.

Teaching Methods Lecture, Practical
Target audiences

This course is also available as: