1 citations · 2 across the 6 of their papers we have counts for
9 papers
An explicit shuffle construction of the homotopy span model of differential linear logic
Paul-André Melliès, Federico Olimpieri, Lionel Vaux Auclair
We give a direct and explicit construction of the homotopy span model of linear logic originally formulated by Melliès using abstract homotopy theory in the Quillen category Cat of…
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…
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…
Canonicity of Proofs in Constructive Modal Logic
Matteo Acclavio, Davide Catta, Federico Olimpieri
In this paper we investigate the Curry-Howard correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the…
Coherence by Normalization for Linear Multicategorical Structures
Federico Olimpieri
We establish a formal correspondence between resource calculi an appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autono…
From Thin Concurrent Games to Generalized Species of Structures (Extended Version)
Pierre Clairambault, Federico Olimpieri, Hugo Paquet
Two families of denotational models have emerged from the semantic analysis of linear logic: dynamic models, typically presented as game semantics, and static models, typically bas…
On the Taylor expansion of -terms and the groupoid structure of their rigid approximants
Federico Olimpieri, Lionel Vaux Auclair
We show that the normal form of the Taylor expansion of a -term is isomorphic to its Böhm tree, improving Ehrhard and Regnier's original proof along three independent directions…
Intersection Type Distributors
Federico Olimpieri
We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduc…
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…