{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171511},"publisher-location":"Berlin\/Heidelberg","reference-count":12,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540571841"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0022575","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T06:14:45Z","timestamp":1131862485000},"page":"263-276","source":"Crossref","is-referenced-by-count":34,"title":["Classical proofs as programs"],"prefix":"10.1007","author":[{"given":"Michel","family":"Parigot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"H. BARENDREGT, The Lambda-Calculus, North-Holland, 1981."},{"key":"29_CR2","unstructured":"J.Y. GIRARD, Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieure. Th\u00e9se, Universit\u00e9 Paris 7, 1972."},{"key":"29_CR3","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J.Y. Girard","year":"1991","unstructured":"J.Y. GIRARD, A new constructive logic: classical logic. Mathematical Structures in Computer Science, vol. 1, 1991, pp. 255\u2013296.","journal-title":"Mathematical Structures in Computer Science"},{"key":"29_CR4","unstructured":"J.Y. GIRARD, Y. LAFONT, and P. TAYLOR, Proofs and Types, Cambridge University Press, 1989."},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"T. GRIFFIN, A formulae-as-types notion of control, Proc. POPL, 1990.","DOI":"10.1145\/96709.96714"},{"key":"29_CR6","unstructured":"J.L. KRIVINE, Lambda-calcul, types et mod\u00e8les, Masson, 1990."},{"key":"29_CR7","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/BF01792986","volume":"30","author":"J.L. Krivine","year":"1990","unstructured":"J.L. KRIVINE, Op\u00e9rateurs de mise en m\u00e9moire et traduction de G\u00f6del. Archiv for Mathematical Logic 30, 1990, pp 241\u2013267.","journal-title":"Archiv for Mathematical Logic"},{"issue":"3","key":"29_CR8","first-page":"149","volume":"26","author":"J.L. Krivine","year":"1990","unstructured":"J.L. KRIVINE, M. PARIGOT, Programming with proofs. EIK 26(3), 1990, pp 149\u2013167.","journal-title":"EIK"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"D. LEIVANT, Reasoning about functional programs and complexity classes associated with type disciplines. Proc. FOCS, 1983, pp 460\u2013469.","DOI":"10.1109\/SFCS.1983.50"},{"key":"29_CR10","first-page":"361","volume":"592","author":"M. Parigot","year":"1991","unstructured":"M. PARIGOT, Free Deduction: an Analysis of \u201cComputations\u201d in Classical Logic. Proc. Russian Conference on Logic Programming, St Petersburg (Russia), 1991, Springer LNCS 592, pp. 361\u2013380.","journal-title":"Springer LNCS"},{"key":"29_CR11","first-page":"190","volume":"624","author":"M. Parigot","year":"1992","unstructured":"M. PARIGOT, \u03bb\u03bc-calculus: an Algorithmic Interpretation of Classical Natural Deduction. Proc. International Conference on Logic Programming and Automated Reasoning, St Petersburg (Russia), 1992, Springer LNCS 624, pp. 190\u2013201.","journal-title":"Springer LNCS"},{"key":"29_CR12","unstructured":"M. PARIGOT, Strong Normalisation for Second Order Classical Natural Deduction, Proc. LICS 1993 (to appear)."}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022575.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:49:07Z","timestamp":1607550547000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022575"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540571841"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0022575","relation":{},"subject":[]}}