{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T23:50:19Z","timestamp":1791071419329,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540291060","type":"print"},{"value":"9783540320241","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560586_8","type":"book-chapter","created":{"date-parts":[[2005,10,20]],"date-time":"2005-10-20T14:08:27Z","timestamp":1129817307000},"page":"81-96","source":"Crossref","is-referenced-by-count":11,"title":["The Language \u03c7: Circuits, Computations and Classical Logic"],"prefix":"10.1007","author":[{"given":"Steffen","family":"van Bakel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"St\u00e9phane","family":"Lengrand","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre","family":"Lescanne","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"4","key":"8_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. Journal of Functional Programming\u00a01(4), 375\u2013416 (1991)","journal-title":"Journal of Functional Programming"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Jim, T.: Continuation-passing, closure-passing style. In: POPL1989, pp. 293\u2013302 (1989)","DOI":"10.1145\/75277.75303"},{"key":"8_CR3","unstructured":"van Bakel, S., Raghunandan, J.: Implementing X. In: TermGraph 2004, ENTCS (2005)"},{"key":"8_CR4","unstructured":"van Bakel, S., Raghunandan, J., Summers, A.: Term Graphs, \u03b1-conversion and Principal Types for \u03c7 (2005)"},{"issue":"2","key":"8_CR5","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0025","volume":"125","author":"F. Barbanera","year":"1996","unstructured":"Barbanera, F., Berardi, S.: A symmetric lambda calculus for classical program extraction. Information and Computation\u00a0125(2), 103\u2013117 (1996)","journal-title":"Information and Computation"},{"key":"8_CR6","volume-title":"The Lambda Calculus: its Syntax and Semantics","author":"H. Barendregt","year":"1984","unstructured":"Barendregt, H.: The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam (1984)"},{"issue":"1","key":"8_CR7","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1017\/S0956796899003524","volume":"10","author":"H.P. Barendregt","year":"2000","unstructured":"Barendregt, H.P., Ghilezan, S.: Lambda terms for natural deduction, sequent calculus and cut-elimination. Journal of Functional Porgramming\u00a010(1), 121\u2013134 (2000)","journal-title":"Journal of Functional Porgramming"},{"key":"8_CR8","unstructured":"Bloo, R., Rose, K.H.: Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In: CSN 1995, pp. 62\u201372 (1995)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: ICFP 2000, pp. 233\u2013243 (2000)","DOI":"10.1145\/351240.351262"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: Computational isomorphisms in classical logic (extended abstract). ENTCS\u00a03 (1996)","DOI":"10.1016\/S1571-0661(05)80417-7"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: A new deconstructive logic: Linear logic. The Journal of Symbolic Logic\u00a062 (1997)","DOI":"10.2307\/2275572"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Dragalin, A.G.: Mathematical Intuitionism: Introduction to Proof Theory. Translations of Mathematical Monographs, vol.\u00a067. American Mathematical Society (1987)","DOI":"10.1090\/mmono\/067"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoretical Computer Science\u00a050, 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"8_CR14","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J.-Y. Girard","year":"1991","unstructured":"Girard, J.-Y.: A new constrcutive logic: classical logic. Mathematical Structures in Computer Science\u00a01(3), 255\u2013296 (1991)","journal-title":"Mathematical Structures in Computer Science"},{"key":"8_CR15","unstructured":"Herbelin, H.: S\u00e9quents qu\u2019on calcule\u00a0: de l\u2019interpr\u00e9tation du calcul des s\u00e9quents comme calcul de \u03bb-termes et comme calcul de strat\u00e9gies gagnantes. Th\u00e8se d\u2019universit\u00e9, Universit\u00e9 Paris\u00a07 (1995)"},{"issue":"1","key":"8_CR16","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.ic.2003.09.004","volume":"189","author":"S. Lengrand","year":"2004","unstructured":"Lengrand, S., Lescanne, P., Dougherty, D., Dezani-Ciancaglini, M., van Bakel, S.: Intersection types for explicit substitutions. Information and Computation\u00a0189(1), 17\u201342 (2004)","journal-title":"Information and Computation"},{"key":"8_CR17","volume-title":"ENTCS","author":"S. Lengrand","year":"2003","unstructured":"Lengrand, S.: Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. In: ENTCS, vol.\u00a086, Elsevier, Amsterdam (2003)"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/174675.174707","volume-title":"POPL 1994","author":"P. Lescanne","year":"1994","unstructured":"Lescanne, P.: From \u03bb\u03c3 to \u03bb\u03c5, a journey through calculi of explicit substitutions. In: POPL 1994, pp. 60\u201369. ACM, New York (1994)"},{"key":"8_CR19","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das Logische Schliessen. Mathematische Zeitschrift 39, 176\u2013210, 405\u2013431 (1935); English translation in [20], pp. 68\u2013131","journal-title":"Mathematische Zeitschrift"},{"key":"8_CR20","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Collected Papers of Gerhard Gentzen","year":"1969","unstructured":"Szabo, M.E. (ed.): The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1969)"},{"key":"8_CR21","series-title":"M.\u00a0Parigot","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. M.\u00a0Parigot, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"8_CR22","unstructured":"Urban, C.: Classical Logic and Computation. PhD thesis, University of Cambridge, Cambridge (2000)"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Call-by-Value is Dual to Call-by-Name. In: ICFP 2003, pp. 189\u2013201 (2003)","DOI":"10.1145\/944705.944723"},{"key":"8_CR24","volume-title":"Principia Mathematica","author":"A.N. Whitehead","year":"1925","unstructured":"Whitehead, A.N., Russell, B.: Principia Mathematica. Cambridge University Press, Cambridge (1925)"},{"key":"8_CR25","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511623585","volume-title":"Principia Mathematica to *56","author":"A.N. Whitehead","year":"1997","unstructured":"Whitehead, A.N., Russell, B.: Principia Mathematica to *56. Cambridge University Press, Cambridge (1997)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560586_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T11:09:04Z","timestamp":1586516944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560586_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291060","9783540320241"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11560586_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}