Equalization of Finite Flowers. - Stefano Berardi (J. Symb. Log., 1988)

Retractions on dI-domains as a model for Type:Type - Stefano Berardi (Inf. Comput., 1991)

A Constructive Valuation Interpretation for Classical Logic and its Use in Witness Extraction. - Franco Barbanera; Stefano Berardi (CAAP, 1992)

Extracting Constructive Content from Classical Logic via Control-like Reductions. - Franco Barbanera; Stefano Berardi (TLCA, 1993)

An Application of PER Models to Program Extraction. - Stefano Berardi (Math. Struct. Comput. Sci., 1993)

Using Subtyping in Program Optimization. - Stefano Berardi; Luca Boerio (TLCA, 1995)

A realization of the negative interpretation of the Axiom of Choice. - Stefano Berardi; Marc Bezem; Thierry Coquand (TLCA, 1995)

A Strong Normalization Result for Classical Logic. - Franco Barbanera; Stefano Berardi (Ann. Pure Appl. Log., 1995)

A Symmetric Lambda Calculus for Classical Program Extraction. - Franco Barbanera; Stefano Berardi (Inf. Comput., 1996)

Proof-Irrelevance out of Exluded-Middle and Choice in the Calculus of Constructions. - Franco Barbanera; Stefano Berardi (J. Funct. Program., 1996)

Pruning Simply Typed Lambda-Terms. - Stefano Berardi (J. Log. Comput., 1996)

A Constructive Valuation Semantics for Classical Logic. - Franco Barbanera; Stefano Berardi (Notre Dame J. Formal Log., 1996)

"Classical" Programming-with-Proofs in lambdaPASym: An Analysis of Non-confluence. - Franco Barbanera; Stefano Berardi; Massimo Schivalocchi (TACS, 1997)

Minimum Information Code in a Pure Functional Language with Data Types. - Stefano Berardi; Luca Boerio (TLCA, 1997)

A parallel game semantics for Linear Logic. - Stefano Baratella; Stefano Berardi (Arch. Math. Log., 1997)

The Simply-Typed Theory of Beta-Conversion has no Maximum Extension. - Franco Barbanera; Stefano Berardi (Inf. Comput., 1997)

On the Computational Content of the Axiom of Choice. - Stefano Berardi; Marc Bezem; Thierry Coquand (J. Symb. Log., 1998)

Approximating Classical Theorems. - Stefano Baratella; Stefano Berardi (J. Log. Comput., 1998)

Total Functionals and Well-Founded Strategies. - Stefano Berardi; Ugo de'Liguoro (TLCA, 1999)

Intuitionistic Completeness for First Order Classical Logic. - Stefano Berardi (J. Symb. Log., 1999)

Type-Based Useless-Code Elimination for Functional Programs. - Stefano Berardi; Mario Coppo; Ferruccio Damiani; Paola Giannini (SAIG, 2000)

BetaEta-Complete Models for System F. - Stefano Berardi; Chantal Berline (Math. Struct. Comput. Sci., 2002)

A full continuous model of polymorphism. - Franco Barbanera; Stefano Berardi (Theor. Comput. Sci., 2003)

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

Krivine's intuitionistic proof of classical completeness (for countable languages). - Stefano Berardi; Silvio Valentini (Ann. Pure Appl. Log., 2004)

A generalization of a conservativity theorem for classical versus intuitionistic arithmetic. - Stefano Berardi (Math. Log. Q., 2004)

Building continuous webbed models for system F. - Stefano Berardi; Chantal Berline (Theor. Comput. Sci., 2004)

Classical logic as limit completion. - Stefano Berardi (Math. Struct. Comput. Sci., 2005)

Some intuitionistic equivalents of classical principles for degree 2 formulas. - Stefano Berardi (Ann. Pure Appl. Log., 2006)

Positive Arithmetic Without Exchange Is a Subclassical Logic. - Stefano Berardi; Makoto Tatsuta (APLAS, 2007)

Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves. - Stefano Berardi (TLCA, 2007)

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

Preface. - Steffen van Bakel; Stefano Berardi (Ann. Pure Appl. Log., 2008)

A sequent calculus for limit computable mathematics. - Stefano Berardi; Yoriyuki Yamagata (Ann. Pure Appl. Log., 2008)

Calculi, types and applications: Essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi Della Rocca. - Stefano Berardi; Ugo de'Liguoro (Theor. Comput. Sci., 2008)

Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1. - Federico Aschieri; Stefano Berardi (TLCA, 2009)

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

Internal Normalization, Compilation and Decompilation for System Fbh. - Stefano Berardi; Makoto Tatsuta (FLOPS, 2010)

Games with 1-backtracking. - Stefano Berardi; Thierry Coquand; Susumu Hayashi (Ann. Pure Appl. Log., 2010)

Interactive Realizers and Monads - Stefano Berardi; Ugo de'Liguoro (CoRR, 2010)

Interactive Learning-Based Realizability for Heyting Arithmetic with EM1 - Federico Aschieri; Stefano Berardi (Log. Methods Comput. Sci., 2010)

Non-Commutative Infinitary Peano Arithmetic. - Makoto Tatsuta; Stefano Berardi (CSL, 2011)

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

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

Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1. - Federico Aschieri; Stefano Berardi; Giovanni Birolo (CSL, 2013)

Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics. - Stefano Berardi; Makoto Tatsuta (TLCA, 2013)

Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic. - Stefano Berardi; Silvia Steila (TYPES, 2013)

Preface. - Steffen van Bakel; Stefano Berardi; Ulrich Berger 001 (Ann. Pure Appl. Log., 2013)

Non-monotonic Pre-fixed Points and Learning. - Stefano Berardi; Ugo de'Liguoro (FICS, 2013)

Proving termination of programs having transition invariants of height ω. - Stefano Berardi; Paulo Oliva; Silvia Steila (ICTCS, 2014)

Ramsey Theorem as an Intuitionistic Property of Well Founded Relations. - Stefano Berardi; Silvia Steila (RTA-TLCA, 2014)

An intuitionistic version of Ramsey Theorem (italian version). - Stefano Berardi (CoRR, 2014)

Proving termination with transition invariants of height omega. - Stefano Berardi; Paulo Oliva; Silvia Steila (CoRR, 2014)

Knowledge Spaces and the Completeness of Learning Strategies. - Stefano Berardi; Ugo de'Liguoro (Log. Methods Comput. Sci., 2014)

Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness. - Stefano Berardi (CSL, 2015)

An intuitionistic version of Ramsey's Theorem and its use in Program Termination. - Stefano Berardi; Silvia Steila (Ann. Pure Appl. Log., 2015)

A Sound, Complete and Effective Second Order Game Semantics. - Stefano Berardi (CoRR, 2016)

Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System. - Stefano Berardi; Makoto Tatsuta (FoSSaCS, 2017)

Equivalence of inductive definitions and cyclic proofs under arithmetic. - Stefano Berardi; Makoto Tatsuta (LICS, 2017)

Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic. - Stefano Berardi; Makoto Tatsuta (CoRR, 2017)

Non-monotonic Pre-fix Points and Learning. - Stefano Berardi; Ugo de'Liguoro (Fundam. Informaticae, 2017)

Ramsey's Theorem for Pairs and k Colors as a sub-Classical Principle of Arithmetic. - Stefano Berardi; Silvia Steila (J. Symb. Log., 2017)

Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs. - Stefano Berardi; Makoto Tatsuta (CMCS, 2018)

Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. - Stefano Berardi; Makoto Tatsuta (Log. Methods Comput. Sci., 2019)

An analysis of the Podelski-Rybalchenko termination theorem via bar recursion. - Stefano Berardi; Paulo Oliva; Silvia Steila (J. Log. Comput., 2019)

A General Constructive Form of Higman's Lemma. - Stefano Berardi; Gabriele Buriola; Peter Schuster 001 (CSL, 2024)

Termination of rewriting on reversible Boolean circuits as a free 3-category problem. - Adriano Barile; Stefano Berardi; Luca Roversi (Theor. Comput. Sci., 2025)