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