PhD in Computer Science

Courses

• Calcolabilità e Complessità  (INF0090)
  Corso di laurea in Informatica
• Fondamenti dell'Informatica (INF0348)
  Corso di laurea in Informatica

Research topics

Logic, Proof Theory, Type Theory, Foundation of Computer Science

Research groups

• Logical Foundations of Computation (Logic)

• Fondazioni logiche della computazione

Activities in agenda

See my calendar

Academic bodies

• Commissione Ricerca
• Consiglio di Dipartimento
• Giunta di Dipartimento

• Commissione Erasmus e Internazionalizzazione
• Consiglio di corso di Laurea e Laurea Magistrale in Informatica

Office hours

(cercate i siti moodle dei miei corsi su http://www.di.unito.it/~stefano)
ricevimento su appuntamento (mandare un messaggio elettronico)
informazioni su:
http://www.di.unito.it/~stefano

ELENCO PUBBLICAZIONI AGGIORNATO AL 2012

2012
j30		Stefano Berardi, Makoto Tatsuta: Internal models of system F for decompilation. Theor. Comput. Sci. 435: 3-20 (2012)
j29		Stefano Berardi, Ugo de'Liguoro: Interactive Realizers: A New Approach to Program Extraction from Nonconstructive Proofs. ACM Trans. Comput. Log. 13(2): 11 (2012)
c18		Stefano Berardi, Ugo de'Liguoro: Knowledge Spaces and the Completeness of Learning Strategies. CSL 2012: 77-91
	2011
c17		Makoto Tatsuta, Stefano Berardi: Non-Commutative Infinitary Peano Arithmetic. CSL 2011: 538-552
	2010
j28		Stefano Berardi, Thierry Coquand, Susumu Hayashi: Games with 1-backtracking. Ann. Pure Appl. Logic 161(10): 1254-1269 (2010)
j27		Steffen van Bakel, Stefano Berardi, Ulrich Berger: Preface. Ann. Pure Appl. Logic 161(11): 1313-1314 (2010)
j26		Federico Aschieri, Stefano Berardi: Interactive Learning-Based Realizability for Heyting Arithmetic with EM1. Logical Methods in Computer Science 6(3) (2010)
c16		Stefano Berardi, Makoto Tatsuta: Internal Normalization, Compilation and Decompilation for System Fbh. FLOPS 2010: 207-223
e4		Steffen van Bakel, Stefano Berardi, Ulrich Berger (Eds.): Proceedings Third International Workshop on Classical Logic and Computation. EPTCS 47, 2010
i1		Stefano Berardi, Ugo de'Liguoro: Interactive Realizers and Monads. CoRR abs/1005.2907 (2010)
	2009
j25		Stefano Berardi, Ugo de'Liguoro: Toward the interpretation of non-constructive reasoning as non-monotonic learning. Inf. Comput. 207(1): 63-81 (2009)
c15		Federico Aschieri, Stefano Berardi: Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1. TLCA 2009: 20-34
e3		Stefano Berardi, Ferruccio Damiani, Ugo de'Liguoro (Eds.): Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers. Lecture Notes in Computer Science 5497, Springer 2009, isbn 978-3-642-02443-6
	2008
j24		Steffen van Bakel, Stefano Berardi: Preface. Ann. Pure Appl. Logic 153(1-3): 1-2 (2008)
j23		Stefano Berardi, Yoriyuki Yamagata: A sequent calculus for limit computable mathematics. Ann. Pure Appl. Logic 153(1-3): 111-126 (2008)
j22		Stefano Berardi, Ugo de'Liguoro: Calculi, types and applications: Essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi Della Rocca. Theor. Comput. Sci. 398(1-3): 1-11 (2008)
c14		Stefano Berardi, Ugo de'Liguoro: A Calculus of Realizers for EM1 Arithmetic (Extended Abstract). CSL 2008: 215-229
	2007
c13		Stefano Berardi, Makoto Tatsuta: Positive Arithmetic Without Exchange Is a Subclassical Logic. APLAS 2007: 271-285
c12		Stefano Berardi: Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves. TLCA 2007: 23-38
	2006
j21		Stefano Berardi: Some intuitionistic equivalents of classical principles for degree 2 formulas. Ann. Pure Appl. Logic 139(1-3): 185-200 (2006)
	2005
j20		Stefano Berardi: Classical logic as limit completion. Mathematical Structures in Computer Science 15(1): 167-200 (2005)
c11		Stefano Berardi, Thierry Coquand, Susumu Hayashi: Games with 1-backtracking. GALOP 2005: 210-225
	2004
j19		Stefano Berardi, Silvio Valentini: Krivine's intuitionistic proof of classical completeness (for countable languages). Ann. Pure Appl. Logic 129(1-3): 93-106 (2004)
j18		Stefano Berardi: A generalization of a conservativity theorem for classical versus intuitionistic arithmetic. Math. Log. Q. 50(1): 41-46 (2004)
j17		Stefano Berardi, Chantal Berline: Building continuous webbed models for system F. Theor. Comput. Sci. 315(1): 3-34 (2004)
c10		Yohji Akama, Stefano Berardi, Susumu Hayashi, Ulrich Kohlenbach: An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. LICS 2004: 192-201
e2		Stefano Berardi, Mario Coppo, Ferruccio Damiani (Eds.): Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers. Lecture Notes in Computer Science 3085, Springer 2004, isbn 3-540-22164-6
	2003
j16		Franco Barbanera, Stefano Berardi: A full continuous model of polymorphism. Theor. Comput. Sci. 290(1): 407-428 (2003)
	2002
j15		Stefano Berardi, Chantal Berline: BetaEta-Complete Models for System F. Mathematical Structures in Computer Science 12(6): 823-874 (2002)
	2000
j14		Stefano Berardi, Chantal Berline: Building continuous webbed models for system F. Electr. Notes Theor. Comput. Sci. 35: 3-33 (2000)
c9		Stefano Berardi, Mario Coppo, Ferruccio Damiani, Paola Giannini: Type-Based Useless-Code Elimination for Functional Programs. SAIG 2000: 172-189
	1999
j13		Stefano Berardi: Intuitionistic Completeness for First Order Classical Logic. J. Symb. Log. 64(1): 304-312 (1999)
c8		Stefano Berardi, Ugo de'Liguoro: Total Functionals and Well-Founded Strategies. TLCA 1999: 54-68
	1998
j12		Stefano Berardi, Marc Bezem, Thierry Coquand: On the Computational Content of the Axiom of Choice. J. Symb. Log. 63(2): 600-622 (1998)
j11		Stefano Baratella, Stefano Berardi: Approximating Classical Theorems. J. Log. Comput. 8(6): 839-854 (1998)
	1997
j10		Stefano Baratella, Stefano Berardi: A parallel game semantics for Linear Logic. Arch. Math. Log. 36(3): 189-217 (1997)
j9		Franco Barbanera, Stefano Berardi: The Simply-Typed Theory of Beta-Conversion has no Maximum Extension. Inf. Comput. 139(1): 57-61 (1997)
c7		Franco Barbanera, Stefano Berardi, Massimo Schivalocchi: "Classical" Programming-with-Proofs in lambdaPASym: An Analysis of Non-confluence. TACS 1997: 365-390
c6		Stefano Berardi, Luca Boerio: Minimum Information Code in a Pure Functional Language with Data Types. TLCA 1997: 30-45
	1996
j8		Franco Barbanera, Stefano Berardi: A Symmetric Lambda Calculus for Classical Program Extraction. Inf. Comput. 125(2): 103-117 (1996)
j7		Franco Barbanera, Stefano Berardi: Proof-Irrelevance out of Exluded-Middle and Choice in the Calculus of Constructions. J. Funct. Program. 6(3): 519-525 (1996)
j6		Stefano Berardi: Pruning Simply Typed Lambda-Terms. J. Log. Comput. 6(5): 663-681 (1996)
j5		Franco Barbanera, Stefano Berardi: A Constructive Valuation Semantics for Classical Logic. Notre Dame Journal of Formal Logic 37(3): 462-482 (1996)
e1		Stefano Berardi, Mario Coppo (Eds.): Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers. Lecture Notes in Computer Science 1158, Springer 1996, isbn 3-540-61780-9
	1995
j4		Franco Barbanera, Stefano Berardi: A Strong Normalization Result for Classical Logic. Ann. Pure Appl. Logic 76(2): 99-116 (1995)
c5		Stefano Berardi, Marc Bezem, Thierry Coquand: A realization of the negative interpretation of the Axiom of Choice. TLCA 1995: 47-62
c4		Stefano Berardi, Luca Boerio: Using Subtyping in Program Optimization. TLCA 1995: 63-77
	1994
c3		Franco Barbanera, Stefano Berardi: A Symmetric Lambda Calculus for "Classical" Program Extraction. TACS 1994: 495-515
	1993
j3		Stefano Berardi: An Application of PER Models to Program Extraction. Mathematical Structures in Computer Science 3(3): 309-331 (1993)
c2		Franco Barbanera, Stefano Berardi: Extracting Constructive Content from Classical Logic via Control-like Reductions. TLCA 1993: 45-59
	1992
c1		Franco Barbanera, Stefano Berardi: A Constructive Valuation Interpretation for Classical Logic and its Use in Witness Extraction. CAAP 1992: 1-23
	1991
j2		Stefano Berardi: Retractions on dI-domains as a model for Type:Type. Inf. Comput. 94(2): 204-231 (1991)
	1988
j1		Stefano Berardi: Equalization of Finite Flowers. J. Symb. Log. 53(1): 105-123 (1988)