Évènement

Federico Olimpieri
LIS, Aix-Marseille
https://www.federicolimpieri.it/~olimpieri/

Date(s) : 25/09/2025   iCal
11h00 - 12h30

We introduce the structural resource λ-calculus, a new formalism in
which strongly normalizing terms of the λ-calculus can naturally be
represented, and at the same time any type derivation can be rewritten
to its linearization. The calculus is shown to be normalizing and
confluent. Noticeably, every strongly normalizable λ-term can be
represented by a type derivation. This is the first example of a system
where the linearization process takes place internally, while remaining
purely finitary and rewrite-based. We conclude by showing how our
linearization procedure bridges semantic and syntactic approaches to
program approximation, yielding new proof techniques and insights.

Emplacement
Luminy - LIS, salle 04.05

Catégories

• Séminaire