The work of the master thesis was a major change in my interests, and gave me the opportunity of meeting Corrado Boehm, who shortly after became the advisor of my PhD course in Computer Science, starting in 1989. Beside to the advisor, who trusted me by opening my mind to a new world, I am indepted to Gianfranco Mascari and Adolfo Piperno, who were of great help to me.
It was at that time that I met Richard Statman, while he was visiting Rome University. Discussing with him and Adolfo Piperno, it appeared that some unpublished results by Statman could throw a new light on our attempts to attack the problem of characterizing provable retractions among simple types. This led to our LICS'92 paper, which ramains one of the best works I have coauthored.
I got my PhD in 1992, by defending a thesis entitled: "Non-deterministic untyped λ-calculus. A study about explicit non-determinism in higher order functional calculi", which was refereed by Jan Willem Klop and Rocco De Nicola with favour. The thesis was inspired by the work by Gerard Boudol, who showed to me the richness of the lattice model of the untyped λ-calculus and the possibilities of its description using intersection types, after Abramsky's work on logical description of domains. The thesis took its definite form after reading Moggi's work on monads, and I also profited of Eugenio's remarks on a preliminary version of a paper sketching the thesis content.
In 1993 I left Rome to Turin, to work with Mariangiola Dezani on intersection and union types, both for pure λ-calculus, togather with Franco Barbanera, and for certain non-deterministic and parallel extensions of it, I had partly conisdered in my PhD thesis. My personal view on this work is that union types are better suited to describe non sequential and non deterministic extensions of the λ-calculus rather than the λ-calculus itself, with the possible exception of introducing aspects of abstract interpretation in the type assignment systems for prototipical programming languages, as Jensen showed shortly thereafter.
A postdoc grant of EEC allowed me to visit Giuseppe Longo at Ecole Normale Superieur in Paris, starting with late 1994 until the end of 1995. I devoted that year to study the recursive models of the lambda-calculus, and I wrote a report about the fully-abstract model of PCF by O'Hearn and Ritchie, which was based on logical relations over Kripke style lambda-models. This was not an original work of mines, rather a concrete exposition of the otherwise abstract construction proposed by the authors.
In 1996 I turned back to Turin, where I had got a permanent position as researcher. The subsequent years have been devoted to developing a denotational foundation of typing and subtyping of object calculi, based on intersection types. More precisely I have been working on a λ-calculus with records and on Abadi and Cardelli's ς-calculus. Working on this I have profited of Steffen van Bakel experience on intersection types.
In 2001 I have been appointed as Associate Professor in Computer Science at the University of Turin.
In 2007 I coauthored a paper on progress in the π-calculus with session types, togather with Dezani and Yoshida. This was the starting point of a new research line on type systems for Milner's π-calculus, and expecially session types porposed by Honda et alii. Presently I am developing related ideas togather with Barbanera and others, and participating to a european project on behavioural types led by Simon Gay.
In the same year I got interest in Berardi's interpretation of classical reasoning based on learning. This is a new view of Coquand's game semantics of classical arithmetic that we have developed into a new concept of realizability, called interactive realizability, aiming at a constructive interpretation of classical proofs that avoids detours through translations of various kinds, while being compositional and (more importantly) reflecting the proof structure.
Starting with 2009 I have been working with Barbanera on contract compliance for web services. We have especially focused on contracts that correspond to session types as introduced by Honda et alii. We have investigated so far various notions of subcontract and compliance, that remain decidable even by relaxing the standard constraints based on the concept of duality.
In 2011 I found an answer to van Bakel's question of the existence of a filter model of the λμ-calculus, which was ideated by Parigot in the 90's to compute with classical proofs. This is based on reconstructing Streicher and Reus's continuation models by means of intersection types, which is possible when working in the category of ω-algebraic lattices. This led me, with van Bakel and Barbanera, to the development of a new typing system for λμ and to a characterisation of strongly normalizing λμ-terms, much as Pottinger did for ordinary λ-calculus in the 80's. Then I moved my investigation to de Groote and Saurin's extension of Parigot's λμ, in the hope to gain a cleaner look of continuations and of control operators in general.
In 2013 I have started a collaboration with Jakob Rehof and his groop in Dortmund, aimed at applying the synthesis by inhabitation method, originated with Rehof and Urzyczyn's work, to classes and mixins. This has renewed the interest in polymorphic typing of extensible records that we are investigating in a new perspective w.r.t. the classical studies in the 90s.
In 2014 I got the italian "Abilitazione Nazionale 01/A1 - I Fascia" to full professorhip in Logic and Complementary Mathematics.
Last updated July 2017