Logical Verification

2018-2019
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
concerned with the proof assistant Lean, a system that is developed
primarily at Microsoft Research. In the practical work, we learn to use
Lean. We will see how to use the system to prove mathematical theorems
in a precise, formal way, and how to verify small functional programs
(e.g., a sorting algorithm). In the course, we focus on its 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 systems, including Agda, Coq,
and Matita.

Onderwijsvorm

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

Toetsvorm

Written exam,
obligatory Lean exercises,
obligatory hand-in theory exercises,
possibly presentations of papers.

Vereiste voorkennis

An introduction course in logic.

Literatuur

Course notes with some recent papers as addition.

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 dr. J. Hölzl
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: