Universitą di Torino


Full Professor in Computer Science.
Affiliation: C. S. Department, Univ. of Torino .
Address: Via Pessinetto 12, Dipartimento di Informatica, 10149 - Torino - Italy.
Office: n. 32, stair L, floor number 3 (office code 032_D_P03_0100). Take the elevator adiacent to the front gate of via Pessinetto 12 and press the button for "floor 1" (Computer Science Dept.). Get off and ask the reception how to reach the stair L. The floor with number "1" is actually a second floor, because between it and the level of the front gate there is a parking floor, called floor "P" or floor "0".
Tel. (+39) 011 670 6750 Fax: (+39) 011 751603 E-mail for erasmus students: commerasmccs, then the e-mail symbol, followed by educ.di.unito.it. Please do not use my personal e-mail for erasmus messages. Personal e-mail: stefano, then the e-mail symbol, followed by di.unito.it.

Frequently used links. C.S. Dept.: ESCO Missioni , ESCO Richieste di Acquisto (RDA) (con richieste in: workflow/tutte le richieste/filtra), Ricerca locale 2016 ( english), interviste tutorato, imp, ftp, educ, iris , u-gov (progetti) , C.S. Intranet , prenotazioni aule, Help Desk , Organi e Commissioni. Math. Dept: campusnet . Physics Dept.: campusnet . Pearson text: Java . Moodle sites (se non riuscite ad accedere al sito scrivetemi): Calcolabilitą e complessitą 2021/2022 (sia A che B), in presenza e streaming, con stanza webex. TARM: tests. ESSE3: registri. Erasmus: mobilita' attive , Servizi online per studenti outgoing.

TALK AT EUTYPES NIJMEGEN, 2018: The simply typed lambda calculus N (January 23, 2018). A research report on system N.

TALK AT FOSSACS 2017: Martin-Lof's Inductive Definitions Are Not Equivalent to Cyclic Proofs (Wednesday, April 26, 2017). A preprint of the paper.


  • Dispense (docx,pdf) di un corso di Programmazione I (Basi di Programmazione) in C++: 24 lezioni, 48 ore, 250 pagine, con 12 tutorati, del 2017. Con esercizi risolti.
  • Dispense (docx) di un corso breve di Programmazione II (Programmazione Avanzata) in C++: 12 lezioni, 24 ore, 100 pagine, senza tutorato, del 2015. Con esercizi risolti di maggiore dimensione.
  • Entrambi i corsi utilizzano il testo online di Allen Downey "How To Think Like A Computer Scientist" del 2012 (pdf), rispettivamente le sezioni 1-10 e 11-15.

    RESEARCH (see also the common publication page):

  • My last talk at the Workshop on Efficient and Natural Proof Systems in Bath: Game Semantics and the Complexity of Interaction (about a result of Federico Aschieri).
  • Site leader for the Torino unit of the COFIN Project: "Metodi Logici per il trattamento dell'informazione" .
  • Steering committee with S. van Bakel and co-chair for the CL&C Congresses Series. including the current congress CL&C18 (Oxford, UK), CL&C16 (Porto, Portugal, satellite of FSCD 2016). The CL&C Congresses Series: CL&C06 (Venice, ICALP 2006), CL&C08 (Reykjavik, ICALP 2008), CL&C10 (Brno, PECP, MFCS & CSL 2010), CL&C12 (Warwick, CSL 2012), CL&C14 (Wien, CSL & LICS 2014). More on van Bakel's home page.
  • PC member of Control Operator Semantics 2013
  • 1995-2008 Organizer of the congresses Types 1995, Types 2003, Types 2008.
  • 2007 Summer School Bertinoro, Italy. Draft of the course: Realizability: Extracting Programs from proofs.
  • 2011 Summer School Realizability in Chambery . Draft of the course: Interactive Realizability. (.pdf version-4 slides/page).
  • Erasmus Committee for C.S. Dept. of Turin Univ.. The conversion table matching european and italian grades (valid since Dec., 13 2010) is the following: E: 18 19 20 D: 21 22 23 24 C: 25 26 27 B: 28 29 A: 30 30/lode. This was the table valid before Dec., 13 2010. This is the site with current list of Erasmus agreements.
  • Game Semantics of Classical Proofs . A site introducing a semantics of proofs of classical logic through Tarski Games with retractable moves. The source code of a Mathematica program assisting two players playing Tarski games with retractable moves ( nb , zip).
    Paper: An Intuitionistic Model Of Delta-0-2 ... . Last conference in Tokyo (version of February 2006): Semantics of Backtracking . Last Types conference (version of December 2004): A game model for 1-backtracking . Previous conference Types conference in Torino (version of June 2004): Programming with Non-Recursive Maps .


  • 2007 Types Summer School (Bertinoro, Italy, August 2007). Draft of the course: Realizability: Extracting Programs from proofs.
  • 2006 Summer School (Collegno, Italy, August 2006). A short introduction to Isabelle. All files of the course , including: slides in .ppt, the solution of Hotel Key Cards exercise, a 16 hour course on Isabelle, more exercices and more solutions (2Mb). Alternatively, only slides in pdf format (8Mb).
  • 2005 Summer School (Gargnano, Italy). A short introduction to lambda calculus. Format: zipped ppt . Solutions of all exercises.
  • 2002 Summer School (Eugene, Oregon): one file with two short courses about Logic and Realizability Formats: ppt , zip . A reference of the course is Boerio Ph.d. thesis: "Optimizing Programs Extracted From Proofs". Formats: ps , zip .


    Old Moodle sites back to the academic year 2007/2008: Laboratorio IIB turno 2 2020/2021, Programmazione IIB 2020/2021, Calcolabilitą e Complessitą 2020/2021 (sia A che B). Laboratorio di Programmazione IIB Turno T2 2019/2020, Programmazione IIB 2019/2020, Calcolabilitą e complessitą 2019/2020 (sia A che B, si tratta delle stesso corso sotto nomi diversi per triennale e magistrale), Programmazione IIB 2018/2019 (con links a: ProgIB, ProgIIA, LabIIA, LabIIB1, LabIIB2, GIT ), Calcolabilitą e complessitą 2018/2019 (sia A che B, si tratta delle stesso corso sotto nomi diversi per triennale e magistrale). Programmazione Avanzata 2017/2018 , Programmazione IIB 2017/2018 (link al corso IIA e al lab. IIB1), Calcolabilitą e complessitą 2017/2018 (con scheda dell'insegnamento), Programmazione IIB 2016/2017 . Logica per Informatica 2016/2017 ( con scheda dell'insegnamento ). Basi di Informatica 2016/2017. Metodi Formali 2016/2017. Programmazione avanzata 2014/2015, Basi di Informatica 2014/2015, Tutorato di Informatica 2014/2015, TIF 2014/2015 , Basi di Informatica A 2013/2014, TIF 2013/2014 , Info A 2012/2013, TIF 12/13 , Info A 2011/2012, TIF A 11/12, TIF A 10/11, Info I 10/11, SPERIM 09/10, Info A 09/10, Info A 08/09, Info A 07/08, Lab. Calc. I 09/10, Lab. Calc. I 08/09, Ded. Aut. 07/08 .

    Teaching (old web sites or terminated courses from 1998/1999 to 2007/2008):

  • Informatica A (Corso del '07/'08, sito ora rimpiazzato dal sito Moodle).
  • Laboratorio di Calcolo I ( Corso sul programma Mathematica , dal '98/'99 al 07'/08', Torino, Dip. Fisica, sito ora rimpiazzato dal sito Moodle). Un sito col le Dispense ; un sito con applicazioni di Mathematica ad altri Corsi della Laurea in Fisica; infine, un sito con brevi Articoli di argomento curioso o divertente.
  • Informatica I ( Corso di Linguaggio C , dal '01/'02 al 06'/07', terminato , Dip. di Matematica),
  • Programmazione 1 ( Corso di Linguaggio Pascal , dal '97/'98 al '00/'01, terminato , Torino, Dip. di Informatica),
  • Sistemi per l'Elaborazione dell'Informazione I e II (98/99, terminato , Lecce, Dip. Matematica).

    Fractals. . Take a look to my site about fractals and to a conference on this topic from a friend (both Italian only, for the moment). Here is a program zooming very tiny details from a few fractals (Eloisa and others), but you need the file alleg.40.dll in the same directory to run it. Some more fractal images: trees , trees 3D .

  • Last update: Sept. 11, 2008