{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:12:08Z","timestamp":1761610328847,"version":"build-2065373602"},"reference-count":22,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3893,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,12]]},"DOI":"10.1016\/s1571-0661(04)80505-x","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"42-59","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":1,"title":["Eliminating Proofs from Programs"],"prefix":"10.1016","volume":"70","author":[{"given":"Femke","family":"van Raamsdonk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paula","family":"Severi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB1","first-page":"118","article-title":"Lambda calculi with types","volume":"volume 2","author":"Barendregt","year":"1992"},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB2","doi-asserted-by":"crossref","unstructured":"G. Barthe, and P.-A. Melli\u00e8s. On the subject reduction property for algebraic type systems. In Proceedings of CSL '96, number 1258 in LNCS, pages 34\u201357. Springer, 1997.","DOI":"10.1007\/3-540-63172-0_31"},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB3","unstructured":"R. Burstall and J. McKinna. Deliverables: An approach to program development in the calculus of constructions. In Proceedings of the First Workshop on Logical Frameworks, pages 113\u2013121, 1990."},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB4","doi-asserted-by":"crossref","unstructured":"T. Crolard. A type theory which is complete for Kreisel's modified realizability. ENTCS, 23 (1), 1999. In the proceedings of a tutorial workshop on realizability semantics and applications, 1999.","DOI":"10.1016\/S1571-0661(04)00104-5"},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB5","unstructured":"B. Barras et al. The Coq proof assistant reference manual. Technical report, INRIA, 1999."},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB6","unstructured":"M. Fern\u00e1ndez, I. Mackie, P. Severi and N. Szasz. A uniform approach to program extraction: Pure Type Systems with ultra-\u2211 types. Preprint."},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB7","doi-asserted-by":"crossref","unstructured":"M. Fern\u00e1ndez and P. Severi. An operational approach to program extraction in the calculus of constructions. To appear in Proceedings of LOPSTR'02, 2002.","DOI":"10.1007\/3-540-45013-0_10"},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB8","doi-asserted-by":"crossref","unstructured":"J.H. Geuvers. The Church-Rosser property for \u03b2\u03b7-reduction in typed lambda calculi. In Proceedings of LICS '92, pages 453\u2013460. IEEE Computer Society Press, 1992.","DOI":"10.1109\/LICS.1992.185556"},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB9","unstructured":"J.H. Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, 1993."},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB10","doi-asserted-by":"crossref","unstructured":"M. Hanus and C. Prehofer. Higher-order narrowing with definitional trees. In H. Ganzinger, editor, Proceedings of RTA '96, number 1103 in LNCS, pages 138\u2013152, 1996.","DOI":"10.1007\/3-540-61464-8_48"},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB11","doi-asserted-by":"crossref","unstructured":"Z. Luo. ECC, an extended calulus of constructions. In Proceedings of LICS '89, pages 386\u2013395. IEEE Computer Society Press, 1989.","DOI":"10.1109\/LICS.1989.39193"},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB12","unstructured":"Z. Luo and R. Pollack. LEGO proof development system: User's manual. Technical report, University of Edinburgh, 1992."},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB13","doi-asserted-by":"crossref","unstructured":"J.H. McKinna. Deliverables: a categorical approach to program development in type theory. PhD thesis, University of Edinburgh, 1992.","DOI":"10.1007\/3-540-57182-5_3"},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB14","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting F\u03c9's programs from proofs in the calculus of constructions. In Proceedings of POPL '89, pages 89\u2013104, 1989.","DOI":"10.1145\/75277.75285"},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB15","unstructured":"C. Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. Th\u00e8eGse d'universit\u00e9A, Paris 7, 1989."},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB16","unstructured":"E. Poll. A Programming Logic Based on Type Theory. PhD thesis, Eindhoven University of Technology, 1994."},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB17","doi-asserted-by":"crossref","unstructured":"P. Severi and E. Poll. Pure type systems with definitions. In Proceedings of LFCS '94, number 813 in LNCS, pages 316\u2013328. Springer, 1994.","DOI":"10.1007\/3-540-58140-5_30"},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB18","unstructured":"P. Severi and N. Szasz. Internal program extraction in the calculus of inductive constructions. In Proceedings of Argentine Workshop in Theoretical Computer Science (WAIT'02), 2002."},{"issue":"1","key":"10.1016\/S1571-0661(04)80505-X_NEWBIB19","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1023\/A:1010663224299","article-title":"Studies of a theory of specifications with built-in program extraction","volume":"27","author":"Severi","year":"2001","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB20","unstructured":"Coq Development Team. The Coq proof assistant reference manual version 7.1 2001. URL: http:\/\/pauillac.inria.fr\/coq\/doc\/main.html."},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB21","unstructured":"LEGO Team. The LEGO library, version 1.3, 1998. URL: http:\/\/www.dcs.ed.ac.uk\/home\/lego\/html\/release.html."},{"key":"10.1016\/S1571-0661(04)80505-X_NEWBIB22","doi-asserted-by":"crossref","unstructured":"V. van Oostrom. Development closed critical pairs. In Proceedings of HOA '95, number 1074 in LNCS, pages 185\u2013200. Springer, 1995.","DOI":"10.1007\/3-540-61254-8_26"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480505X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480505X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:06:10Z","timestamp":1761609970000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106610480505X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,12]]}},"alternative-id":["S157106610480505X"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80505-x","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Eliminating Proofs from Programs","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80505-X","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}