Stefano Berardi

Steffen van Bakel, Stefano Berardi, Ulrich Berger: Preface. Ann. Pure Appl. Logic 164(6): 589-590 (2013)

Stefano Berardi, Makoto Tatsuta: Internal models of system F for decompilation. Theor. Comput. Sci. 435: 3-20 (2012)

Stefano Berardi, Ugo de'Liguoro: Interactive Realizers: A New Approach to Program Extraction from Nonconstructive Proofs. ACM Trans. Comput. Log. 13(2): 11 (2012)

Stefano Berardi, Ugo de'Liguoro: Knowledge Spaces and the Completeness of Learning Strategies. CSL 2012: 77-91

Makoto Tatsuta, Stefano Berardi: Non-Commutative Infinitary Peano Arithmetic. CSL 2011: 538-552

Stefano Berardi, Thierry Coquand, Susumu Hayashi: Games with 1-backtracking. Ann. Pure Appl. Logic 161(10): 1254-1269 (2010)

Steffen van Bakel, Stefano Berardi, Ulrich Berger: Preface. Ann. Pure Appl. Logic 161(11): 1313-1314 (2010)

Federico Aschieri, Stefano Berardi: Interactive Learning-Based Realizability for Heyting Arithmetic with EM1. Logical Methods in Computer Science 6(3) (2010)

Stefano Berardi, Makoto Tatsuta: Internal Normalization, Compilation and Decompilation for System F_bh. FLOPS 2010: 207-223

Steffen van Bakel, Stefano Berardi, Ulrich Berger (Eds.): Proceedings Third International Workshop on Classical Logic and Computation. EPTCS 47, 2010

Stefano Berardi, Ugo de'Liguoro: Interactive Realizers and Monads. CoRR abs/1005.2907 (2010)

Stefano Berardi, Ugo de'Liguoro: Toward the interpretation of non-constructive reasoning as non-monotonic learning. Inf. Comput. 207(1): 63-81 (2009)

Federico Aschieri, Stefano Berardi: Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1. TLCA 2009: 20-34

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

Steffen van Bakel, Stefano Berardi: Preface. Ann. Pure Appl. Logic 153(1-3): 1-2 (2008)

Stefano Berardi, Yoriyuki Yamagata: A sequent calculus for limit computable mathematics. Ann. Pure Appl. Logic 153(1-3): 111-126 (2008)

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)

Stefano Berardi, Ugo de'Liguoro: A Calculus of Realizers for EM1 Arithmetic (Extended Abstract). CSL 2008: 215-229

Stefano Berardi, Makoto Tatsuta: Positive Arithmetic Without Exchange Is a Subclassical Logic. APLAS 2007: 271-285

Stefano Berardi: Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves. TLCA 2007: 23-38

Stefano Berardi: Some intuitionistic equivalents of classical principles for degree 2 formulas. Ann. Pure Appl. Logic 139(1-3): 185-200 (2006)

Stefano Berardi: Classical logic as limit completion. Mathematical Structures in Computer Science 15(1): 167-200 (2005)

Stefano Berardi, Thierry Coquand, Susumu Hayashi: Games with 1-backtracking. GALOP 2005: 210-225

Stefano Berardi, Silvio Valentini: Krivine's intuitionistic proof of classical completeness (for countable languages). Ann. Pure Appl. Logic 129(1-3): 93-106 (2004)

Stefano Berardi: A generalization of a conservativity theorem for classical versus intuitionistic arithmetic. Math. Log. Q. 50(1): 41-46 (2004)

Stefano Berardi, Chantal Berline: Building continuous webbed models for system F. Theor. Comput. Sci. 315(1): 3-34 (2004)

Yohji Akama, Stefano Berardi, Susumu Hayashi, Ulrich Kohlenbach: An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. LICS 2004: 192-201

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

Franco Barbanera, Stefano Berardi: A full continuous model of polymorphism. Theor. Comput. Sci. 290(1): 407-428 (2003)

Stefano Berardi, Chantal Berline: BetaEta-Complete Models for System F. Mathematical Structures in Computer Science 12(6): 823-874 (2002)

Stefano Berardi, Chantal Berline: Building continuous webbed models for system F. Electr. Notes Theor. Comput. Sci. 35: 3-33 (2000)

Stefano Berardi, Mario Coppo, Ferruccio Damiani, Paola Giannini: Type-Based Useless-Code Elimination for Functional Programs. SAIG 2000: 172-189

Stefano Berardi: Intuitionistic Completeness for First Order Classical Logic. J. Symb. Log. 64(1): 304-312 (1999)

Stefano Berardi, Ugo de'Liguoro: Total Functionals and Well-Founded Strategies. TLCA 1999: 54-68

Stefano Berardi, Marc Bezem, Thierry Coquand: On the Computational Content of the Axiom of Choice. J. Symb. Log. 63(2): 600-622 (1998)

Stefano Baratella, Stefano Berardi: Approximating Classical Theorems. J. Log. Comput. 8(6): 839-854 (1998)

Stefano Baratella, Stefano Berardi: A parallel game semantics for Linear Logic. Arch. Math. Log. 36(3): 189-217 (1997)

Franco Barbanera, Stefano Berardi: The Simply-Typed Theory of Beta-Conversion has no Maximum Extension. Inf. Comput. 139(1): 57-61 (1997)

Franco Barbanera, Stefano Berardi, Massimo Schivalocchi: "Classical" Programming-with-Proofs in lambda_PA^Sym: An Analysis of Non-confluence. TACS 1997: 365-390

Stefano Berardi, Luca Boerio: Minimum Information Code in a Pure Functional Language with Data Types. TLCA 1997: 30-45

Franco Barbanera, Stefano Berardi: A Symmetric Lambda Calculus for Classical Program Extraction. Inf. Comput. 125(2): 103-117 (1996)

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)

Stefano Berardi: Pruning Simply Typed Lambda-Terms. J. Log. Comput. 6(5): 663-681 (1996)

Franco Barbanera, Stefano Berardi: A Constructive Valuation Semantics for Classical Logic. Notre Dame Journal of Formal Logic 37(3): 462-482 (1996)

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

Franco Barbanera, Stefano Berardi: A Strong Normalization Result for Classical Logic. Ann. Pure Appl. Logic 76(2): 99-116 (1995)

Stefano Berardi, Marc Bezem, Thierry Coquand: A realization of the negative interpretation of the Axiom of Choice. TLCA 1995: 47-62

Stefano Berardi, Luca Boerio: Using Subtyping in Program Optimization. TLCA 1995: 63-77

Franco Barbanera, Stefano Berardi: A Symmetric Lambda Calculus for "Classical" Program Extraction. TACS 1994: 495-515

Stefano Berardi: An Application of PER Models to Program Extraction. Mathematical Structures in Computer Science 3(3): 309-331 (1993)

Franco Barbanera, Stefano Berardi: Extracting Constructive Content from Classical Logic via Control-like Reductions. TLCA 1993: 45-59

Franco Barbanera, Stefano Berardi: A Constructive Valuation Interpretation for Classical Logic and its Use in Witness Extraction. CAAP 1992: 1-23

Stefano Berardi: Retractions on dI-domains as a model for Type:Type. Inf. Comput. 94(2): 204-231 (1991)

Stefano Berardi: Equalization of Finite Flowers. J. Symb. Log. 53(1): 105-123 (1988)