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: 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
Research Papers
Davide BarbarossaUniversité Paris 13, Giulio ManzonettoUniversité Paris 13
Link to publication DOI Media Attached File Attached
15:56 - 16:18
Talk
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
Research Papers
Matthieu SozeauInria, Simon BoulierInria, Yannick ForsterSaarland University, Nicolas TabareauInria, Théo WinterhalterInria — LS2N
Link to publication DOI Media Attached File Attached