{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:30Z","timestamp":1725456210378},"publisher-location":"Berlin\/Heidelberg","reference-count":12,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012825","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"101-110","source":"Crossref","is-referenced-by-count":3,"title":["An environment for automated reasoning about partial functions"],"prefix":"10.1007","author":[{"given":"David A.","family":"Basin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Robert S. Boyer and J. Strother Moore. A Computational Logic. Academic Press, 1979."},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Robert S. Boyer and J. Strother Moore. A mechanical proof of the unsolvability of the halting problem. Journal of the Association for Computing Machinery, July 1984.","DOI":"10.1145\/828.1882"},{"key":"6_CR3","unstructured":"R.L. Constable. Constructive mathematics and automatic program writers. In Proceedings of IFIP Congress, Ljubljana, 1971."},{"key":"6_CR4","unstructured":"R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986."},{"key":"6_CR5","unstructured":"R.L. Constable and S.F. Smith. Partial objects in constructive type theory. In Symposium on Logic in Computer Science, Computer Society Press of the IEEE, 1987."},{"key":"6_CR6","unstructured":"Thierry Coquand and G\u00e9rard Huet. A theory of constructions. 1984. Unpublished manuscript."},{"key":"6_CR7","unstructured":"Douglas J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell, 1987."},{"key":"6_CR8","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0049-237X(09)70189-2","volume-title":"Sixth International Congress for Logic, Methodology, and Philosophy of Science","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153\u2013175, North Holland, Amsterdam, 1982."},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Lawrence Paulson. Lessons learned from LCF: a survey of natural deduction proofs. Comp. J., 28(5), 1985.","DOI":"10.1093\/comjnl\/28.5.474"},{"key":"6_CR10","unstructured":"H. Rogers, Jr. Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967."},{"key":"6_CR11","unstructured":"N. Shankar. Towards Mechanical Metamathematics. Technical Report 43, University of Texas at Austin, 1984."},{"key":"6_CR12","unstructured":"S.F. Smith. The Structure Of Computation in Type Theory. PhD thesis, Cornell, 1988. In preparation."}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012825","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:24:14Z","timestamp":1586579054000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012825"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0012825","relation":{},"subject":[]}}