Intuitionistic First-Order Logic: Categorical Semantics via the Curry-Howard Isomorphism

Marco Benini

This reports introduces a novel sound and complete semantics for first order intuitionistic logic, in the framework of category theory and by the computational interpretation of th…