Sveriges mest populära poddar
Type Theory Forall

#8 Cedille - Chris Jenkins

1 tim 6 min11 maj 2021

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

Type Theory Forall med Pedro Abreu finns tillgänglig på flera plattformar. Informationen på denna sida kommer från offentliga podd-flöden.