POPL 2020 (series) / Research Papers / Taylor Subsumes Scott, Berry, Kahn and Plotkin
Taylor Subsumes Scott, Berry, Kahn and PlotkinDistinguished Paper
Fri 24 Jan 2020 15:35 - 15:56 at Ile de France II (IDF II) - Semantics & Type Theory Chair(s): Arthur Azevedo de Amorim
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.
Slides Talk (ManzonettoTalk.pdf) | 1.46MiB |
Fri 24 Jan Times are displayed in time zone: Saskatchewan, Central America change
Fri 24 Jan
Times are displayed in time zone: Saskatchewan, Central America change
15:35 - 16:40: Semantics & Type TheoryResearch Papers at Ile de France II (IDF II) Chair(s): Arthur Azevedo de AmorimCarnegie Mellon University, USA | |||
15:35 - 15:56 Talk | Taylor Subsumes Scott, Berry, Kahn and PlotkinDistinguished Paper Research Papers Link to publication DOI Media Attached File Attached | ||
15:56 - 16:18 Talk | Reduction Monads and Their Signatures Research Papers Benedikt AhrensUniversity of Birmingham, United Kingdom, André HirschowitzUniversité Côte d'Azur, Ambroise LafontInria, France, Marco MaggesiUniversità di Firenze Link to publication DOI Media Attached | ||
16:18 - 16:40 Talk | Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq Research Papers Matthieu SozeauInria, Simon BoulierInria, Yannick ForsterSaarland University, Nicolas TabareauInria, Théo WinterhalterInria — LS2N Link to publication DOI Media Attached File Attached |