Skip to main content
PRL Project

Efficient Programming by Extract in Nuprl Type Theory - Continued

by Aleksey Nogin


I am going to continue talking about efficient programming by extract in Nuprl type theory.

I will try to explain while the pigeon-hole principle required such uncomputational proof and will present a slightly better proof.

I will also present the efficient proof of decidability of state reachability and explain why writing such a proof could be done in more straghtforward way than the proof of the pigeon-hole principle.