In March I will be in Genoa for the “Correctness by Construction – CORCON 2014” meeting. In this workshop, part of the CORCON project, I am one of the organisers and I will give a keynote talk.
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.