From the 1 of 6 linked papers with an AI index.
6 papers
Definitional Inversion, Without Normalisation
Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu +3
The paper presents a domain‑theoretic proof technique that establishes definitional inversion properties (injectivity and no‑confusion) of type constructors in dependent type syste…
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…
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…
The categorical contours of the Chomsky-Schützenberger representation theorem
Paul-André Melliès, Noam Zeilberger
We develop fibrational perspectives on context-free grammars and on nondeterministic finite-state automata over categories and operads. A generalized CFG is a functor from a free c…