Curry-Howard II

A few days ago, I gave a talk in the Logic Seminar at Leeds. The slides are available at leeds14102012.

Essentially, it shows a semantics for full first-order intuitionistic logic in category theory. It also shows a semantics for the corresponding lambda-calculus.

The relation between the two semantics is exactly the Curry-Howard isomorphisms, which is not surprising.

The surprise is that the semantics is point-free, that is, no universe is needed to interpret terms. Or better, terms are not interpreted as elements but, rather, they generate a structure that keeps together the category where formulae and proofs are interpreted. This resembles somewhat Formal Topology (in more than one way, to say the truth).

In the immediate future, I want to relate this semantics with the one based on Heyting categories, and also with the Kripke-Joyal semantics which is based on Grothendieck topoi.