{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:15:15Z","timestamp":1754482515705},"publisher-location":"New York, NY","reference-count":13,"publisher":"Springer New York","isbn-type":[{"type":"print","value":"9780387972268"},{"type":"electronic","value":"9780387348018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/0-387-97226-9_36","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:11:42Z","timestamp":1330182702000},"page":"333-357","source":"Crossref","is-referenced-by-count":7,"title":["Verification of combinational logic in Nuprl"],"prefix":"10.1007","author":[{"given":"David A.","family":"Basin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Vecchio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"5","key":"17_CR1","doi-asserted-by":"crossref","first-page":"611","DOI":"10.1109\/32.24710","volume":"15","author":"G. Barrett","year":"1989","unstructured":"G. Barrett. Formal methods applied to a floating point number system. IEEE Transactions on Software Engineering, 15(5):611\u2013621, May 1989.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"17_CR2","unstructured":"David A. Basin. Implementing Problem Solving Environments In Constructive Type Theory. PhD thesis, Cornell University, 1990. To appear."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"David A. Basin. Building theories in Nuprl. In Logic At Botik, '89, 1989. To Appear.","DOI":"10.1007\/3-540-51237-3_3"},{"key":"17_CR4","unstructured":"Robert S. Boyer and J. Strother Moore. A Computational Logic. Academic Press, 1979."},{"key":"17_CR5","unstructured":"A. J. Camillieri, M. J. C. Gordon, and T. F. Melham. Hardware verification using higher-order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. North Holland, September 1986."},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"A. Cohn. A proof of correctness of the VIPER microprocessor: The first level. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis, pages 27\u201372. Kluwer, 1988.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"17_CR7","unstructured":"R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Michael J. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"17_CR9","unstructured":"Douglas J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988."},{"key":"17_CR10","unstructured":"Warren J. Hunt. The mechanical verification of a microprocessor design. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 89\u2013129. Elsevier Science Publishers B. V. (North-Holland), 1987."},{"key":"17_CR11","unstructured":"INMOS. T800 architecture. INMOS Technical note 6."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153\u2013175, Amsterdam, 1982. North Holland.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"17_CR13","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"L. C. Paulson","year":"1983","unstructured":"Lawrence C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119\u2013149, 1983.","journal-title":"Science of Computer Programming"}],"container-title":["Lecture Notes in Computer Science","Hardware Specification, Verification and Synthesis: Mathematical Aspects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/0-387-97226-9_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:21:35Z","timestamp":1605644495000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/0-387-97226-9_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9780387972268","9780387348018"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/0-387-97226-9_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}