Publications

Fo-bicategories are a categorification of Peirce’s calculus of relations. Notably, their laws provide a proof system for …

We provide a new description of Joyal’s arithmetic universes through a characterization of the exact and regular completions of …

Implicative algebras have been recently introduced by Miquel in order to provide a unifying notion of model, encompassing the most …

Temporal logics stands for a widely adopted family of formalisms forthe verification of computational devices, enriching propositional …

Originally introduced in the context of the algebraic approach to term graph rewriting, the notion of gs-monoidal category has surfaced …

Introduced in the 1990s in the context of the algebraic approach to graph rewriting, gs-monoidal categories are symmetric monoidal …

We present a first-order linear-time temporal logic for reasoning about the evolution of directed graphs. Its semantics is based on the …

Gödel’s Dialectica interpretation was conceived as a tool to obtain the consistency of Heyting arithmetic in the 40s. In recent …

This paper aims to provide an intrinsic characterization of the notion of generalized existential completion of a conjunctive doctrine …

Gödel’s Dialectica interpretation was designed to obtain the consistency of Peano arithmetic via a proof of consistency of …

Gödel’s Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in …

We introduce the notion of a Gödel fibration, which is a fibration categorically embodying both the logical principles of traditional …

We determine the existential completion of a primary doctrine, and we prove that the 2-monad obtained from it is lax-idempotent, and …