{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214531},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540404385"},{"type":"electronic","value":"9783540450139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45013-0_10","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:06:29Z","timestamp":1184601989000},"page":"111-125","source":"Crossref","is-referenced-by-count":1,"title":["An Operational Approach to Program Extraction in the Calculus of Constructions"],"prefix":"10.1007","author":[{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paula","family":"Severi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,24]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"J-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.","key":"10_CR1","DOI":"10.1017\/CBO9780511624162"},{"doi-asserted-by":"crossref","unstructured":"H.P. Barendregt. Lambda calculi with types. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 118\u2013310. Oxford University Press, 1992.","key":"10_CR2","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"unstructured":"Barras et al. The Coq Proof Assistant Reference Manual. Technical report, INRIA, 1999.","key":"10_CR3"},{"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_CR4"},{"doi-asserted-by":"crossref","unstructured":"Z. Luo. ECC, an Extended Calculus of Constructions. In Proceedings of LICS\u2019 89, IEEE, pages 386\u2013395. IEEE Computer Society Press, 1989.","key":"10_CR5","DOI":"10.1109\/LICS.1989.39193"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1017\/S0960129500000256","volume":"3","author":"Z. Luo","year":"1993","unstructured":"Z. Luo. Program specification and data refinement in type theory. Mathematical Structures in Computer Science, 3:333\u2013363, 1993.","journal-title":"Mathematical Structures in Computer Science"},{"issue":"2","key":"10_CR7","doi-asserted-by":"publisher","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M.H.A. Newman","year":"1942","unstructured":"M.H.A. Newman. On theories with a combinatorial definition of equivalence. Annals of Mathematics, 43(2):223\u2013243, 1942.","journal-title":"Annals of Mathematics"},{"doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting F \u03c9\u2019s programs from proofs in the Calculus of Constructions. In Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989. ACM.","key":"10_CR8","DOI":"10.1145\/75277.75285"},{"unstructured":"C. Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. Th\u00e8se d\u2019universit\u00e9, Paris 7, 1989.","key":"10_CR9"},{"unstructured":"E. Poll. A Programming Logic Based on Type Theory. PhD thesis, Eindhoven University of Technology, 1994.","key":"10_CR10"},{"doi-asserted-by":"crossref","unstructured":"F. van Raamsdonk and P. Severi. Eliminating proofs from programs. In Proceedings of Third International Workshop on Logical Frameworks and Meta-Languages, volume 70.2 of Electronic Notes in Theoretical Computer Science, 2002.","key":"10_CR11","DOI":"10.1016\/S1571-0661(04)80505-X"},{"issue":"1","key":"10_CR12","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1023\/A:1010663224299","volume":"27","author":"P. Severi","year":"2001","unstructured":"P. Severi and N. Szasz. Studies of a theory of specifications with built-in program extraction. Journal of Automated Reasoning, 27(1):61\u201387, 2001.","journal-title":"Journal of Automated Reasoning"},{"unstructured":"P. Severi and N. Szasz. Internal Program Extraction in the Calculus of Inductive Constructions. In 6th Argentinian Workshop in Theoretical Computer Science (WAIT\u201902), 31st JAIIO, 2002.","key":"10_CR13"},{"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_CR14"}],"container-title":["Lecture Notes in Computer Science","Logic Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45013-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,16]],"date-time":"2024-02-16T18:40:53Z","timestamp":1708108853000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45013-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540404385","9783540450139"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45013-0_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}