{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:00:09Z","timestamp":1725663609342},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_60","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:46:40Z","timestamp":1330192000000},"page":"475-494","source":"Crossref","is-referenced-by-count":1,"title":["Some normalization properties of martin-l\u00f6f's type theory, and applications"],"prefix":"10.1007","author":[{"given":"David A.","family":"Basin","sequence":"first","affiliation":[]},{"given":"Douglas J.","family":"Howe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"23_CR1","unstructured":"S. F. Allen. A non-type theoretic definition of Martin-L\u00f6f's types. In Proceedings of the Second Annual Symposium on Logic in Computer Science, pages 215\u2013221. IEEE, 1987."},{"key":"23_CR2","unstructured":"S. F. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, 1987."},{"key":"23_CR3","unstructured":"D. A. Basin. Extracting circuits from constructive proofs. In IFIP-IEEE International Workshop on Formal Methods in VLSI Design, Miami, USA, January 1991."},{"key":"23_CR4","first-page":"43","volume-title":"From HDL Descriptions to Guaranteed Correct Circuit Designs","author":"A. Camilleri","year":"1987","unstructured":"A. Camilleri, M. Gordon, and T. Melham. Hardware verification using higher-order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 43\u201367. Elsevier Science Publishers B. V. (North-Holland), 1987."},{"key":"23_CR5","unstructured":"R. Constable and D. Howe. Nuprl as a general logic. In P. Odifreddi, editor, Logic in Computer Science, pages 77\u201390. Academic Press, 1990."},{"key":"23_CR6","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"key":"23_CR7","unstructured":"M. P. Fourman. Formal methods for modeling design. In Conference on Modeling the Innovation: Communications, Automation and Information Systems, Rome, Italy, 1990."},{"key":"23_CR8","unstructured":"F. Hanna, N. Daeche, and M. Longley. VERITAS+: A specification language based on type theory. In Hardware Specification, Verification and Synthesis: Mathematical Aspects, Ithaca, New York, 1989. Springer-Verlag."},{"key":"23_CR9","unstructured":"F. K. Hanna, M. Longley, and N. Daeche. Formal synthesis of digital systems. In IMEC-IFIP International Workshop on: Applied Formal Methods For Correct VLSI Design, volume 2, pages 532\u2013548, Leuven, Belgium, 1989."},{"key":"23_CR10","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. In The Second Annual Symposium on Logic in Computer Science. IEEE, 1987."},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"D. Howe. Computational metatheory in Nuprl. Proc. of 9th International Conference on Automated Deduction, pages 238\u2013257, 1988.","DOI":"10.1007\/BFb0012835"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"D. Howe. Equality in lazy computation systems. Proc. Fourth Annual Symposium on Logic in Computer Science, IEEE, pages 198\u2013203, June 1989.","DOI":"10.1109\/LICS.1989.39174"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"D. Howe. On computational open-endedness in Martin-L\u00f6f's type theory. To appear in Proc. Sixth Annual Symposium on Logic in Computer Science, IEEE.","DOI":"10.1109\/LICS.1991.151641"},{"key":"23_CR14","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":"P. 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."},{"key":"23_CR15","unstructured":"B. N\u00f6rdstrom, K. Petersson, and J. M. Smith. Programming in Martin-L\u00f6f's Type Theory, volume 7 of International Series of Monographs on Computer Science. Oxford Science Publications, 1990."},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Natural deduction proof as higher-order resolution. Journal of Logic Programming, (3):237\u2013258, 1985.","DOI":"10.1016\/0743-1066(86)90015-4"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54415-1_60.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:21:28Z","timestamp":1619558488000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}