LaTeXing proofs

December 2, 2014

I’ve written a LaTeX package to typeset proofs in natural deduction and similar systems.
In some ways, it improves the existing packages by adding a new feature: the ability to reference assumptions in a proof and the ability to create and reference “proof summaries”.

If you want to have a look, it is available at CTAN.

Time for a change

October 16, 2014

Now it is official: from November 1st, 2014, I will be a mathematical logician in the Dipartimento di Scienza e Alta Tecnologia, Università degli Studi dell’Insubria, part of the mathematical group.

As it is clear from my experience, I have always worked in the borderline between mathematics and computer science, specifically between logic and computability. Of course, in my not so short career, I did many things, but the centre of my research was there.

Today, I am more on the mathematical side. And, since I am, officially, a computer scientist working in a computer science department, there is a problem. Moreover, my current department focuses on technology and applications: a wise decision, considering that it operates in a region where many small industries are present, and there is a relevant demand for high-trained technicians. But that’s not something I can really contribute to.

So, I moved both my official sector and my academic affiliation. The result will be effective in a couple of weeks. Then, I will change the relevant data in the website.

Visiting JAIST

May 28, 2014

Currently, I’m in the Japanese Advanced Institute of Science and Technology, kindly hosted by Prof. H. Ishihara and Dr. T. Nemoto, as part of the CORCON research project.

In this period, I am going to work on formalising equality in a deep sense inside logically distributive categories, and to relate them with computation through type theory.

During this period, I will give a couple of seminars to the logic group in JAIST: one about logical distributive categories as a point-free foundation of mathematics, and one about the computation modulo a function. Both seminars are strictly related to the research I’m conducting here.

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 ( 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 for those who are interested.

Any comment is welcome.

New blog

June 30, 2013

I decided to open a new blog: 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.


Get every new post delivered to your Inbox.

Join 270 other followers