Philipp Haselwarter: Extensional type theories for proof assistants

Datum objave: 2. 10. 2017
Seminar za temelje matematike in teoretično računalništvo
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.