Skip to main content
To KTH's start page To KTH's start page

Loïc Pujet: Indexed inductive types in Observational Type Theory

Time: Wed 2023-06-21 10.00 - 12.00

Location: Albano house 1, floor 3, Room U (Kovalevsky)

Participating: Loïc Pujet, Stockholm University

Export to calendar


Observational Type Theory (OTT) was designed by Altenkirch, McBride and Swierstra to extend MLTT with function extensionality and the uniqueness of identity proofs, while preserving most of its computational properties. It can be thought of as a type theory for setoids with a proof-irrelevant equality, just like Cubical Type Theory is a type theory for fibrant cubical sets.

The aim of this talk is to present joint work with Nicolas Tabareau on implementing OTT in the Coq proof assistant. In particular, I will explain how we handle the full scheme of indexed inductive types of Coq, without breaking compatibility with the existing Coq syntax.