TYPES

This was the continuation of the FP5 project with the same name, building on the strong collaboration and achievements in four successful European projects (ESPRIT BRA and Working Group), in which we built several computer systems for proof development (e.g. Coq, Isabelle, etc.) and used them in applications. The theory and the associated systems developed by consortium members define the state of the art in type theory and its applications. Some impressive examples using these systems have been achieved. However, it is a long-term project to make this technology suitable for use by engineers, mathematicians and students. The proposed Coordination Action maintained our community so that sites doing related and complementary work could continue to communicate and collaborate fruitfully.

More details on the CORDIS web page of the project

Among many activities, I chaired the TYPES 2007 conference, which was held in Cividale del Friuli, near Udine. It was a cool project indeed.