Workshop in Genoa

February 3, 2014

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, 2013

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!


Point-free semantics

July 2, 2013

Following 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, 2013

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.


Seminario a Firenze

April 20, 2013

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

If interested, here are the slides.


Workshop

November 28, 2012

For 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, 2012

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.


Follow

Get every new post delivered to your Inbox.

Join 258 other followers