Marco Benini

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.

Leave a Reply

Please log in using one of these methods to post your comment: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s


This entry was posted on November 22, 2012 by in Category Theory, Mathematics, Seminars, Topos Theory.
%d bloggers like this: