Every proof assistant: redtt
This week the speaker will be Jon Sterling, and we are getting two proof assistants for the price of one!
redttand the future of Cartesian cubical type theory
Time: Thursday, June 4, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Jon Sterling (Carnegie Mellon University)
Proof assistant: redtt and cooltt
redttis an interactive proof assistant for Cartesian cubical type theory, a version of Martin-Löf type theory featuring computational versions of function extensionality, higher inductive types, and univalence. Building on ideas from Epigram, Agda, and Idris,
redttintroduces a new cubical take on interactive proof development with holes. We will first introduce the basics of cubical type theory and then dive into an interactive demonstration of
redtt’s features and its mathematical library.
After this we will catch a first public glimpse of the future of
redtt, a new prototype that our team is building currently code-named “
coolttintroduces syntax to split on disjunctions of cofibrations in arbitrary positions, implementing the full definitional eta law for disjunction. While
coolttis still in the early stages, it already has full support for univalence and cubical interactive proof development.
The video recording of the talk.