Marco Benini


The Curry-Howard isomorphism relates lambda-calculus with intuitionistic logic. Essentially, it says that to every variant of intuitionistic logic (propositional vs predicative, first-order, second-order, weak higher-order, full higher-order) corresponds a typed lambda-calculus whose types are the formulae and whose terms are the proofs.

In this period, I’m looking at the categorical models of intuitionistic logics and at the categorical models of typed lambda-calculi. It is folklore that these models are the same. In fact, this is false: they are strictly related, but essentially different. And there are a few surprises…

Soon, I will write a draft on these topics. Stay tuned if interested!

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 )

Twitter picture

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

Facebook photo

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

Connecting to %s


This entry was posted on December 27, 2011 by in Category Theory, Mathematics, Papers, Topos Theory.
%d bloggers like this: