An Environment for Automated Reasoning About Partial Functions
| dc.contributor.author | Basin, David A. | en_US |
| dc.date.accessioned | 2007-04-23T17:23:17Z | |
| dc.date.available | 2007-04-23T17:23:17Z | |
| dc.date.issued | 1987-11 | en_US |
| dc.description.abstract | We report on a new environment developed and implemented inside the Nuprl type theory that facilitates proving theorems about partial functions. It is the first such automated type-theoretic account of partiality. We demonstrate that such an environment can be used effectively for proving theorems about computability and for developing partial programs with correctness proofs. This extends the well-known proofs as programs paradigm to partial functions. | en_US |
| dc.format.extent | 1208827 bytes | |
| dc.format.extent | 294554 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-884 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/6724 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | An Environment for Automated Reasoning About Partial Functions | en_US |
| dc.type | technical report | en_US |