{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T05:59:55Z","timestamp":1770271195698,"version":"3.49.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"DFG","award":["OS 293\/5-1"],"award-info":[{"award-number":["OS 293\/5-1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"<jats:p>\n            Functional programming language design has been shaped by the framework of natural deduction, in which language constructs are divided into introduction and elimination rules for\n            <jats:italic>producers<\/jats:italic>\n            of values. In sequent calculus-based languages, left introduction rules replace (right) elimination rules and provide a dedicated sublanguage for\n            <jats:italic>consumers<\/jats:italic>\n            of values. In this paper, we present and analyze a wider design space of programming languages which encompasses four kinds of rules: Introduction and elimination, both left and right. We analyze the influence of rule choice on program structure and argue that having all kinds of rules enriches a programmer\u2019s modularity arsenal. In particular, we identify four ways of adhering to the principle that \u201dthe structure of the program follows the structure of the data\u201c and show that they correspond to the four possible choices of rules. We also propose the principle of\n            <jats:italic>bi-expressibility<\/jats:italic>\n            to guide and validate the design of rules for a connective. Finally, we deepen the well-known dualities between different connectives by means of the proof\/refutation duality.\n          <\/jats:p>","DOI":"10.1145\/3547637","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"438-465","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Introduction and elimination, left and right"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5294-5506","authenticated-orcid":false,"given":"Klaus","family":"Ostermann","sequence":"first","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1272-0972","authenticated-orcid":false,"given":"David","family":"Binder","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8320-8445","authenticated-orcid":false,"given":"Ingo","family":"Skupin","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8709-6321","authenticated-orcid":false,"given":"Tim","family":"S\u00fcberkr\u00fcb","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0165-9387","authenticated-orcid":false,"given":"Paul","family":"Downen","sequence":"additional","affiliation":[{"name":"University of Massachusetts at Lowell, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429075"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371098"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2012","volume":"108","author":"Carraro Alberto","year":"2012","unstructured":"Alberto Carraro , Thomas Ehrhard , and Antonino Salibra . 2012 . The stack calculus . In Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2012 , Rio de Janeiro, Brazil , September 29-30, 2012 (EPTCS, Vol. 113). 93\u2013 108 . https:\/\/doi.org\/10.48550\/arXiv.1303.7331 Alberto Carraro, Thomas Ehrhard, and Antonino Salibra. 2012. The stack calculus. In Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2012, Rio de Janeiro, Brazil, September 29-30, 2012 (EPTCS, Vol. 113). 93\u2013108. https:\/\/doi.org\/10.48550\/arXiv.1303.7331"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.4.529"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/357766.351262"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_14"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000023"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2021.1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_5"},{"key":"e_1_2_1_12_1","volume-title":"Matthew Flatt, and Shriram Krishnamurthi.","author":"Felleisen Matthias","year":"2001","unstructured":"Matthias Felleisen , Robert Bruce Findler , Matthew Flatt, and Shriram Krishnamurthi. 2001 . How to Design Programs. An Introduction to Computing and Programming. The MIT Press , Cambridge, Massachusetts London, England. Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. 2001. How to Design Programs. An Introduction to Computing and Programming. The MIT Press, Cambridge, Massachusetts London, England."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000113"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58216-9_27"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80065-3"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328484"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614964"},{"key":"e_1_2_1_20_1","unstructured":"William Lovas and Karl Crary. 2006. Structural Normalization for Classical Natural Deduction. Draft. \t\t\t\t  William Lovas and Karl Crary. 2006. Structural Normalization for Classical Natural Deduction. Draft."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_30"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_24"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021264102972"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6685674"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_3"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55460-2_27"},{"key":"e_1_2_1_28_1","volume-title":"\u03bb \u03bc -Calculus: An algorithmic interpretation of classical natural deduction","author":"Parigot Michel","unstructured":"Michel Parigot . 1992. \u03bb \u03bc -Calculus: An algorithmic interpretation of classical natural deduction . In Logic Programming and Automated Reasoning, Andrei Voronkov (Ed.). Springer , Berlin, Heidelberg . 190\u2013201. Michel Parigot. 1992. \u03bb \u03bc -Calculus: An algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning, Andrei Voronkov (Ed.). Springer, Berlin, Heidelberg. 190\u2013201."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_1_30_1","volume-title":"Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell","author":"Prawitz Dag","year":"1965","unstructured":"Dag Prawitz . 1965 . Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell , Stockholm. Reprinted Mineola NY : Dover Publications ( 2006) Dag Prawitz. 1965. Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell, Stockholm. Reprinted Mineola NY: Dover Publications (2006)"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02120864"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784763"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.48"},{"key":"e_1_2_1_35_1","volume-title":"The Stanford Encyclopedia of Philosophy (Spring 2018 ed.), Edward N","author":"Schroeder-Heister Peter","unstructured":"Peter Schroeder-Heister . 2018. Proof-Theoretic Semantics . In The Stanford Encyclopedia of Philosophy (Spring 2018 ed.), Edward N . Zalta (Ed.). Metaphysics Research Lab, Stanford University . Peter Schroeder-Heister. 2018. Proof-Theoretic Semantics. In The Stanford Encyclopedia of Philosophy (Spring 2018 ed.), Edward N. Zalta (Ed.). Metaphysics Research Lab, Stanford University."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016848.1016864"},{"key":"e_1_2_1_37_1","unstructured":"Arnaud Spiwack. 2014. A Dissection of L. Unpublished draft \t\t\t\t  Arnaud Spiwack. 2014. A Dissection of L. Unpublished draft"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-012-9417-8"},{"key":"e_1_2_1_39_1","unstructured":"Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods. North-Holland. \t\t\t\t  Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods. North-Holland."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944723"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_15"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364568"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.01.001"},{"key":"e_1_2_1_44_1","volume-title":"The Logical Basis of Evaluation Order and Pattern-Matching. Ph. D. Dissertation","author":"Zeilberger Noam","unstructured":"Noam Zeilberger . 2009. The Logical Basis of Evaluation Order and Pattern-Matching. Ph. D. Dissertation . Carnegie Mellon University . USA. isbn:9781109163018 Noam Zeilberger. 2009. The Logical Basis of Evaluation Order and Pattern-Matching. Ph. D. Dissertation. Carnegie Mellon University. USA. isbn:9781109163018"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547637","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547637","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547637"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":44,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547637"],"URL":"https:\/\/doi.org\/10.1145\/3547637","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}