{"id":124,"date":"2012-04-16T11:41:21","date_gmt":"2012-04-16T10:41:21","guid":{"rendered":"http:\/\/sites.google.com\/feeds\/content\/site\/tcsunica\/7686587897779804437"},"modified":"2013-11-22T15:40:06","modified_gmt":"2013-11-22T14:40:06","slug":"phd-short-course-proofs-and-types","status":"publish","type":"post","link":"https:\/\/dottorati.unica.it\/matematicaeinformatica\/2012\/04\/16\/phd-short-course-proofs-and-types\/","title":{"rendered":"PhD short course: Proofs and types"},"content":{"rendered":"
Upcoming PhD course
<\/font><\/div>
<\/font>
Proofs and Types<\/b>

<\/font>
May-June 2012
<\/font>\n<\/div>\nDipartimento di Matematica e Informatica - Via Ospedale 72, Cagliari

Paolo Di Giamberardino<\/b>

<\/font>Dipartimento di Matematica e Informatica<\/font>
<\/font>Universit\u00e0 degli Studi di Cagliari<\/font>
<\/font>
<\/font><\/div>\n
\nAbstract<\/span><\/b>. Computer science owes its birth largely to logic and to the research on \nthe foundations of mathematics. In early nineties, the notion of \n"computational model" was defined in the framework of logic in order to \ngive an answer to Hilbert's second problem: is there a general algorithm\n or mechanical procedure to establish, for each formula of arithmetic, whether it is a theorem <\/span><\/font>or not<\/span><\/font>, i.e. if the formula is deducible from the axioms?<\/span>

\nSubsequentely, the theoretical notion of computational model was the basis on which modern computers were developed.<\/span><\/font>\n

\nThe "family resemblance" between logic and computer science was\n precisely formulated in the '60, with the discovery by Haskell Curry and\n William Howard of the isomorphism between proofs and programs, a cornerstone result connecting proof theory and programming languages\u200b\u200b.<\/span><\/font>\n

\nThe purpose of this short course is to present in an accessible way the \nCurry Howard isomorphism, highlighting its significance and importance.<\/span><\/font>

<\/font>\nContents.<\/b>
<\/font>
  1. The simply-typed lambda-calculus (May <\/font>9, Aula F, <\/font>15:00-17.00<\/font>)
    <\/font><\/li>
  2. Intuitionistic logic and natural deduction. The Curry-Howard isomorphism <\/font>(May 11<\/font>, Aula F, <\/font>15:00-17.00<\/font>)<\/font><\/li>
  3. System F and polymorphism (<\/font>June 22, Aula C, 12.00<\/font>)
    <\/font><\/li><\/ol>\nReferences.<\/span><\/b>
    <\/font>\n