Curriculum Vitae

Silvio Valentini was born in Padova (Italy) January 6, 1953. He attended his studies in Mathematics at the Mathematical department of the University of Padova where he obtained his master's degree summa cum laude by discussing a thesis titled "L'uso del calcolo dei predicati per la scrittura di algoritmi", under the supervision of professor Giovanni Sambin and professor Enrico Pagello.

On October 1, 1977 he won a C.N.R. grant for Algebra and Geometry at the department of Mathematics of the university of Siena (Italy) under the supervision of professor Roberto Magari.

On November 1, 1980 he became a Ricercatore Universitario Confermato at the department of Mathematics of the University of Siena.

On April 2, 1984 he moved to the Institute of Algebra e Geometry of the university of Padova.

Then he won a competition for a position of associate professor in Algebra and on September 25, 1987 he became associate professor of Mathematical Logic at the department of Computer Science of the university of Milano.

On November 1, 1991 he moved to the department of Pure and Applied Mathematics of the university of Padova where he worked until today.

On June 22, 1999 he obtained a PhD in Mathematics and Informatics at the Katholieke Universiteit of Nijmegen by defending a thesis titled "Methamatematical aspects of Martin-Loef's type theory", under the supervision of professor Henk Barendreght.


The earlier scientific works of Silvio Valentini dealt with modal logic, and in particular with the modal logic of provability, which was the main topic in the Siena group, for which he developed a proof theoretical approach. Moreover he analized the use of logical calculi in theoretical computer science.

Then he began to study typed lambda calculi, with a particular attention to Martin-Loef's Intuitionistic Type Theory, but also simple typed lambda calculus and to the definition of typed calculi based on non sub-structural logic.

At present his main interests are the development of actual pieces of mathematics within Intuitionistic Type Theory and the construction of categorical semantics for typed lambda calculi, but he is also working in collaboration with researchers of C.N.R. to apply Intuitionistic Type Theory in order to construct pieces of hardware which can be proved to be correct and he is interested in using a type theoretical approach in studing program correctness and security.

[Back]