{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:48:24Z","timestamp":1725490104763},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_7","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T14:49:52Z","timestamp":1187794192000},"page":"70-85","source":"Crossref","is-referenced-by-count":6,"title":["Extracting Purely Functional Contents from Logical Inductive Types"],"prefix":"10.1007","author":[{"given":"David","family":"Delahaye","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine","family":"Dubois","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Fr\u00e9d\u00e9ric","family":"\u00c9tienne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Attali, I., Parigot, D.: Integrating Natural Semantics and Attribute Grammars: the Minotaur System. Technical Report 2339, INRIA (1994)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","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, pp. 24\u201340. Springer, Heidelberg (2002)"},{"issue":"2","key":"7_CR3","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/64135.65005","volume":"24","author":"P. Borras","year":"1988","unstructured":"Borras, P., Cl\u00e9ment, D., Despeyroux, T., Incerpi, J., Kahn, G., Lang, B., Pascual, V.: Centaur: the System. ACM SIGSOFT\/SIGPLAN Software Engineering Symposium on Practical Software Development Environments (PSDE)\u00a024(2), 14\u201324 (1988)","journal-title":"ACM SIGSOFT\/SIGPLAN Software Engineering Symposium on Practical Software Development Environments (PSDE)"},{"key":"7_CR4","unstructured":"Dubois, C., Gayraud, R.: Compilation de la s\u00e9mantique naturelle vers ML. In: Weis, P. (ed.) Journ\u00e9es Francophones des Langages Applicatifs (JFLA), Morzine-Avoriaz (France) (February 1999)"},{"issue":"1-2","key":"7_CR5","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.scico.2005.02.006","volume":"58","author":"M.V. Hermenegildo","year":"2005","unstructured":"Hermenegildo, M.V., Puebla, G., Bueno, F., L\u00f3pez-Garc\u00eda, P.: Integrated Program Debugging, Verification, and Optimization using Abstract Interpretation (and the Ciao System Preprocessor). Science of Computer Programming\u00a058(1-2), 115\u2013140 (2005)","journal-title":"Science of Computer Programming"},{"key":"7_CR6","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":"7_CR7","first-page":"109","volume-title":"Principles and Practice of Declarative Programming (PPDP)","author":"D. Overton","year":"2002","unstructured":"Overton, D., Somogyi, Z., Stuckey, P.J.: Constraint-based Mode Analysis of Mercury. In: Principles and Practice of Declarative Programming (PPDP), Pittsburgh (PA, USA), October 2002, pp. 109\u2013120. ACM Press, New York (2002)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/3-540-61053-7_61","volume-title":"Compiler Construction","author":"M. Pettersson","year":"1996","unstructured":"Pettersson, M.: A Compiler for Natural Semantics. In: Gyim\u00f3thy, T. (ed.) CC 1996. LNCS, vol.\u00a01060, pp. 177\u2013191. Springer, Heidelberg (1996)"},{"issue":"3","key":"7_CR9","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1093\/logcom\/4.3.249","volume":"4","author":"R.F. St\u00e4rk","year":"1994","unstructured":"St\u00e4rk, R.F.: Input\/Output Dependencies of Normal Logic Programs. Journal of Logic and Computation\u00a04(3), 249\u2013262 (1994)","journal-title":"Journal of Logic and Computation"},{"key":"7_CR10","unstructured":"The Coq Development Team: Coq, version 8.1. INRIA (November 2006), available at: \n                  \n                    http:\/\/coq.inria.fr\/"},{"key":"7_CR11","unstructured":"The Cristal Team: Objective Caml, version 3.09.3. INRIA (September 2006), available at: \n                  \n                    http:\/\/caml.inria.fr\/"},{"issue":"1-2","key":"7_CR12","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1016\/j.jlap.2005.09.008","volume":"67","author":"A. Verdejo","year":"2006","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Executable Structural Operational Semantics in Maude. Journal of Logic and Algebraic Programming\u00a067(1-2), 226\u2013293 (2006)","journal-title":"Journal of Logic and Algebraic Programming"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:28:14Z","timestamp":1619519294000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}