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

Displayed 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 Amorim Carnegie Mellon University, USA
15:35
21m
Talk
Taylor Subsumes Scott, Berry, Kahn and PlotkinDistinguished Paper
Research Papers
Davide Barbarossa Université Paris 13, Giulio Manzonetto Université Paris 13
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
Reduction Monads and Their Signatures
Research Papers
Benedikt Ahrens University of Birmingham, United Kingdom, André Hirschowitz Université Côte d'Azur, Ambroise Lafont Inria, France, Marco Maggesi Università di Firenze
Link to publication DOI Media Attached
16:18
21m
Talk
Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
Research Papers
Matthieu Sozeau Inria, Simon Boulier Inria, Yannick Forster Saarland University, Nicolas Tabareau Inria, Théo Winterhalter Inria — LS2N
Link to publication DOI Media Attached File Attached