Marco Benini

Curry-Howard

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!

Advertisements

Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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 )

Google+ photo

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

Connecting to %s

Information

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