KnowledgeBase » 
SEMINAR
» ID = 519
Efficient Programming by Extract in Nuprl Type Theory - Continued
by Aleksey Nogin
1999-2000
Comment
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.