80 citations · 114 across the 20 of their papers we have counts for
26 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…
Syntax and semantics of focalisation with relative monads and comonads
Éléonore Mangel, Paul-André Melliès, Guillaume Munch-Maccagnoni
The logical principles of focalisation and polarisation can be used to design well-behaved term syntaxes for sequent calculus, which play a role as meta-languages for describing ef…
Definitional Inversion, Without Normalisation
Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu +3
We contribute a new proof technique, based on domain theory, to prove key meta-theoretic properties of dependent type systems: definitional inversion properties, i.e. injectivity a…
The Latent Space of Equational Theories
Luis Berlioz, Paul-André Melliès
Building on the collaborative Equational Theories project initiated by Terence Tao fifteen months ago, and combining it with ideas coming from machine learning and finite model the…
A cartesian closed fibration of higher-order regular languages
Paul-André Melliès, Vincent Moreau
We explain how to construct in two different ways a cartesian closed fibration of higher-order regular languages in the sense of Salvati. In the first construction, we use fibratio…
Classical notions of computation and the Hasegawa-Thielecke theorem (extended version)
Éléonore Mangel, Paul-André Melliès, Guillaume Munch-Maccagnoni
In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involut…