{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T23:50:27Z","timestamp":1791071427728,"version":"4.1.0"},"reference-count":50,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2008,6,1]],"date-time":"2008-06-01T00:00:00Z","timestamp":1212278400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2008,6]]},"abstract":"<jats:p><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129508006762_inline1\"><jats:alt-text>$\\X$<\/jats:alt-text><\/jats:inline-graphic>is an untyped continuation-style formal language with a typed subset that provides a Curry\u2013Howard isomorphism for a sequent calculus for implicative classical logic.<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129508006762_inline1\"><jats:alt-text>$\\X$<\/jats:alt-text><\/jats:inline-graphic>can also be viewed as a language for describing nets by composition of basic components connected by wires. These features make<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129508006762_inline1\"><jats:alt-text>${\\X}$<\/jats:alt-text><\/jats:inline-graphic>an expressive platform on which many different (applicative) programming paradigms can be mapped. In this paper we will present the syntax and reduction rules for<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129508006762_inline1\"><jats:alt-text>$\\X$<\/jats:alt-text><\/jats:inline-graphic>; in order to demonstrate its expressive power, we will show how elaborate calculi can be embedded, such as the \u03bb-calculus, Bloo and Rose's calculus of explicit substitutions \u03bbx, Parigot's \u03bb\u03bc and Curien and Herbelin's<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129508006762_inline2\"><jats:alt-text>$\\lmmt$<\/jats:alt-text><\/jats:inline-graphic>.<\/jats:p><jats:p><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129508006762_inline1\"><jats:alt-text>${\\X}$<\/jats:alt-text><\/jats:inline-graphic>was first presented in Lengrand (2003), where it was called the \u03bb\u03be-calculus. It can be seen as the pure untyped computational content of the reduction system for the implicative classical sequent calculus of Urban (2000).<\/jats:p>","DOI":"10.1017\/s0960129508006762","type":"journal-article","created":{"date-parts":[[2008,6,18]],"date-time":"2008-06-18T09:28:06Z","timestamp":1213781286000},"page":"555-609","source":"Crossref","is-referenced-by-count":10,"title":["Computation with classical sequents"],"prefix":"10.1017","volume":"18","author":[{"given":"STEFFEN","family":"VAN BAKEL","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"PIERRE","family":"LESCANNE","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2008,6,1]]},"reference":[{"key":"S0960129508006762_ref50","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511623585"},{"key":"S0960129508006762_ref47","first-page":"123","article-title":"Strong normalisation of cut-elimination in classical logic","volume":"45","author":"Urban","year":"2001","journal-title":"Fundamentae Informaticae"},{"key":"S0960129508006762_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_32"},{"key":"S0960129508006762_ref45","unstructured":"Urban C. (2000) Classical Logic and Computation, Ph.D. thesis, University of Cambridge."},{"key":"S0960129508006762_ref44","volume-title":"The Collected Papers of Gerhard Gentzen","author":"Szabo","year":"1969"},{"key":"S0960129508006762_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_7"},{"key":"S0960129508006762_ref41","doi-asserted-by":"crossref","unstructured":"Parigot M. (1993) Classical proofs as programs. Kurt G\u00f6del Colloquium 263\u2013276. (Presented at TYPES Workshop, at B\u01cestad, June 1992.)","DOI":"10.1007\/BFb0022575"},{"key":"S0960129508006762_ref38","first-page":"60","volume-title":"Proceedings of the 21st Annual ACM Symposium on Principles Of Programming Languages","author":"Lescanne","year":"1994"},{"key":"S0960129508006762_ref36","unstructured":"Lengrand S. (2006) Normalisation & Equivalence in Proof Theory & Type Theory, Ph.D. thesis, University of Paris VII and University of St Andrews."},{"key":"S0960129508006762_ref34","unstructured":"Lengrand S. (2002) A computational interpretation of the cut-rule in classical sequent calculus, Master's thesis, Mathematical Institute and Computing Laboratory, University of Oxford."},{"key":"S0960129508006762_ref31","unstructured":"Herbelin H. (1995) S\u00e9quents qu'on calcule : de l'interpr\u00e9tation du calcul des s\u00e9quents comme calcul de \u03bb-termes et comme calcul de strat\u00e9gies gagnantes, Th\u00e8se d'universit\u00e9, Universit\u00e9 Paris 7."},{"key":"S0960129508006762_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58216-9_27"},{"key":"S0960129508006762_ref29","doi-asserted-by":"crossref","unstructured":"Griffin T. (1990) A formulae-as-types notion of control. In: Proceedings of the 17th Annual ACM Symposium on Principles Of Programming Languages 47\u201358.","DOI":"10.1145\/96709.96714"},{"key":"S0960129508006762_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001328"},{"key":"S0960129508006762_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"S0960129508006762_ref42","unstructured":"Raghunandan J. and Summers A. (2006) On the Computational Representation of Classical Logical Connectives. (Presented at 2nd International Workshop on Developments in Computational Models (DCM 2006), Venice, Italy.)"},{"key":"S0960129508006762_ref25","doi-asserted-by":"crossref","unstructured":"Ghilezan S. and Lescanne P. (2004) Classical proofs, typed processes and intersection types. In: Berardi S. , Coppo M. and Damiani F. (eds.) TYPES'03 (to appear in Springer-Verlag Lecture Notes in Computer Science).","DOI":"10.1007\/978-3-540-24849-1_15"},{"key":"S0960129508006762_ref23","doi-asserted-by":"publisher","DOI":"10.2307\/2275572"},{"key":"S0960129508006762_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80417-7"},{"key":"S0960129508006762_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02962-6"},{"key":"S0960129508006762_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15983-5_13"},{"key":"S0960129508006762_ref17","doi-asserted-by":"crossref","unstructured":"Clement D. (1986) A Simple Applicative Language: MINI-ML. Technical Report 529, INRIA centre Sophia Antipolis (France).","DOI":"10.1145\/319838.319847"},{"key":"S0960129508006762_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013061"},{"key":"S0960129508006762_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90047-7"},{"key":"S0960129508006762_ref14","unstructured":"Bloo R. and Rose K. (1995) Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. CSN'95 \u2013 Computer Science in the Netherlands 62\u201372. (Available at ftp:\/\/ftp.diku.dk\/diku\/semantics\/papers\/D-246.ps.)"},{"key":"S0960129508006762_ref13","unstructured":"Bloo R. and Geuvers J. H. (1996) Explicit substitution: on the edge of strong normalisation. Computing Science Reports 96\u201310, Eindhoven University of Technology, The Netherlands. (To appear in Theoretical Computer Science.)"},{"key":"S0960129508006762_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003524"},{"key":"S0960129508006762_ref11","volume-title":"The Lambda Calculus: its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"S0960129508006762_ref10","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0025"},{"key":"S0960129508006762_ref8","unstructured":"van Bakel S. and Raghunandan J. (2005) Implementing $\\x$ . Electronic Proceedings of Second International Workshop on Term Graph Rewriting 2004 (TermGraph'04). Electronic Notes in Theoretical Computer Science."},{"key":"S0960129508006762_ref6","unstructured":"Audebaud P. and van Bakel S. (2006) Understanding $\\x$ with \u03bb\u03bc. Consistent interpretations of the implicative sequent calculus in natural deduction (submitted)."},{"key":"S0960129508006762_ref5","doi-asserted-by":"crossref","unstructured":"Ariola Z. M. , Herbelin H. and Sabry A. (2004) A type-theoretic foundation of continuations and prompts. In: Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming (ICFP'04), ACM 40\u201353.","DOI":"10.1145\/1016850.1016860"},{"key":"S0960129508006762_ref32","unstructured":"Herbelin H. (2005) C'est maintenant qu'on calcule: au c\u0153ur de la dualit\u00e9, M\u00e9moire d'habilitation, Universit\u00e9 Paris 11."},{"key":"S0960129508006762_ref39","doi-asserted-by":"crossref","unstructured":"Ong C.-H. L. and Stewart C. A. (1997) A Curry-Howard foundation for functional computation with control. In: Proceedings of the 24th Annual ACM Symposium on Principles Of Programming Languages 215\u2013227.","DOI":"10.1145\/263699.263722"},{"key":"S0960129508006762_ref49","volume-title":"Principia Mathematica","author":"Whitehead","year":"1925"},{"key":"S0960129508006762_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"S0960129508006762_ref19","doi-asserted-by":"crossref","unstructured":"Curien P.-L. and Herbelin H. (2000) The Duality of Computation. In: Proc. of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00), ACM 233\u2013243. (A corrected version is available from http:\/\/yquem.inria.fr\/herbelin\/publis\/icfp-CuHer00-duality+errata.ps.gz)","DOI":"10.1145\/351240.351262"},{"key":"S0960129508006762_ref16","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0960129508006762_ref15","unstructured":"de Bruijn N. G. (1978) A namefree lambda calculus with facilities for internal definition of expressions and segments. TH-Report 78-WSK-03, Technological University Eindhoven, Netherlands, Department of Mathematics."},{"key":"S0960129508006762_ref9","unstructured":"van Bakel S. and Raghunandan J. (2006) Capture avoidance and garbage collection for $\\x$ . Presented at the Third International Workshop on Term Graph Rewriting 2006 (TermGraph'06), Vienna, Austria."},{"key":"S0960129508006762_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82619-2"},{"key":"S0960129508006762_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.09.004"},{"key":"S0960129508006762_ref48","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944723"},{"key":"S0960129508006762_ref7","first-page":"81","volume-title":"Springer-Verlag Lecture Notes in Computer Science","author":"van Bakel","year":"2005"},{"key":"S0960129508006762_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75303"},{"key":"S0960129508006762_ref20","volume-title":"Combinatory Logic","author":"Curry","year":"1958"},{"key":"S0960129508006762_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129508006762_ref2","volume-title":"Compilers: Principles, Techniques and Tools","author":"Aho","year":"1988"},{"key":"S0960129508006762_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"S0960129508006762_ref4","first-page":"871","volume-title":"Springer-Verlag Lecture Notes in Computer Science","volume":"2719","author":"Ariola","year":"2003"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129508006762","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T00:43:14Z","timestamp":1557621794000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129508006762\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,6]]}},"alternative-id":["S0960129508006762"],"URL":"https:\/\/doi.org\/10.1017\/s0960129508006762","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,6]]}}}