|
eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/7298
| Title: | Improving the Efficiency of Nuprl Proofs |
| Authors: | Nogin, Aleksey |
| Keywords: | computer science
technical report |
| Issue Date: | Aug-1997 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR97-1643 |
| Abstract: | In order to use Nuprl system as a programming language with built-in verification one has to improve the efficiency of the programs extracted from the Nuprl proofs. In the current paper we consider proofs from the Nuprl automata library. In some of these proofs (pigeon-hole principle, decidability of the state reachability, decidability of the equivalence relation on words induced by the automata language) sources of exponential-time complexity have been detected and replaced by new complexity cautious proofs. The new proofs now lead to polynomial-time algorithms extracted by the same Nuprl extractor, thus eliminating all known unnecessary exponentials from the Nuprl automata library. General principles of efficient programming on Nuprl are also discussed. Key Words and Phrases: automata, constructivity, Myhill-Nerode theorem, Nuprl, program extraction, program verification, state minimization. |
| URI: | http://hdl.handle.net/1813/7298 |
| Appears in Collections: | Computer Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
