3 papers
cs.LO2025
Linearization via Rewriting (Long Version)
Ugo Dal Lago, Federico Olimpieri
We introduce the structural resource lambda-calculus, a new formalism in which strongly normalizing terms of the lambda-calculus can naturally be represented, and at the same time…
cs.LO2024
An Indexed Linear Logic for Idempotent Intersection Types (Long version)
Flavien Breuvart, Federico Olimpieri
Indexed Linear Logic has been introduced by Ehrhard and Bucciarelli, it can be seen as a logical presentation of non-idempotent intersection types extended through the relational s…
cs.LO2020
Normalization, Taylor expansion and rigid approximation of -terms
Federico Olimpieri
The aim of this work is to characterize three fundamental normalization proprieties in lambda-calculus trough the Taylor expansion of -terms. The general proof strategy consist…