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.

Barbarossa D., Manzonetto G. (2020). Taylor subsumes Scott, Berry, Kahn and Plotkin. PROCEEDINGS OF ACM ON PROGRAMMING LANGUAGES, 4(POPL), 1-23 [10.1145/3371069].

Taylor subsumes Scott, Berry, Kahn and Plotkin

Barbarossa D.
;
2020

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.
2020
Barbarossa D., Manzonetto G. (2020). Taylor subsumes Scott, Berry, Kahn and Plotkin. PROCEEDINGS OF ACM ON PROGRAMMING LANGUAGES, 4(POPL), 1-23 [10.1145/3371069].
Barbarossa D.; Manzonetto G.
File in questo prodotto:
File Dimensione Formato  
3371069.pdf

accesso aperto

Tipo: Versione (PDF) editoriale / Version Of Record
Licenza: Licenza per Accesso Aperto. Creative Commons Attribuzione (CCBY)
Dimensione 411.39 kB
Formato Adobe PDF
411.39 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/916695
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 21
  • ???jsp.display-item.citation.isi??? 13
social impact