[HoTT] February 23: Loïc Pujet, Observational Type Theory meets CIC

[HoTT] February 23: Loïc Pujet, Observational Type Theory meets CIC

['EMILY RIEHL' via Homotopy Type Theory]

[-- Attachment #1: Type: text/plain, Size: 2323 bytes --]

The HoTTEST seminar continues this Thursday at the usual time, 11:30am EST = 16:30 UTC.

Our speaker is  Loïc Pujet, who's talk is titled "Observational Type Theory meets CIC".  The talk will be 60 minutes long, followed by
up to 30 minutes for questions.  The abstract is below.

The Zoom link is https://zoom.us/j/994874377

Further information, including the list of upcoming speakers, and videos and slides from past talks, is at:

https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

Emily

(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen,
Chris Kapulkin, and Emily Riehl.)

--

Observational Type Theory (OTT) extends dependent type theory with an equality that satisfies extensionality principles for functions and propositions, as well as quotient types. But unlike HoTT, the equality of OTT is a proposition that does not contain any higher structure. Thus, if HoTT is the language of infinity-groupoids, OTT is the language of propositions and sets.

In this talk I will go over the integration of OTT with the Calculus of Inductive Constructions—the theory of Coq—which supports both impredicative propositions and a large class of inductive types.

In order to obtain strong theoretical guarantees on our theory, I will explain how to build several models for OTT: one the one hand, models in set theory to establish consistency; and on the other hand, reducibility models to establish normalization, a type-checking algorithm, and bounds on its proof-theoretic strength.

Finally, I will discuss the use of OTT as an internal language for Grothendieck toposes and the principle of unique choice.This presentation is based on joint work with Nicolas Tabareau.

Most of the results that I will present have been formalized in Agda and Coq.


Professor of Mathematics (she/her)
Johns Hopkins University
emilyriehl.github.io


-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/DS7PR01MB77586E3980E74CA744BE8E74C8AA9%40DS7PR01MB7758.prod.exchangelabs.com.

[-- Attachment #2: Type: text/html, Size: 5888 bytes --]