Stefano Berardi

Publication Activity (10 Years)

Years Active: 1988-2024
Publications (10 Years): 16

Top Topics

Rewrite Systems

Inductive Reasoning

Top Venues

Log. Methods Comput. Sci.

Publications

Stefano Berardi, Gabriele Buriola, Peter Schuster
A General Constructive Form of Higman's Lemma. CSL (2024)
Adriano Barile, Stefano Berardi, Luca Roversi
Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem. CoRR (2024)
Adriano Barile, Stefano Berardi, Luca Roversi
Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem. ICTCS (2023)
Stefano Berardi, Paulo Oliva, Silvia Steila
An analysis of the Podelski-Rybalchenko termination theorem via bar recursion. J. Log. Comput. 29 (4) (2019)
Stefano Berardi, Makoto Tatsuta
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. Log. Methods Comput. Sci. 15 (3) (2019)
Stefano Berardi, Makoto Tatsuta
Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs. CMCS (2018)
Stefano Berardi, Makoto Tatsuta
Equivalence of inductive definitions and cyclic proofs under arithmetic. LICS (2017)
Stefano Berardi, Makoto Tatsuta
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic. CoRR (2017)
Stefano Berardi, Makoto Tatsuta
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. CoRR (2017)
Stefano Berardi, Silvia Steila
Ramsey's Theorem for Pairs and k Colors as a sub-Classical Principle of Arithmetic. J. Symb. Log. 82 (2) (2017)
Stefano Berardi, Makoto Tatsuta
Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System. FoSSaCS (2017)
Stefano Berardi, Ugo de'Liguoro
Non-monotonic Pre-fix Points and Learning. Fundam. Informaticae 150 (3-4) (2017)
Stefano Berardi, Silvia Steila
Ramsey's Theorem for Pairs and $k$ Colors as a Sub-Classical Principle of Arithmetic. CoRR (2016)
Stefano Berardi
A Sound, Complete and Effective Second Order Game Semantics. CoRR (2016)
Stefano Berardi
Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness. CSL (2015)
Stefano Berardi, Silvia Steila
An intuitionistic version of Ramsey's Theorem and its use in Program Termination. Ann. Pure Appl. Log. 166 (12) (2015)
Stefano Berardi
An intuitionistic version of Ramsey Theorem (italian version). CoRR (2014)
Stefano Berardi, Paulo Oliva, Silvia Steila
Proving termination of programs having transition invariants of height ω. ICTCS (2014)
Stefano Berardi, Paulo Oliva, Silvia Steila
Proving termination with transition invariants of height omega. CoRR (2014)
Stefano Berardi, Silvia Steila
Ramsey Theorem as an Intuitionistic Property of Well Founded Relations. RTA-TLCA (2014)
Stefano Berardi, Ugo de'Liguoro
Knowledge Spaces and the Completeness of Learning Strategies. Log. Methods Comput. Sci. 10 (1) (2014)
Stefano Berardi, Silvia Steila
Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic. TYPES (2013)
Federico Aschieri, Stefano Berardi, Giovanni Birolo
Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1. CSL (2013)
Stefano Berardi, Makoto Tatsuta
Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics. TLCA (2013)
Stefano Berardi, Ugo de'Liguoro
Non-monotonic Pre-fixed Points and Learning. FICS (2013)
Steffen van Bakel, Stefano Berardi, Ulrich Berger
Preface. Ann. Pure Appl. Log. 164 (6) (2013)
Stefano Berardi, Ugo de'Liguoro
Interactive Realizers: A New Approach to Program Extraction from Nonconstructive Proofs. ACM Trans. Comput. Log. 13 (2) (2012)
Stefano Berardi, Makoto Tatsuta
Internal models of system F for decompilation. Theor. Comput. Sci. 435 (2012)
Stefano Berardi, Ugo de'Liguoro
Knowledge Spaces and the Completeness of Learning Strategies. CSL (2012)
Makoto Tatsuta, Stefano Berardi
Non-Commutative Infinitary Peano Arithmetic. CSL (2011)
Federico Aschieri, Stefano Berardi
Interactive Learning-Based Realizability for Heyting Arithmetic with EM1 Log. Methods Comput. Sci. 6 (3) (2010)
Stefano Berardi, Thierry Coquand, Susumu Hayashi
Games with 1-backtracking. Ann. Pure Appl. Log. 161 (10) (2010)
Stefano Berardi, Ugo de'Liguoro
Interactive Realizers and Monads CoRR (2010)
Stefano Berardi, Makoto Tatsuta
. FLOPS (2010)
Steffen van Bakel, Stefano Berardi, Ulrich Berger
Preface. Ann. Pure Appl. Log. 161 (11) (2010)
Federico Aschieri, Stefano Berardi
Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1. TLCA (2009)
Stefano Berardi, Ugo de'Liguoro
Toward the interpretation of non-constructive reasoning as non-monotonic learning. Inf. Comput. 207 (1) (2009)
Stefano Berardi, Ugo de'Liguoro
A Calculus of Realizers for EM1 Arithmetic (Extended Abstract). CSL (2008)
Steffen van Bakel, Stefano Berardi
Preface. Ann. Pure Appl. Log. 153 (1-3) (2008)
Stefano Berardi, Yoriyuki Yamagata
A sequent calculus for limit computable mathematics. Ann. Pure Appl. Log. 153 (1-3) (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) (2008)
Stefano Berardi, Makoto Tatsuta
Positive Arithmetic Without Exchange Is a Subclassical Logic. APLAS (2007)
Stefano Berardi
Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves. TLCA (2007)
Stefano Berardi
Some intuitionistic equivalents of classical principles for degree 2 formulas. Ann. Pure Appl. Log. 139 (1-3) (2006)
Stefano Berardi
Classical logic as limit completion. Math. Struct. Comput. Sci. 15 (1) (2005)
Stefano Berardi, Thierry Coquand, Susumu Hayashi
Games with 1-backtracking. GALOP@ETAPS (2005)
Stefano Berardi, Chantal Berline
Building continuous webbed models for system F. Theor. Comput. Sci. 315 (1) (2004)
Yohji Akama, Stefano Berardi, Susumu Hayashi, Ulrich Kohlenbach
An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. LICS (2004)
Stefano Berardi, Silvio Valentini
Krivine's intuitionistic proof of classical completeness (for countable languages). Ann. Pure Appl. Log. 129 (1-3) (2004)
Stefano Berardi
A generalization of a conservativity theorem for classical versus intuitionistic arithmetic. Math. Log. Q. 50 (1) (2004)
Franco Barbanera, Stefano Berardi
A full continuous model of polymorphism. Theor. Comput. Sci. 290 (1) (2003)
Stefano Berardi, Chantal Berline
BetaEta-Complete Models for System F. Math. Struct. Comput. Sci. 12 (6) (2002)
Stefano Berardi, Mario Coppo, Ferruccio Damiani, Paola Giannini
Type-Based Useless-Code Elimination for Functional Programs. SAIG (2000)
Stefano Berardi, Chantal Berline
Building continuous webbed models for system F. Electron. Notes Theor. Comput. Sci. 35 (2000)
Stefano Berardi
Intuitionistic Completeness for First Order Classical Logic. J. Symb. Log. 64 (1) (1999)
Stefano Berardi, Ugo de'Liguoro
Total Functionals and Well-Founded Strategies. TLCA (1999)
Stefano Baratella, Stefano Berardi
Approximating Classical Theorems. J. Log. Comput. 8 (6) (1998)
Stefano Berardi, Marc Bezem, Thierry Coquand
On the Computational Content of the Axiom of Choice. J. Symb. Log. 63 (2) (1998)
Franco Barbanera, Stefano Berardi, Massimo Schivalocchi
: An Analysis of Non-confluence. TACS (1997)
Stefano Berardi, Luca Boerio
Minimum Information Code in a Pure Functional Language with Data Types. TLCA (1997)
Stefano Baratella, Stefano Berardi
A parallel game semantics for Linear Logic. Arch. Math. Log. 36 (3) (1997)
Franco Barbanera, Stefano Berardi
The Simply-Typed Theory of Beta-Conversion has no Maximum Extension. Inf. Comput. 139 (1) (1997)
Franco Barbanera, Stefano Berardi
Proof-Irrelevance out of Exluded-Middle and Choice in the Calculus of Constructions. J. Funct. Program. 6 (3) (1996)
Franco Barbanera, Stefano Berardi
A Symmetric Lambda Calculus for Classical Program Extraction. Inf. Comput. 125 (2) (1996)
Stefano Berardi
Pruning Simply Typed Lambda-Terms. J. Log. Comput. 6 (5) (1996)
Franco Barbanera, Stefano Berardi
A Constructive Valuation Semantics for Classical Logic. Notre Dame J. Formal Log. 37 (3) (1996)
Stefano Berardi, Marc Bezem, Thierry Coquand
A realization of the negative interpretation of the Axiom of Choice. TLCA (1995)
Stefano Berardi, Luca Boerio
Using Subtyping in Program Optimization. TLCA (1995)
Franco Barbanera, Stefano Berardi
A Strong Normalization Result for Classical Logic. Ann. Pure Appl. Log. 76 (2) (1995)
Franco Barbanera, Stefano Berardi
A Symmetric Lambda Calculus for "Classical" Program Extraction. TACS (1994)
Stefano Berardi
An Application of PER Models to Program Extraction. Math. Struct. Comput. Sci. 3 (3) (1993)
Franco Barbanera, Stefano Berardi
Extracting Constructive Content from Classical Logic via Control-like Reductions. TLCA (1993)
Franco Barbanera, Stefano Berardi
A Constructive Valuation Interpretation for Classical Logic and its Use in Witness Extraction. CAAP (1992)
Stefano Berardi
Retractions on dI-domains as a model for Type:Type Inf. Comput. 94 (2) (1991)
Stefano Berardi
Equalization of Finite Flowers. J. Symb. Log. 53 (1) (1988)