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.| 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.


