Write a Blog >>

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: (GMT-06:00) Saskatchewan, Central America change

POPL-2020-Research-Papers
15:35 - 16:40: Research Papers - Semantics & Type Theory at Ile de France II (IDF II)
Chair(s): Arthur Azevedo de AmorimCarnegie Mellon University, USA
POPL-2020-Research-Papers15:35 - 15:56
Talk
Davide BarbarossaUniversité Paris 13, Giulio ManzonettoUniversité Paris 13
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers15:56 - 16:18
Talk
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
POPL-2020-Research-Papers16:18 - 16:40
Talk
Matthieu SozeauInria, Simon BoulierInria, Yannick ForsterSaarland University, Nicolas TabareauInria, Théo WinterhalterInria — LS2N
Link to publication DOI Media Attached File Attached