Stefano Berardi

83 papers A* 2B 8Misc 1Journal 45Unranked 20
YearRankTypeTitle / Venue / Authors
2025 J jnl
Termination of rewriting on reversible Boolean circuits as a free 3-category problem.
Theor. Comput. Sci.
Adriano Barile, Stefano Berardi, Luca Roversi
2024 B conf
A General Constructive Form of Higman's Lemma.
CSL
Stefano Berardi, Gabriele Buriola, Peter Schuster
2024 J jnl
Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem.
CoRR
Adriano Barile, Stefano Berardi, Luca Roversi
2023 — conf
Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem.
ICTCS
Adriano Barile, Stefano Berardi, Luca Roversi
2021 — ed.
26th International Conference on Types for Proofs and Programs, TYPES 2020, University of Turin, Italy, March 2-5, 2020
TYPES
Ugo de'Liguoro, Stefano Berardi, Thorsten Altenkirch
2019 J jnl
An analysis of the Podelski-Rybalchenko termination theorem via bar recursion.
J. Log. Comput.
Stefano Berardi, Paulo Oliva, Silvia Steila
2019 J jnl
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs.
Log. Methods Comput. Sci.
Stefano Berardi, Makoto Tatsuta
2018 — conf
Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs.
CMCS
Stefano Berardi, Makoto Tatsuta
2018 — ed.
Proceedings Seventh International Workshop on Classical Logic and Computation, CL&C 2018, Oxford (UK), 7th of July 2018.
CL&C
Stefano Berardi, Alexandre Miquel
2017 J jnl
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs.
CoRR
Stefano Berardi, Makoto Tatsuta
2017 B conf
Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System.
FoSSaCS
Stefano Berardi, Makoto Tatsuta
2017 J jnl
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic.
CoRR
Stefano Berardi, Makoto Tatsuta
2017 A* conf
Equivalence of inductive definitions and cyclic proofs under arithmetic.
LICS
Stefano Berardi, Makoto Tatsuta
2017 J jnl
Non-monotonic Pre-fix Points and Learning.
Fundam. Informaticae
Stefano Berardi, Ugo de'Liguoro
2017 J jnl
Ramsey's Theorem for Pairs and k Colors as a sub-Classical Principle of Arithmetic.
J. Symb. Log.
Stefano Berardi, Silvia Steila
2016 J jnl
A Sound, Complete and Effective Second Order Game Semantics.
CoRR
Stefano Berardi
2016 — ed.
Proceedings Sixth International Workshop on Classical Logic and Computation, CL&C 2016, Porto, Portugal , 23th June 2016.
CL&C
Ulrich Kohlenbach, Steffen van Bakel, Stefano Berardi
2016 J jnl
Ramsey's Theorem for Pairs and $k$ Colors as a Sub-Classical Principle of Arithmetic.
CoRR
Stefano Berardi, Silvia Steila
2015 J jnl
An intuitionistic version of Ramsey's Theorem and its use in Program Termination.
Ann. Pure Appl. Log.
Stefano Berardi, Silvia Steila
2015 B conf
Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness.
CSL
Stefano Berardi
2014 J jnl
An intuitionistic version of Ramsey Theorem (italian version).
CoRR
Stefano Berardi
2014 J jnl
Knowledge Spaces and the Completeness of Learning Strategies.
Log. Methods Comput. Sci.
Stefano Berardi, Ugo de'Liguoro
2014 — conf
Proving termination of programs having transition invariants of height ω.
ICTCS
Stefano Berardi, Paulo Oliva, Silvia Steila
2014 J jnl
Proving termination with transition invariants of height omega.
CoRR
Stefano Berardi, Paulo Oliva, Silvia Steila
2014 — conf
Ramsey Theorem as an Intuitionistic Property of Well Founded Relations.
RTA-TLCA
Stefano Berardi, Silvia Steila
2013 — conf
Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics.
TLCA
Stefano Berardi, Makoto Tatsuta
2013 — conf
Non-monotonic Pre-fixed Points and Learning.
FICS
Stefano Berardi, Ugo de'Liguoro
2013 J jnl
Preface.
Ann. Pure Appl. Log.
Steffen van Bakel, Stefano Berardi, Ulrich Berger
2013 — conf
Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic.
TYPES
Stefano Berardi, Silvia Steila
2013 B conf
Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1.
CSL
Federico Aschieri, Stefano Berardi, Giovanni Birolo
2012 J jnl
Interactive Realizers: A New Approach to Program Extraction from Nonconstructive Proofs.
ACM Trans. Comput. Log.
Stefano Berardi, Ugo de'Liguoro
2012 J jnl
Internal models of system F for decompilation.
Theor. Comput. Sci.
Stefano Berardi, Makoto Tatsuta
2012 B conf
Knowledge Spaces and the Completeness of Learning Strategies.
CSL
Stefano Berardi, Ugo de'Liguoro
2011 B conf
Non-Commutative Infinitary Peano Arithmetic.
CSL
Makoto Tatsuta, Stefano Berardi
2010 J jnl
Games with 1-backtracking.
Ann. Pure Appl. Log.
Stefano Berardi, Thierry Coquand, Susumu Hayashi
2010 J jnl
Interactive Learning-Based Realizability for Heyting Arithmetic with EM1
Log. Methods Comput. Sci.
Federico Aschieri, Stefano Berardi
2010 J jnl
Interactive Realizers and Monads
CoRR
Stefano Berardi, Ugo de'Liguoro
2010 Misc conf
Internal Normalization, Compilation and Decompilation for System
FLOPS
Stefano Berardi, Makoto Tatsuta
2010 J jnl
Preface.
Ann. Pure Appl. Log.
Steffen van Bakel, Stefano Berardi, Ulrich Berger
2010 — ed.
Proceedings Third International Workshop on Classical Logic and Computation, CL&C 2010, Brno, Czech Republic, 21-22 August 2010.
CL&C
Steffen van Bakel, Stefano Berardi, Ulrich Berger
2009 — conf
Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1.
TLCA
Federico Aschieri, Stefano Berardi
2009 J jnl
Toward the interpretation of non-constructive reasoning as non-monotonic learning.
Inf. Comput.
Stefano Berardi, Ugo de'Liguoro
2009 — ed.
Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers
TYPES
Stefano Berardi, Ferruccio Damiani, Ugo de'Liguoro
2008 B conf
A Calculus of Realizers for EM1 Arithmetic (Extended Abstract).
CSL
Stefano Berardi, Ugo de'Liguoro
2008 J jnl
A sequent calculus for limit computable mathematics.
Ann. Pure Appl. Log.
Stefano Berardi, Yoriyuki Yamagata
2008 J jnl
Calculi, types and applications: Essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi Della Rocca.
Theor. Comput. Sci.
Stefano Berardi, Ugo de'Liguoro
2008 J jnl
Preface.
Ann. Pure Appl. Log.
Steffen van Bakel, Stefano Berardi
2007 B conf
Positive Arithmetic Without Exchange Is a Subclassical Logic.
APLAS
Stefano Berardi, Makoto Tatsuta
2007 — conf
Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves.
TLCA
Stefano Berardi
2006 J jnl
Some intuitionistic equivalents of classical principles for degree 2 formulas.
Ann. Pure Appl. Log.
Stefano Berardi
2005 J jnl
Classical logic as limit completion.
Math. Struct. Comput. Sci.
Stefano Berardi
2005 — conf
Games with 1-backtracking.
GALOP@ETAPS
Stefano Berardi, Thierry Coquand, Susumu Hayashi
2004 J jnl
A generalization of a conservativity theorem for classical versus intuitionistic arithmetic.
Math. Log. Q.
Stefano Berardi
2004 A* conf
An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles.
LICS
Yohji Akama, Stefano Berardi, Susumu Hayashi, Ulrich Kohlenbach
2004 J jnl
Building continuous webbed models for system F.
Theor. Comput. Sci.
Stefano Berardi, Chantal Berline
2004 J jnl
Krivine's intuitionistic proof of classical completeness (for countable languages).
Ann. Pure Appl. Log.
Stefano Berardi, Silvio Valentini
2004 — ed.
Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers
TYPES
Stefano Berardi, Mario Coppo, Ferruccio Damiani
2003 J jnl
A full continuous model of polymorphism.
Theor. Comput. Sci.
Franco Barbanera, Stefano Berardi
2002 J jnl
BetaEta-Complete Models for System F.
Math. Struct. Comput. Sci.
Stefano Berardi, Chantal Berline
2000 — conf
Type-Based Useless-Code Elimination for Functional Programs.
SAIG
Stefano Berardi, Mario Coppo, Ferruccio Damiani, Paola Giannini
1999 J jnl
Intuitionistic Completeness for First Order Classical Logic.
J. Symb. Log.
Stefano Berardi
1999 — conf
Total Functionals and Well-Founded Strategies.
TLCA
Stefano Berardi, Ugo de'Liguoro
1998 J jnl
Approximating Classical Theorems.
J. Log. Comput.
Stefano Baratella, Stefano Berardi
1998 — conf
Building continuous webbed models for system F.
Workshop on Domains
Stefano Berardi, Chantal Berline
1998 J jnl
On the Computational Content of the Axiom of Choice.
J. Symb. Log.
Stefano Berardi, Marc Bezem, Thierry Coquand
1997 — conf
"Classical" Programming-with-Proofs in lambda
TACS
Franco Barbanera, Stefano Berardi, Massimo Schivalocchi
1997 J jnl
A parallel game semantics for Linear Logic.
Arch. Math. Log.
Stefano Baratella, Stefano Berardi
1997 — conf
Minimum Information Code in a Pure Functional Language with Data Types.
TLCA
Stefano Berardi, Luca Boerio
1997 J jnl
The Simply-Typed Theory of Beta-Conversion has no Maximum Extension.
Inf. Comput.
Franco Barbanera, Stefano Berardi
1996 J jnl
A Constructive Valuation Semantics for Classical Logic.
Notre Dame J. Formal Log.
Franco Barbanera, Stefano Berardi
1996 J jnl
A Symmetric Lambda Calculus for Classical Program Extraction.
Inf. Comput.
Franco Barbanera, Stefano Berardi
1996 J jnl
Proof-Irrelevance out of Exluded-Middle and Choice in the Calculus of Constructions.
J. Funct. Program.
Franco Barbanera, Stefano Berardi
1996 J jnl
Pruning Simply Typed Lambda-Terms.
J. Log. Comput.
Stefano Berardi
1996 — ed.
Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers
TYPES
Stefano Berardi, Mario Coppo
1995 J jnl
A Strong Normalization Result for Classical Logic.
Ann. Pure Appl. Log.
Franco Barbanera, Stefano Berardi
1995 — conf
A realization of the negative interpretation of the Axiom of Choice.
TLCA
Stefano Berardi, Marc Bezem, Thierry Coquand
1995 — conf
Using Subtyping in Program Optimization.
TLCA
Stefano Berardi, Luca Boerio
1994 — conf
A Symmetric Lambda Calculus for "Classical" Program Extraction.
TACS
Franco Barbanera, Stefano Berardi
1993 J jnl
An Application of PER Models to Program Extraction.
Math. Struct. Comput. Sci.
Stefano Berardi
1993 — conf
Extracting Constructive Content from Classical Logic via Control-like Reductions.
TLCA
Franco Barbanera, Stefano Berardi
1992 — conf
A Constructive Valuation Interpretation for Classical Logic and its Use in Witness Extraction.
CAAP
Franco Barbanera, Stefano Berardi
1991 J jnl
Retractions on dI-domains as a model for Type:Type
Inf. Comput.
Stefano Berardi
1988 J jnl
Equalization of Finite Flowers.
J. Symb. Log.
Stefano Berardi