To everyone who needs to contact me by email. Due to a change in the system, my official address (@uninsubria.it) is temporarily out of work. Please, use the gmail address!
I decided to open a new blog: marcobeniniphoto.wordpress.com. It does not contain any material about my academic work, nor about research. Instead it shows and discusses some of my photographs.
if you are interested, please, pay it a visit.
Yesterday, I gave a seminar in the Department of Philosophy in Florence.
If interested, here are the slides.
For those interested, I want to signal the workshop Foundation of Mathematics for Computer-Aided Formalization. I’ve just registered for participation.
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.
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!