PRL Seminars
Aleksey Nogin
Efficient Programming by Extract in Nuprl Type Theory - ContinuedFebruary 14, 2000
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. Papers
|
| Home | | Introduction | | Authors | | Topics | | Chronological List | | PRL Project |