Stefano Berardi - researchr profile publications

researchr

You are not signed in
Sign in
Sign up

Publications with a 'Stefano Berardi' as author, editor, or advisor:

26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, ItalyUgo de'Liguoro, Stefano Berardi, Thorsten Altenkirch, editors, Volume 188 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. [doi]
Equalization of Finite FlowersStefano Berardi. JSYML, 53(1):105-123, 1988.
A realization of the negative interpretation of the Axiom of ChoiceStefano Berardi, Marc Bezem, Thierry Coquand. tlca 1995: 47-62
Proof-Irrelevance out of Exluded-Middle and Choice in the Calculus of ConstructionsFranco Barbanera, Stefano Berardi. JFP, 6(3):519-525, 1996.
Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category ProblemAdriano Barile, Stefano Berardi, Luca Roversi. ictcs 2023: 31-43 [doi]
Internal Normalization, Compilation and Decompilation for System ::::F::::::bh::Stefano Berardi, Makoto Tatsuta. FLOPS 2010: 207-223 [doi]
A Constructive Valuation Interpretation for Classical Logic and its Use in Witness ExtractionFranco Barbanera, Stefano Berardi. caap 1992: 1-23
Non-Commutative Infinitary Peano ArithmeticMakoto Tatsuta, Stefano Berardi. csl 2011: 538-552 [doi]
Pruning Simply Typed Lambda-TermsStefano Berardi. logcom, 6(5):663-681, 1996.
Classical logic as limit completionStefano Berardi. mscs, 15(1):167-200, 2005. [doi]
Toward the interpretation of non-constructive reasoning as non-monotonic learningStefano Berardi, Ugo de Liguoro. iandc, 207(1):63-81, 2009. [doi]
Proving termination of programs having transition invariants of height ωStefano Berardi, Paulo Oliva, Silvia Steila. ictcs 2014: 237-240 [doi]
Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof SystemStefano Berardi, Makoto Tatsuta. fossacs 2017: 301-317 [doi]
An analysis of the Podelski-Rybalchenko termination theorem via bar recursionStefano Berardi, Paulo Oliva, Silvia Steila. logcom, 29(4):555-575, 2019. [doi]
Equivalence of inductive definitions and cyclic proofs under arithmeticStefano Berardi, Makoto Tatsuta. lics 2017: 1-12 [doi]
Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected PapersStefano Berardi, Mario Coppo, Ferruccio Damiani, editors, Volume 3085 of Lecture Notes in Computer Science, Springer, 2004.
Retractions on dI-domains as a model for Type:TypeStefano Berardi. iandc, 94(2):204-231, October 1991.
Minimum Information Code in a Pure Functional Language with Data TypesStefano Berardi, Luca Boerio. tlca 1997: 30-45
Types for Proofs and Programs, International Workshop TYPES 95, Torino, Italy, June 5-8, 1995, Selected PapersStefano Berardi, Mario Coppo, editors, Volume 1158 of Lecture Notes in Computer Science, Springer, 1996.
Type-Based Useless-Code Elimination for Functional ProgramsStefano Berardi, Mario Coppo, Ferruccio Damiani, Paola Giannini. saig 2000: 172-189 [doi]
A Symmetric Lambda Calculus for Classical Program ExtractionFranco Barbanera, Stefano Berardi. tacs 1994: 495-515
Games with 1-backtrackingStefano Berardi, Thierry Coquand, Susumu Hayashi. galop 2005: 210-225
A Symmetric Lambda Calculus for Classical Program ExtractionFranco Barbanera, Stefano Berardi. iandc, 125(2):103-117, 1996.
Interactive Realizers: A New Approach to Program Extraction from Nonconstructive ProofsStefano Berardi, Ugo de'Liguoro. tocl, 13(2):11, 2012. [doi]
A generalization of a conservativity theorem for classical versus intuitionistic arithmeticStefano Berardi. mlq, 50(1):41-46, 2004. [doi]
Building continuous webbed models for system FStefano Berardi, Chantal Berline. ENTCS, 35:3-33, 2000. [doi]
Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic ProofsStefano Berardi, Makoto Tatsuta. cmcs 2018: 13-33 [doi]
Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable MovesStefano Berardi. tlca 2007: 23-38 [doi]
Positive Arithmetic Without Exchange Is a Subclassical LogicStefano Berardi, Makoto Tatsuta. aplas 2007: 271-285 [doi]
Intuitionistic Completeness for First Order Classical LogicStefano Berardi. JSYML, 64(1):304-312, 1999.
A sequent calculus for limit computable mathematicsStefano Berardi, Yoriyuki Yamagata. APAL, 153(1-3):111-126, 2008. [doi]
Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1Federico Aschieri, Stefano Berardi. tlca 2009: 20-34 [doi]
On the Computational Content of the Axiom of ChoiceStefano Berardi, Marc Bezem, Thierry Coquand. JSYML, 63(2):600-622, 1998.
Non-monotonic Pre-fix Points and LearningStefano Berardi, Ugo de'Liguoro. FUIN, 150(3-4):259-280, 2017. [doi]
A full continuous model of polymorphismFranco Barbanera, Stefano Berardi. TCS, 290(1):407-428, 2003.
Knowledge Spaces and the Completeness of Learning StrategiesStefano Berardi, Ugo de'Liguoro. csl 2012: 77-91 [doi]
Using Subtyping in Program OptimizationStefano Berardi, Luca Boerio. tlca 1995: 63-77
Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1Federico Aschieri, Stefano Berardi, Giovanni Birolo. csl 2013: 45-60 [doi]
Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected PapersStefano Berardi, Ferruccio Damiani, Ugo de Liguoro, editors, Volume 5497 of Lecture Notes in Computer Science, Springer, 2009. [doi]
A Strong Normalization Result for Classical LogicFranco Barbanera, Stefano Berardi. APAL, 76(2):99-116, 1995.
A General Constructive Form of Higman's LemmaStefano Berardi, Gabriele Buriola, Peter Schuster 0001. csl 2024: [doi]
Approximating Classical TheoremsStefano Baratella, Stefano Berardi. logcom, 8(6):839-854, 1998.
Internal models of system F for decompilationStefano Berardi, Makoto Tatsuta. TCS, 435:3-20, 2012. [doi]
PrefaceSteffen van Bakel, Stefano Berardi, Ulrich Berger. APAL, 164(6):589-590, 2013. [doi]
An Arithmetical Hierarchy of the Law of Excluded Middle and Related PrinciplesYohji Akama, Stefano Berardi, Susumu Hayashi, Ulrich Kohlenbach. lics 2004: 192-201 [doi]
BetaEta-Complete Models for System FStefano Berardi, Chantal Berline. mscs, 12(6):823-874, 2002.
A Calculus of Realizers for EM1 Arithmetic (Extended Abstract)Stefano Berardi, Ugo de Liguoro. csl 2008: 215-229 [doi]
Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic ArithmeticStefano Berardi, Silvia Steila. TYPES 2014: 64-83 [doi]
Building continuous webbed models for system FStefano Berardi, Chantal Berline. TCS, 315(1):3-34, 2004. [doi]
A Constructive Valuation Semantics for Classical LogicFranco Barbanera, Stefano Berardi. ndjfl, 37(3):462-482, 1996.
An intuitionistic version of Ramsey's Theorem and its use in Program TerminationStefano Berardi, Silvia Steila. APAL, 166(12):1382-1406, 2015. [doi]
Ramsey Theorem as an Intuitionistic Property of Well Founded RelationsStefano Berardi, Silvia Steila. RTA 2014: 93-107 [doi]
Ramsey's Theorem for Pairs and k Colors as a sub-Classical Principle of ArithmeticStefano Berardi, Silvia Steila. JSYML, 82(2):737-753, 2017. [doi]
Games with Sequential Backtracking and Complete Game Semantics for Subclassical LogicsStefano Berardi, Makoto Tatsuta. tlca 2013: 61-76 [doi]
Classical Programming-with-Proofs in lambda::PA:::::Sym:::: An Analysis of Non-confluenceFranco Barbanera, Stefano Berardi, Massimo Schivalocchi. tacs 1997: 365-390
Krivine s intuitionistic proof of classical completeness (for countable languages)Stefano Berardi, Silvio Valentini. APAL, 129(1-3):93-106, 2004. [doi]
Total Functionals and Well-Founded StrategiesStefano Berardi, Ugo de Liguoro. tlca 1999: 54-68 [doi]
Some intuitionistic equivalents of classical principles for degree 2 formulasStefano Berardi. APAL, 139(1-3):185-200, 2006. [doi]
An Application of PER Models to Program ExtractionStefano Berardi. mscs, 3(3):309-331, 1993.
The Simply-Typed Theory of Beta-Conversion has no Maximum ExtensionFranco Barbanera, Stefano Berardi. iandc, 139(1):57-61, 1997.
Extracting Constructive Content from Classical Logic via Control-like ReductionsFranco Barbanera, Stefano Berardi. tlca 1993: 45-59
Calculi, types and applications: Essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi Della RoccaStefano Berardi, Ugo de Liguoro. TCS, 398(1-3):1-11, 2008. [doi]
Games with 1-backtrackingStefano Berardi, Thierry Coquand, Susumu Hayashi. APAL, 161(10):1254-1269, 2010. [doi]
PrefaceSteffen van Bakel, Stefano Berardi, Ulrich Berger. APAL, 161(11):1313-1314, 2010. [doi]
PrefaceSteffen van Bakel, Stefano Berardi. APAL, 153(1-3):1-2, 2008. [doi]
Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-FoundednessStefano Berardi. csl 2015: 343-358 [doi]
Termination of rewriting on reversible Boolean circuits as a free 3-category problemAdriano Barile, Stefano Berardi, Luca Roversi. TCS, 1028:115031, 2025. [doi]
Non-monotonic Pre-fix Points and LearningStefano Berardi, Ugo de'Liguoro. FUIN, 150(3-4):259-280, 2017. [doi]
A parallel game semantics for Linear LogicStefano Baratella, Stefano Berardi. AML, 36(3):189-217, 1997. [doi]
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic ProofsStefano Berardi, Makoto Tatsuta. lmcs, 15(3), 2019. [doi]

runs on WebDSL