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!