{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:33:03Z","timestamp":1725471183201},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_16","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"162-176","source":"Crossref","is-referenced-by-count":4,"title":["Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics"],"prefix":"10.1007","author":[{"given":"Robert","family":"Constable","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Moczyd\u0142owski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","first-page":"55","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. The Journal of Symbolic Logic\u00a05, 55\u201368 (1940)","journal-title":"The Journal of Symbolic Logic"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"16_CR3","unstructured":"Berghofer, S.: Proofs, Programs and Executable Specifications in Higher Order Logic. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2004)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, Springer, Heidelberg (2002)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin-Mohring, C.: Inductively defined types, preliminary version. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, pp. 50\u201366. Springer, Heidelberg (1990)"},{"key":"16_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development; Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development; Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"16_CR7","volume-title":"Automated Deduction","author":"H. Benl","year":"1998","unstructured":"Benl, H., Berger, U., Schwichtenberg, H., others,: Proof theory at work: Program development in the Minlog system. In: Bibel, W., Schmitt, P.G. (eds.) Automated Deduction, vol.\u00a0II, Kluwer, Dordrecht (1998)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Allen, S.F., et al.: Innovations in computational type theory using Nuprl (to appear, 2006)","DOI":"10.1016\/j.jal.2005.10.005"},{"key":"16_CR9","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., et al.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, NJ (1986)"},{"key":"16_CR10","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0049-237X(09)70189-2","volume-title":"Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. In: Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science, pp. 153\u2013175. North-Holland, Amsterdam (1982)"},{"key":"16_CR11","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6f\u2019s Type Theory. Oxford Sciences Publication, Oxford (1990)"},{"key":"16_CR12","unstructured":"Augustsson, L., Coquand, T., Nordstr\u00f6m, B.: A short description of another logical framework. In: Proceedings of the First Annual Workshop on Logical Frameworks, Sophia-Antipolis, France, pp. 39\u201342 (1990)"},{"key":"16_CR13","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual \u2013 Version V8.0 (2004), http:\/\/coq.inria.fr"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/10930755_19","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hickey","year":"2003","unstructured":"Hickey, J., et al.: MetaPRL \u2014 A modular logical environment. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 287\u2013303. Springer, Heidelberg (2003)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/10721959_12","volume-title":"Automated Deduction - CADE-17","author":"S. Allen","year":"2000","unstructured":"Allen, S., et al.: The Nuprl open logical environment. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 170\u2013176. Springer, Heidelberg (2000)"},{"key":"16_CR16","volume-title":"Logic Colloquium 1977","author":"P. Aczel","year":"1978","unstructured":"Aczel, P.: The type theoretic interpretation of constructive set theory. In: MacIntyre, A., Pacholski, L., Paris, J. (eds.) Logic Colloquium 1977, North-Holland, Amsterdam (1978)"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BFb0014309","volume-title":"Algebraic Methodology and Software Technology","author":"D.J. Howe","year":"1996","unstructured":"Howe, D.J.: Semantic foundations for embedding HOL in Nuprl. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol.\u00a01101, pp. 85\u2013101. Springer, Heidelberg (1996)"},{"key":"16_CR18","volume-title":"Frontiers of Combining Systems, FroCoS 1998, ILLC","author":"D.J. Howe","year":"1998","unstructured":"Howe, D.J.: Toward sharing libraries of mathematics between theorem provers. In: Frontiers of Combining Systems, FroCoS 1998, ILLC, Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"16_CR19","doi-asserted-by":"publisher","first-page":"1233","DOI":"10.2178\/jsl\/1129642124","volume":"70","author":"M. Rathjen","year":"2005","unstructured":"Rathjen, M.: The disjunction and related properties for constructive Zermelo-Fraenkel set theory. Journal of Symbolic Logic\u00a070, 1233\u20131254 (2005)","journal-title":"Journal of Symbolic Logic"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Moczyd\u0142owski, W.: Normalization of IZF with Replacement. Technical Report 2006-2024, Computer Science Department, Cornell University (2006)","DOI":"10.1007\/11874683_34"},{"key":"16_CR21","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"16_CR22","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/BFb0066775","volume-title":"Cambridge Summer School in Mathematical Logic","author":"J. Myhill","year":"1973","unstructured":"Myhill, J.: Some properties of intuitionistic Zermelo-Fraenkel set theory. In: Cambridge Summer School in Mathematical Logic, vol.\u00a029, pp. 206\u2013231. Springer, Heidelberg (1973)"},{"key":"16_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of Constructive Mathematics","author":"M.J. Beeson","year":"1985","unstructured":"Beeson, M.J.: Foundations of Constructive Mathematics. Springer, Heidelberg (1985)"},{"key":"16_CR24","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/0168-0072(86)90050-3","volume":"32","author":"D. McCarty","year":"1986","unstructured":"McCarty, D.: Realizability and recursive set theory. Journal of Pure and Applied Logic\u00a032, 153\u2013183 (1986)","journal-title":"Journal of Pure and Applied Logic"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Friedman, H.: The consistency of classical set theory relative to a set theory with intuitionistic logic. The Journal of Symbolic Logic, 315\u2013319 (1973)","DOI":"10.2307\/2272068"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:14:30Z","timestamp":1605644070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11814771_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}