Taylor subsumes Scott, Berry, Kahn and Plotkin

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 λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple...

Full description

Saved in:
Bibliographic Details
Published in:Proceedings of ACM on programming languages 2020-01, Vol.4 (POPL), p.1-23
Main Authors: Barbarossa, Davide, Manzonetto, Giulio
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c258t-fcf39627c0c4d031cd5a853dbc71c6f02579e44b7c2718ec864e71b3565eb6c83
cites cdi_FETCH-LOGICAL-c258t-fcf39627c0c4d031cd5a853dbc71c6f02579e44b7c2718ec864e71b3565eb6c83
container_end_page 23
container_issue POPL
container_start_page 1
container_title Proceedings of ACM on programming languages
container_volume 4
creator Barbarossa, Davide
Manzonetto, Giulio
description 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 λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott’s continuity, Berry’s stability or Kahn and Plotkin’s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.
doi_str_mv 10.1145/3371069
format article
fullrecord <record><control><sourceid>crossref</sourceid><recordid>TN_cdi_crossref_primary_10_1145_3371069</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>10_1145_3371069</sourcerecordid><originalsourceid>FETCH-LOGICAL-c258t-fcf39627c0c4d031cd5a853dbc71c6f02579e44b7c2718ec864e71b3565eb6c83</originalsourceid><addsrcrecordid>eNpNj8tKAzEUQIMoWGrxF7Jz06m5uXnNUosvLChY10NyJ8HqdEaS6WL-XsQuXJ2zOnAYuwSxAlD6GtGCMPUJm0lldQVKwuk_P2eLUj6FEFCjcljP2Grrp27IvBxCOexj4W80jOOS38acpyV_9h89933LX7th_Nr1F-ws-a7ExZFz9n5_t10_VpuXh6f1zaYiqd1YJUpYG2lJkGoFArXaO41tIAtkkpDa1lGpYElacJGcUdFCQG10DIYcztnVX5fyUEqOqfnOu73PUwOi-T1tjqf4AztXQzc</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype></control><display><type>article</type><title>Taylor subsumes Scott, Berry, Kahn and Plotkin</title><source>ACM Digital Library</source><creator>Barbarossa, Davide ; Manzonetto, Giulio</creator><creatorcontrib>Barbarossa, Davide ; Manzonetto, Giulio</creatorcontrib><description>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 λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott’s continuity, Berry’s stability or Kahn and Plotkin’s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.</description><identifier>ISSN: 2475-1421</identifier><identifier>EISSN: 2475-1421</identifier><identifier>DOI: 10.1145/3371069</identifier><language>eng</language><ispartof>Proceedings of ACM on programming languages, 2020-01, Vol.4 (POPL), p.1-23</ispartof><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c258t-fcf39627c0c4d031cd5a853dbc71c6f02579e44b7c2718ec864e71b3565eb6c83</citedby><cites>FETCH-LOGICAL-c258t-fcf39627c0c4d031cd5a853dbc71c6f02579e44b7c2718ec864e71b3565eb6c83</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,780,784,27924,27925</link.rule.ids></links><search><creatorcontrib>Barbarossa, Davide</creatorcontrib><creatorcontrib>Manzonetto, Giulio</creatorcontrib><title>Taylor subsumes Scott, Berry, Kahn and Plotkin</title><title>Proceedings of ACM on programming languages</title><description>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 λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott’s continuity, Berry’s stability or Kahn and Plotkin’s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.</description><issn>2475-1421</issn><issn>2475-1421</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2020</creationdate><recordtype>article</recordtype><recordid>eNpNj8tKAzEUQIMoWGrxF7Jz06m5uXnNUosvLChY10NyJ8HqdEaS6WL-XsQuXJ2zOnAYuwSxAlD6GtGCMPUJm0lldQVKwuk_P2eLUj6FEFCjcljP2Grrp27IvBxCOexj4W80jOOS38acpyV_9h89933LX7th_Nr1F-ws-a7ExZFz9n5_t10_VpuXh6f1zaYiqd1YJUpYG2lJkGoFArXaO41tIAtkkpDa1lGpYElacJGcUdFCQG10DIYcztnVX5fyUEqOqfnOu73PUwOi-T1tjqf4AztXQzc</recordid><startdate>202001</startdate><enddate>202001</enddate><creator>Barbarossa, Davide</creator><creator>Manzonetto, Giulio</creator><scope>AAYXX</scope><scope>CITATION</scope></search><sort><creationdate>202001</creationdate><title>Taylor subsumes Scott, Berry, Kahn and Plotkin</title><author>Barbarossa, Davide ; Manzonetto, Giulio</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c258t-fcf39627c0c4d031cd5a853dbc71c6f02579e44b7c2718ec864e71b3565eb6c83</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2020</creationdate><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Barbarossa, Davide</creatorcontrib><creatorcontrib>Manzonetto, Giulio</creatorcontrib><collection>CrossRef</collection><jtitle>Proceedings of ACM on programming languages</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Barbarossa, Davide</au><au>Manzonetto, Giulio</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Taylor subsumes Scott, Berry, Kahn and Plotkin</atitle><jtitle>Proceedings of ACM on programming languages</jtitle><date>2020-01</date><risdate>2020</risdate><volume>4</volume><issue>POPL</issue><spage>1</spage><epage>23</epage><pages>1-23</pages><issn>2475-1421</issn><eissn>2475-1421</eissn><abstract>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 λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott’s continuity, Berry’s stability or Kahn and Plotkin’s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.</abstract><doi>10.1145/3371069</doi><tpages>23</tpages><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 2475-1421
ispartof Proceedings of ACM on programming languages, 2020-01, Vol.4 (POPL), p.1-23
issn 2475-1421
2475-1421
language eng
recordid cdi_crossref_primary_10_1145_3371069
source ACM Digital Library
title Taylor subsumes Scott, Berry, Kahn and Plotkin
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-01T07%3A22%3A07IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-crossref&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Taylor%20subsumes%20Scott,%20Berry,%20Kahn%20and%20Plotkin&rft.jtitle=Proceedings%20of%20ACM%20on%20programming%20languages&rft.au=Barbarossa,%20Davide&rft.date=2020-01&rft.volume=4&rft.issue=POPL&rft.spage=1&rft.epage=23&rft.pages=1-23&rft.issn=2475-1421&rft.eissn=2475-1421&rft_id=info:doi/10.1145/3371069&rft_dat=%3Ccrossref%3E10_1145_3371069%3C/crossref%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c258t-fcf39627c0c4d031cd5a853dbc71c6f02579e44b7c2718ec864e71b3565eb6c83%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rfr_iscdi=true