{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T17:45:16Z","timestamp":1778262316359,"version":"3.51.4"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential \u03bb-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in \u03bb-calculus that are usually demonstrated by exploiting Scott\u2019s continuity, Berry\u2019s stability or Kahn and Plotkin\u2019s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the B\u00f6hm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.<\/jats:p>","DOI":"10.1145\/3371069","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Taylor subsumes Scott, Berry, Kahn and Plotkin"],"prefix":"10.1145","volume":"4","author":[{"given":"Davide","family":"Barbarossa","sequence":"first","affiliation":[{"name":"University of Paris 13, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giulio","family":"Manzonetto","sequence":"additional","affiliation":[{"name":"University of Paris 13, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.10.003"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236789"},{"key":"e_1_2_2_3_1","volume-title":"3rd International Workshop on Trends in Linear Logic and Applications.","author":"Barbarossa Davide","year":"2019"},{"key":"e_1_2_2_4_1","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"90","author":"Barendregt Henk P.","year":"1977"},{"key":"e_1_2_2_5_1","unstructured":"Henk P. Barendregt. 1984. The lambda-calculus its syntax and semantics (revised ed.). Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland.  Henk P. Barendregt. 1984. The lambda-calculus its syntax and semantics (revised ed.). Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland."},{"key":"e_1_2_2_6_1","article-title":"Automatic Differentiation in Machine Learning: a Survey","volume":"18","author":"Baydin Atilim Gunes","year":"2017","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_2_2_7_1","volume-title":"ICALP (Lecture Notes in Computer Science)","author":"Berry G\u00e9rard"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005676"},{"key":"e_1_2_2_9_1","first-page":"622","article-title":"Cartesian differential categories","volume":"22","author":"Blute Richard","year":"2009","journal-title":"Theory and Applications of Categories"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_1"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.008"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10485-013-9312-0"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000014"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000396"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003729"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2012.259"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000372"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2967973.2968608"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00392-X"},{"key":"e_1_2_2_20_1","volume-title":"CiE (Lecture Notes in Computer Science)","author":"Ehrhard Thomas"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.003"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.06.001"},{"key":"e_1_2_2_23_1","volume-title":"Probabilistic call by push value. Logical Methods in Computer Science 15, 1","author":"Ehrhard Thomas","year":"2019"},{"key":"e_1_2_2_24_1","volume-title":"19th International Conference, RTA 2008 (Lecture Notes in Computer Science), Andrei Voronkov (Ed.)","volume":"5117","author":"Endrullis J\u00f6rg"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1080\/10556788.2017.1333613"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1112\/jlms\/jdm096"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785809"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1080\/10556788.2017.1378653"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.292.2"},{"key":"e_1_2_2_30_1","volume-title":"A syntactic characterization of the equality in some models for the \u03bb-calculus","author":"Hyland Martin","year":"1975"},{"key":"e_1_2_2_31_1","first-page":"62","article-title":"A Tutorial on (Co)Algebras and (Co)Induction","volume":"62","author":"Jacobs Bart","year":"1997","journal-title":"EATCS Bulletin"},{"key":"e_1_2_2_33_1","volume-title":"Revisiting Call-by-value B\u00f6hm trees in light of their Taylor expansion. CoRR abs\/1809.02659","author":"Kerinec Emma","year":"2018"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000493"},{"key":"e_1_2_2_35_1","volume-title":"RTA (Lecture Notes in Computer Science)","author":"Kuper Jan"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.13"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2012012"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.36"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80083-5"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209126"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.3.373"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03816-7_49"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.10.014"},{"key":"e_1_2_2_45_1","volume-title":"Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics","volume":"133","author":"Nederpelt Rob P."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535879"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000316"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.2307\/2272645"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_2_50_1","volume-title":"Toposes, Algebraic Geometry and Logic (Lecture Notes in Mathematics)","author":"Scott Dana S."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003548"},{"key":"e_1_2_2_52_1","volume-title":"Logic, Language and Computation (Lecture Notes in Computer Science)","author":"Takahashi Masako"},{"key":"e_1_2_2_53_1","doi-asserted-by":"crossref","unstructured":"Takeshi Tsukada Kazuyuki Asada and C.-H. Luke Ong. 2018. Species Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic Probabilistic and Quantum Programs. In LICS. ACM 889\u2013898.  Takeshi Tsukada Kazuyuki Asada and C.-H. Luke Ong. 2018. Species Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic Probabilistic and Quantum Programs. In LICS. ACM 889\u2013898.","DOI":"10.1145\/3209108.3209157"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509990089"},{"key":"e_1_2_2_56_1","volume-title":"Normalizing the Taylor expansion of non-deterministic \u03bb-terms, via parallel reduction of resource vectors. Logical Methods in Computer Science","author":"Vaux Lionel","year":"2019"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205036"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jocs.2011.10.007"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371069","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371069","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:42Z","timestamp":1750273542000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371069"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":56,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371069"],"URL":"https:\/\/doi.org\/10.1145\/3371069","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}