{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:19Z","timestamp":1774837819710,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540406648","type":"print"},{"value":"9783540451303","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/10930755_14","type":"book-chapter","created":{"date-parts":[[2006,6,19]],"date-time":"2006-06-19T11:27:09Z","timestamp":1150716429000},"page":"205-220","source":"Crossref","is-referenced-by-count":9,"title":["Program Extraction from Large Proof Developments"],"prefix":"10.1007","author":[{"given":"Lu\u00eds","family":"Cruz-Filipe","sequence":"first","affiliation":[]},{"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","first-page":"117","volume-title":"Handbook of logic in computer science","author":"H.P. Barendregt","year":"1992","unstructured":"Barendregt, H.P.: Lambda calculi with types. In: Handbook of logic in computer science, vol.\u00a02, pp. 117\u2013309. Oxford Univ. Press, New York (1992)"},{"key":"14_CR2","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill Book Company, New York (1967)"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S0049-237X(08)70740-7","volume-title":"Intuitionism and Proof Theory (Proceedings of the summer Conference at Buffalo, N.Y., 1968)","author":"E. Bishop","year":"1970","unstructured":"Bishop, E.: Mathematics as a numerical language. In: Intuitionism and Proof Theory (Proceedings of the summer Conference at Buffalo, N.Y., 1968), pp. 53\u201371. North-Holland, Amsterdam (1970)"},{"key":"14_CR4","unstructured":"Capretta, V.: Abstraction and Computation. PhD thesis, University of Nijmegen (2002)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-39185-1_5","volume-title":"Types for Proofs and Programs","author":"J. Carlstr\u00f6m","year":"2003","unstructured":"Carlstr\u00f6m, J.: Subsets, quotients and partial functions in martin-l\u00f6f\u2019s type theory. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 78\u201394. Springer, Heidelberg (2003) (to appear)"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-44557-9_7","volume-title":"Types for Proofs and Programs","author":"A. Ciaffaglione","year":"2000","unstructured":"Ciaffaglione, A., Gianantonio, P.D.: A co-inductive approach to real numbers. In: Coquand, T., Nordstr\u00f6m, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol.\u00a01956, pp. 114\u2013130. Springer, Heidelberg (2000)"},{"key":"14_CR7","unstructured":"Courant, J.: MC2: A module calculus for pure type systems. Technical Report 1292, LRI (September 2001)"},{"key":"14_CR8","unstructured":"Fern\u00e1ndez, M., Mackie, I., Severi, P., Szasz, N.: A uniform approach to program extraction: Pure type systems with ultra \u03c3-types, http:\/\/www.cmat.edu.uy\/~severi\/publications.html"},{"key":"14_CR9","unstructured":"Geuvers, H.: Inconsistency of classical logic in type theory, http:\/\/www.cs.kun.nl\/~herman\/note.ps.gz"},{"key":"14_CR10","first-page":"271","volume-title":"Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: The algebraic hierarchy of the FTA Project. In: Linton, S.S. (ed.) Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems, pp. 271\u2013286. Elsevier, Amsterdam (2002)"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-45842-5_7","volume-title":"Types for Proofs and Programs","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Wiedijk, F., Zwanenburg, J.: A constructive proof of the Fundamental Theorem of Algebra without using the rationals. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 96\u2013111. Springer, Heidelberg (2002)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proceedings ICFP 2002 (2002)","DOI":"10.1145\/581478.581501"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P. Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 200\u2013219. Springer, Heidelberg (2003)"},{"key":"14_CR14","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0049-237X(09)70189-2","volume-title":"Logic, Methodology and the Philosophy of Science VI","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer science. In: Logic, Methodology and the Philosophy of Science VI, pp. 153\u2013175. North-Holland, Amsterdam (1982)"},{"key":"14_CR15","unstructured":"Niqui, M.: Exact arithmetic on Stern-Brocot tree, (2003) (submitted)"},{"key":"14_CR16","volume-title":"Sixteenth Annual ACM Symposium on Principles of Programming Languages","author":"C. Paulin-Mohring","year":"1989","unstructured":"Paulin-Mohring, C.: Extracting F\u03c9\u2019s programs from proofs in the Calulus of Constructions. In: Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin. ACM, New York (1989)"},{"key":"14_CR17","unstructured":"Pottier, L.: Quotients dans le CCI. Technical Report RR-4053, INRIA (November 2000), http:\/\/www-sop.inria.fr\/rapports\/sophia\/RR-4053.html"},{"key":"14_CR18","unstructured":"Prost, F.: Marking techniques for extraction. Technical Report 95-47, Laboratoire de l\u2019informatique du Parall\u00e9lisme, Ecole Normale Sup\u00e9rieure de Lyon (1995)"},{"key":"14_CR19","unstructured":"Schwichtenberg, H.: Minimal logic for computable functionals. Technical report, Mathematisches Institut der Universit\u00e4t M\u00fcnchen (2002)"},{"key":"14_CR20","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual Version 7.3. INRIA-Rocquencourt (2002)"},{"key":"14_CR21","series-title":"Handbook of Proof Theory","first-page":"407","volume-title":"Realizability","author":"A.S. Troelstra","year":"1998","unstructured":"Troelstra, A.S.: Realizability. Handbook of Proof Theory, pp. 407\u2013473. North-Holland, Amsterdam (1998)"},{"key":"14_CR22","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Constructivism in mathematics. An introduction","author":"A.S. Troelstra","year":"1988","unstructured":"Troelstra, A.S., van Dalen, D.: Constructivism in mathematics. An introduction. Studies in Logic and the Foundations of Mathematics, vol.\u00a0123. North-Holland, Amsterdam (1988)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10930755_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T08:24:08Z","timestamp":1555662248000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10930755_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406648","9783540451303"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/10930755_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}