{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:06:16Z","timestamp":1770293176224,"version":"3.49.0"},"reference-count":55,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2018,2,1]],"date-time":"2018-02-01T00:00:00Z","timestamp":1517443200000},"content-version":"unspecified","delay-in-days":31,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2018]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a model of computation that heavily emphasizes the concept of <jats:italic>duality<\/jats:italic> and the interaction between opposites\u2013production interacts with consumption. The symmetry of this framework naturally explains more complicated features of programming languages through relatively familiar concepts. For example, binding a value to a variable is dual to manipulating the flow of control in a program. By looking at the computational interpretation of the sequent calculus, we find a language that lets us speak about duality, control flow, and evaluation order in programs as first-class concepts.<\/jats:p><jats:p>We begin by reviewing Gentzen's LK sequent calculus and show how the Curry\u2013Howard isomorphism still applies to give us a different basis for expressing computation. We then illustrate how the fundamental dilemma of computation in the sequent calculus gives rise to a duality between <jats:italic>evaluation strategies<\/jats:italic>: strict languages are dual to lazy languages. Finally, we discuss how the concept of <jats:italic>focusing<\/jats:italic>, developed in the setting of proof search, is related to the idea of type safety for computation expressed in the sequent calculus. In this regard, we compare and contrast two different methods of focusing that have appeared in the literature, <jats:italic>static<\/jats:italic> and <jats:italic>dynamic<\/jats:italic> focusing, and illustrate how they are two means to the same end.<\/jats:p>","DOI":"10.1017\/s0956796818000023","type":"journal-article","created":{"date-parts":[[2018,2,1]],"date-time":"2018-02-01T01:04:20Z","timestamp":1517447060000},"source":"Crossref","is-referenced-by-count":12,"title":["A tutorial on computational classical logic and the sequent calculus"],"prefix":"10.1017","volume":"28","author":[{"given":"PAUL","family":"DOWNEN","sequence":"first","affiliation":[]},{"given":"ZENA M.","family":"ARIOLA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2018,2,1]]},"reference":[{"key":"S0956796818000023_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"S0956796818000023_ref34","unstructured":"Laurent O. (2002) \u00c9tude de la polarisation en logique. PhD thesis, Universit\u00e9 de la M\u00e9diterran\u00e9e - Aix-Marseille II."},{"key":"S0956796818000023_ref12","unstructured":"de Bruijn N. (1968) AUTOMATH, A Language for Mathematics. Technical Report 66-WSK-05, Technological University Eindhoven."},{"key":"S0956796818000023_ref36","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.22"},{"key":"S0956796818000023_ref16","unstructured":"Felleisen M. & Friedman D. P. (1986) Control operators, the SECD machine, and the \u03bb-calculus. In Proceedings of the IFIP TC 2\/WG2.2 Working Conference on Formal Descriptions of Programming Concepts Part III, pp. 193\u2013219."},{"key":"S0956796818000023_ref50","unstructured":"Singh S. , Peyton Jones S. , Norell U. , Pottier F. , Meijer E. , & McBride C. (2011) Sexy types\u2013-are we done yet? Software Summit. URL https:\/\/www.microsoft.com\/en-us\/research\/video\/sexy-types-are-we-done-yet\/."},{"key":"S0956796818000023_ref18","volume-title":"Declarative Continuations and Categorical Duality","author":"Filinski","year":"1989"},{"key":"S0956796818000023_ref43","unstructured":"Emmanuel P. (2004) Explicit Substitutions, Logic and Normalization. PhD thesis, Universit\u00e9 Paris-Diderot \u2013 Paris VII, Jun. 2004."},{"key":"S0956796818000023_ref46","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"key":"S0956796818000023_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"S0956796818000023_ref7","doi-asserted-by":"publisher","DOI":"10.2307\/1968337"},{"key":"S0956796818000023_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_68"},{"key":"S0956796818000023_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90093-S"},{"key":"S0956796818000023_ref30","unstructured":"Howard W. A. (1980) The formulae-as-types notion of constructions. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, pp. 479\u2013490. ISBN 0123490502. Unpublished manuscript of 1969."},{"key":"S0956796818000023_ref28","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. PhD thesis, Universit\u00e9 Paris 7, January 1995."},{"key":"S0956796818000023_ref53","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"S0956796818000023_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_30"},{"key":"S0956796818000023_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_15"},{"key":"S0956796818000023_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"S0956796818000023_ref31","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1010051815785","article-title":"Revised5 report on the algorithmic language Scheme","volume":"11","author":"Kelsey","year":"1998","journal-title":"Higher-Order and Symb. Comput."},{"key":"S0956796818000023_ref49","unstructured":"Selinger P. (2003) Some remarks on control categories, 2003. URL http:\/\/mathstat.dalca\/~selinger\/papers\/controlremarks.pdf. Unpublished Manuscript."},{"key":"S0956796818000023_ref2","volume-title":"Compiling with Continuations","author":"Appel","year":"1992"},{"key":"S0956796818000023_ref48","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950000311X"},{"key":"S0956796818000023_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201363"},{"key":"S0956796818000023_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36575-3_27"},{"key":"S0956796818000023_ref1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"S0956796818000023_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"S0956796818000023_ref10","volume-title":"Combinatory Logic","author":"Curry","year":"1958"},{"key":"S0956796818000023_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"S0956796818000023_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291179"},{"key":"S0956796818000023_ref22","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001328"},{"key":"S0956796818000023_ref26","unstructured":"Graham-Lengrand S. (2016) The Curry-Howard view of classical logic: A short introduction. Lecture Notes for the MPRI course on Curry-Howard correspondence for Classical Logic. URL http:\/\/www.lix.polytechnique.fr\/~lengrand\/Work\/Teaching\/MPRI\/Notes.pdf. Unpublished Manuscript."},{"key":"S0956796818000023_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"S0956796818000023_ref29","unstructured":"Herbelin H. (2005) C'est maintenant qu'on calcule : Au coeur de la dualit\u00e9. Habilitation thesis, Universit\u00e9 Paris 11, 2005."},{"key":"S0956796818000023_ref55","unstructured":"Zeilberger N. (2013) Polarity in proof theory and programming. Lecture Notes for the Summer School on Linear Logic and Geometry of Interaction in Torino, Italy. URL http:\/\/noamz.org\/talks\/logpolpro.pdf. Unpublished Manuscript."},{"key":"S0956796818000023_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"key":"S0956796818000023_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/10705424_20"},{"key":"S0956796818000023_ref40","unstructured":"Peyton Jones S. , Tolmach A. & Hoare T. (2001) Playing by the rules: Rewriting as a practical optimisation technique in GHC. In Haskell Workshop 2001. ACM SIGPLAN."},{"key":"S0956796818000023_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013061"},{"key":"S0956796818000023_ref47","doi-asserted-by":"crossref","unstructured":"Scherer G. (2016) Which Types Have a Unique Inhabitant? Focusing on Pure Program Equivalence. PhD thesis, Universit\u00e9 Paris-Diderot.","DOI":"10.1145\/2784731.2784757"},{"key":"S0956796818000023_ref41","unstructured":"Pfenning F. (2010a) Lecture notes on focusing. Lecture notes for the Oregon Programming Languages Summer School 2010 course on Proof Theory Foundations, Lecture 4. URL http:\/\/www.cs.cmu.edu\/~fp\/courses\/oregon-m10\/04-focusing.pdf. Unpublished Manuscript."},{"key":"S0956796818000023_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0956796818000023_ref42","unstructured":"Pfenning F. (2010b) Lecture notes on sequent calculus. Lecture Notes for the Carnegie Mellon University course 15-816 on Modal Logic, Lecture 8. URL http:\/\/www.cs.cmu.edu\/~fp\/courses\/15816-s10\/lectures\/08-seqcalc.pdf. Unpublished Manuscript."},{"key":"S0956796818000023_ref44","unstructured":"Reynolds J. C. (1983) Types, abstraction and parametric polymorphism. In Proceedings of the IFIP 9th World Computer Congress, Information Processing 83. Amsterdam: Elsevier Science Publishers B. V. (North-Holland), pp. 513\u2013523."},{"key":"S0956796818000023_ref25","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0956796818000023_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019459"},{"key":"S0956796818000023_ref54","unstructured":"Zeilberger N. (2009) The Logical Basis of Evaluation Order and Pattern-Matching. PhD thesis, Carnegie Mellon University."},{"key":"S0956796818000023_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15240-5_13"},{"key":"S0956796818000023_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21691-6_6"},{"key":"S0956796818000023_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_14"},{"key":"S0956796818000023_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1516507.1516508"},{"key":"S0956796818000023_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950100336X"},{"key":"S0956796818000023_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784762"},{"key":"S0956796818000023_ref51","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944723"},{"key":"S0956796818000023_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951931"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796818000023","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T14:31:33Z","timestamp":1559831493000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796818000023\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"references-count":55,"alternative-id":["S0956796818000023"],"URL":"https:\/\/doi.org\/10.1017\/s0956796818000023","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"article-number":"e3"}}