Efficient Programming by Extract in Nuprl Type Theory - Continued
by Aleksey Nogin
CommentI 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.