Logical Verification

2019-2020
Dit vak wordt in het Engels aangeboden. Omschrijvingen kunnen daardoor mogelijk alleen in het Engels worden weergegeven.

Doel vak

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

Inhoud vak

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.

Onderwijsvorm

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.

Vereiste voorkennis

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

Literatuur

Course notes

Doelgroep

mCS, mAI, mMath, mPDCS

Algemene informatie

Vakcode X_400115
Studiepunten 6 EC
Periode P2
Vakniveau 500
Onderwijstaal Engels
Faculteit Faculteit der Bètawetenschappen
Vakcoördinator dr. J.C. Blanchette
Examinator dr. J.C. Blanchette
Docenten A. Bentkamp
dr. J.C. Blanchette

Praktische informatie

Voor dit vak moet je zelf intekenen.

Voor dit vak kun je last-minute intekenen.

Werkvormen Hoorcollege, Practicum
Doelgroepen

Dit vak is ook toegankelijk als: