Lison Blondeau-Patissier
I2M & LIS, Aix-Marseille
Date(s) : 29/06/2023 iCal
10 h 30 min - 11 h 15 min
As shown by Tsukada and Ong, normal (extensional) simply-typed resource terms correspond to plays
in Hyland-Ong games, quotiented by Melliès’ homotopy equivalence. Though inspiring, their proof
is indirect, relying on the injectivity of the relational model w.r.t. both sides of the correspondence —
in particular, the dynamics of the resource calculus is taken into account only via the compatibility
of the relational model with the composition of normal terms defined by normalization.
We revisit and extend these results. Our first contribution is to restate
the correspondence by considering causal structures we call augmentations, which are canonical
representatives of Hyland-Ong plays up to homotopy. This allows us to give a direct and explicit
account of the connection with normal resource terms. As a second contribution, we extend this
account to the reduction of resource terms: building on a notion of strategies as weighted sums of
augmentations, we provide a denotational model of the resource calculus, invariant under reduction.
A key step — and our third contribution — is a categorical model we call a resource category, which
is to the resource calculus what differential categories are to the differential λ-calculus.
Emplacement
Amphi 5 - TPR2 (room 500-504, fifth floor)
Catégories