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