#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke

Type Theory Forall

English - October 16, 2023 12:10 - 1 hour - 79.5 MB - ★★★★★ - 6 ratings
Technology Science type theory programming languages academia Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed

Previous Episode: #33 Z3 and Lean, the Spiritual Journey - Leo de Moura

Next Episode: #35 Teika, Self-Education and F***ing Floating Points - Eduardo Rafael

Andrew Marmaduke is a PhD Candidate from the University of Iowa, he works
under Aaron Stump and has been working on revamping the theorem prover
Cedille 2. In this episode we tackle fundamental questions about the
foundations of the theorem provers, Cedille and Cedille 2.

Links

Andrew's Website
AndrasKovacs' Smalltt
Failure of Normalization in Impredicative Type Theory with
Proof-Irrelevant Propositional Equality
Impredicative Encodings of (Higher) Inductive Types