Publications

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 …