Home > News > Philipp Haselwarter: Extensional type theories for proof assistants

Philipp Haselwarter: Extensional type theories for proof assistants

Date: 2. 10. 2017
Source: Mathematics and theoretical computing seminar
Torek, 3. 10. 2017, od 12h do 14h, Plemljev seminar, Jadranska 19

Abstract: We present Martin-Löf's type theory with equality reflection and discuss some of the difficulties that arise when we want to implement it in a proof assistant. We then present equivalent formulations of type theory that have better meta-theoretical behaviour and thereby attempt to remedy some of these problems.

This is joint work with Andrej Bauer, and work in progress.