#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke

Type Theory Forall
16/10/2023 1h 28min
#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke

Listen "#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke"

Descargar episodio Ver en sitio original

Episode Synopsis



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.
If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall
Links

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



More episodes of the podcast Type Theory Forall

#58 Constructivism and Computational Content - Andrej Bauer 16/12/2025
#57 Compilers for Privacy-Preserving Computation, Category Theory, and Keeping a Good Rythm in your PhD - Raghav Malik 06/12/2025
#56 Property Based Testing and PL Grad School Applications - Francille Zhuang 17/11/2025
#55 The Death of OO, The Beauty of Scheme, BobKonf, and FunArch - Mike Sperber 27/10/2025
#54 The Goal of Science is to Communicate Ideas! - Philip Wadler 29/09/2025
#53 RustBelt, Iris, and the Art of Writing - Derek Dreyer 27/08/2025
#52 Why is Haskell so special - Lennart Augustsson 10/07/2025
#51 s/Coq/Rocq - Nicolas Tabareau 04/06/2025
#50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra 14/05/2025
#49 Self-Education in PL - Ryan Brewer 14/03/2025
© 2003-2026 ZARZA | AHEAD OF OUR TIME
privacy policy
In God we trust In God we trust
PreSales Questions? Click Here
or call our toll-free line at +1-888-5002068 Miami, Florida, USA