#8 Cedille - Chris Jenkins
Type Theory Forall
English - May 11, 2021 02:30 - 1 hour - 48.2 MB - ★★★★★ - 6 ratingsTechnology Science type theory programming languages academia Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: #7 Hacking Isabelle's Internals - Daniel Matichuk
Next Episode: #9 Logic and Proof Theory - Anupam Das
In this episode I have a nice conversation with Chris Jenkins to talk about
the Cedille theorem prover, based on a very concise type theory called CDLE.
The main selling point of Cedille is that the theory is so small that the
typing rules fit one page. And yet it is strong enough to do relevant theorem
proving. This is probably the most technical episode so far.
Links
Leroy Jenkins
Cedille Cast
The Iowa Type Theory Commute
Cedille Page
Github Page