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.

## Problems with email

November 19, 2013To 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!

## Point-free semantics

July 2, 2013Following the Marie Curie Fellowship in Leeds which ended in March, I have finished to write the long and complex report about my findings in that sabbatical period. The report now is available at ArXiv.org for those who are interested.

Any comment is welcome.

## New blog

June 30, 2013I 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.

## Seminario a Firenze

April 20, 2013Yesterday, I gave a seminar in the Department of Philosophy in Florence.

If interested, here are the slides.

## Workshop

November 28, 2012For those interested, I want to signal the workshop Foundation of Mathematics for Computer-Aided Formalization. I’ve just registered for participation.

## Curry-Howard II

November 22, 2012A 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.