Post date: 16-Apr-2012 10:41:21
Upcoming PhD course
Proofs and Types
May-June 2012
Dipartimento di Matematica e Informatica - Via Ospedale 72, Cagliari
Paolo Di Giamberardino
Dipartimento di Matematica e Informatica
Università degli Studi di Cagliari
Abstract. Computer science owes its birth largely to logic and to the research on the foundations of mathematics. In early nineties, the notion of "computational model" was defined in the framework of logic in order to give an answer to Hilbert's second problem: is there a general algorithm or mechanical procedure to establish, for each formula of arithmetic, whether it is a theorem or not, i.e. if the formula is deducible from the axioms?
Subsequentely, the theoretical notion of computational model was the basis on which modern computers were developed.
The "family resemblance" between logic and computer science was precisely formulated in the '60, with the discovery by Haskell Curry and William Howard of the isomorphism between proofs and programs, a cornerstone result connecting proof theory and programming languages.
The purpose of this short course is to present in an accessible way the Curry Howard isomorphism, highlighting its significance and importance.
Contents.
References.
Slides.