default search action
Stefano Berardi
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [c31]Stefano Berardi, Gabriele Buriola, Peter Schuster:
A General Constructive Form of Higman's Lemma. CSL 2024: 16:1-16:17 - [i8]Adriano Barile, Stefano Berardi, Luca Roversi:
Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem. CoRR abs/2401.02091 (2024) - 2023
- [c30]Adriano Barile, Stefano Berardi, Luca Roversi:
Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem. ICTCS 2023: 31-43 - 2021
- [e7]Ugo de'Liguoro, Stefano Berardi, Thorsten Altenkirch
:
26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy. LIPIcs 188, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2021, ISBN 978-3-95977-182-5 [contents]
2010 – 2019
- 2019
- [j36]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) - [j35]Stefano Berardi, Paulo Oliva, Silvia Steila
An analysis of the Podelski-Rybalchenko termination theorem via bar recursion. J. Log. Comput. 29(4): 555-575 (2019) - 2018
- [c29]Stefano Berardi, Makoto Tatsuta:
Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs. CMCS 2018: 13-33 - [e6]Stefano Berardi, Alexandre Miquel:
Proceedings Seventh International Workshop on Classical Logic and Computation, CL&C 2018, Oxford (UK), 7th of July 2018. EPTCS 281, 2018 [contents] - 2017
- [j34]Stefano Berardi, Ugo de'Liguoro:
Non-monotonic Pre-fix Points and Learning. Fundam. Informaticae 150(3-4): 259-280 (2017) - [j33]Stefano Berardi, Silvia Steila
Ramsey's Theorem for Pairs and k Colors as a sub-Classical Principle of Arithmetic. J. Symb. Log. 82(2): 737-753 (2017) - [c28]Stefano Berardi, Makoto Tatsuta:
Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System. FoSSaCS 2017: 301-317 - [c27]Stefano Berardi, Makoto Tatsuta:
Equivalence of inductive definitions and cyclic proofs under arithmetic. LICS 2017: 1-12 - [i7]Stefano Berardi, Makoto Tatsuta:
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic. CoRR abs/1712.03502 (2017) - [i6]Stefano Berardi, Makoto Tatsuta:
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. CoRR abs/1712.09603 (2017) - 2016
- [e5]Ulrich Kohlenbach, Steffen van Bakel, Stefano Berardi:
Proceedings Sixth International Workshop on Classical Logic and Computation, CL&C 2016, Porto, Portugal , 23th June 2016. EPTCS 213, 2016 [contents] - [i5]Stefano Berardi, Silvia Steila:
Ramsey's Theorem for Pairs and $k$ Colors as a Sub-Classical Principle of Arithmetic. CoRR abs/1601.01891 (2016) - [i4]Stefano Berardi:
A Sound, Complete and Effective Second Order Game Semantics. CoRR abs/1610.08845 (2016) - 2015
- [j32]Stefano Berardi, Silvia Steila
An intuitionistic version of Ramsey's Theorem and its use in Program Termination. Ann. Pure Appl. Log. 166(12): 1382-1406 (2015) - [c26]Stefano Berardi:
Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness. CSL 2015: 343-358 - 2014
- [j31]Stefano Berardi, Ugo de'Liguoro:
Knowledge Spaces and the Completeness of Learning Strategies. Log. Methods Comput. Sci. 10(1) (2014) - [c25]Stefano Berardi, Paulo Oliva, Silvia Steila:
Proving termination of programs having transition invariants of height ω. ICTCS 2014: 237-240 - [c24]Stefano Berardi, Silvia Steila:
Ramsey Theorem as an Intuitionistic Property of Well Founded Relations. RTA-TLCA 2014: 93-107 - [i3]Stefano Berardi:
An intuitionistic version of Ramsey Theorem (italian version). CoRR abs/1401.2515 (2014) - [i2]Stefano Berardi, Paulo Oliva, Silvia Steila:
Proving termination with transition invariants of height omega. CoRR abs/1407.4692 (2014) - 2013
- [j30]Steffen van Bakel
Preface. Ann. Pure Appl. Log. 164(6): 589-590 (2013) - [c23]Federico Aschieri, Stefano Berardi, Giovanni Birolo:
Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1. CSL 2013: 45-60 - [c22]Stefano Berardi, Makoto Tatsuta:
Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics. TLCA 2013: 61-76 - [c21]Stefano Berardi, Silvia Steila:
Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic. TYPES 2013: 64-83 - [c20]Stefano Berardi, Ugo de'Liguoro:
Non-monotonic Pre-fixed Points and Learning. FICS 2013: 1-10 - 2012
- [j29]Stefano Berardi, Makoto Tatsuta:
Internal models of system F for decompilation. Theor. Comput. Sci. 435: 3-20 (2012) - [j28]Stefano Berardi, Ugo de'Liguoro:
Interactive Realizers: A New Approach to Program Extraction from Nonconstructive Proofs. ACM Trans. Comput. Log. 13(2): 11:1-11:21 (2012) - [c19]Stefano Berardi, Ugo de'Liguoro:
Knowledge Spaces and the Completeness of Learning Strategies. CSL 2012: 77-91 - 2011
- [c18]Makoto Tatsuta, Stefano Berardi:
Non-Commutative Infinitary Peano Arithmetic. CSL 2011: 538-552 - 2010
- [j27]Stefano Berardi, Thierry Coquand, Susumu Hayashi:
Games with 1-backtracking. Ann. Pure Appl. Log. 161(10): 1254-1269 (2010) - [j26]Steffen van Bakel
Preface. Ann. Pure Appl. Log. 161(11): 1313-1314 (2010) - [j25]Federico Aschieri, Stefano Berardi:
Interactive Learning-Based Realizability for Heyting Arithmetic with EM1. Log. Methods Comput. Sci. 6(3) (2010) - [c17]Stefano Berardi, Makoto Tatsuta:
Internal Normalization, Compilation and Decompilation for System Fbh. FLOPS 2010: 207-223 - [e4]Steffen van Bakel, Stefano Berardi, Ulrich Berger:
Proceedings Third International Workshop on Classical Logic and Computation, CL&C 2010, Brno, Czech Republic, 21-22 August 2010. EPTCS 47, 2010 [contents] - [i1]Stefano Berardi, Ugo de'Liguoro:
Interactive Realizers and Monads. CoRR abs/1005.2907 (2010)
2000 – 2009
- 2009
- [j24]Stefano Berardi, Ugo de'Liguoro:
Toward the interpretation of non-constructive reasoning as non-monotonic learning. Inf. Comput. 207(1): 63-81 (2009) - [c16]Federico Aschieri, Stefano Berardi:
Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1. TLCA 2009: 20-34 - [e3]Stefano Berardi, Ferruccio Damiani
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 [contents] - 2008
- [j23]Steffen van Bakel
Preface. Ann. Pure Appl. Log. 153(1-3): 1-2 (2008) - [j22]Stefano Berardi, Yoriyuki Yamagata
A sequent calculus for limit computable mathematics. Ann. Pure Appl. Log. 153(1-3): 111-126 (2008) - [j21]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) - [c15]Stefano Berardi, Ugo de'Liguoro:
A Calculus of Realizers for EM1 Arithmetic (Extended Abstract). CSL 2008: 215-229 - 2007
- [c14]Stefano Berardi, Makoto Tatsuta:
Positive Arithmetic Without Exchange Is a Subclassical Logic. APLAS 2007: 271-285 - [c13]Stefano Berardi:
Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves. TLCA 2007: 23-38 - 2006
- [j20]Stefano Berardi:
Some intuitionistic equivalents of classical principles for degree 2 formulas. Ann. Pure Appl. Log. 139(1-3): 185-200 (2006) - 2005
- [j19]Stefano Berardi:
Classical logic as limit completion. Math. Struct. Comput. Sci. 15(1): 167-200 (2005) - [c12]Stefano Berardi, Thierry Coquand, Susumu Hayashi:
Games with 1-backtracking. GALOP@ETAPS 2005: 210-225 - 2004
- [j18]Stefano Berardi, Silvio Valentini:
Krivine's intuitionistic proof of classical completeness (for countable languages). Ann. Pure Appl. Log. 129(1-3): 93-106 (2004) - [j17]Stefano Berardi:
A generalization of a conservativity theorem for classical versus intuitionistic arithmetic. Math. Log. Q. 50(1): 41-46 (2004) - [j16]Stefano Berardi, Chantal Berline:
Building continuous webbed models for system F. Theor. Comput. Sci. 315(1): 3-34 (2004) - [c11]Yohji Akama
An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. LICS 2004: 192-201 - [e2]Stefano Berardi, Mario Coppo, Ferruccio Damiani
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 [contents] - 2003
- [j15]Franco Barbanera, Stefano Berardi:
A full continuous model of polymorphism. Theor. Comput. Sci. 290(1): 407-428 (2003) - 2002
- [j14]Stefano Berardi, Chantal Berline:
BetaEta-Complete Models for System F. Math. Struct. Comput. Sci. 12(6): 823-874 (2002) - 2000
- [c10]Stefano Berardi, Mario Coppo, Ferruccio Damiani, Paola Giannini
Type-Based Useless-Code Elimination for Functional Programs. SAIG 2000: 172-189
1990 – 1999
- 1999
- [j13]Stefano Berardi:
Intuitionistic Completeness for First Order Classical Logic. J. Symb. Log. 64(1): 304-312 (1999) - [c9]Stefano Berardi, Ugo de'Liguoro:
Total Functionals and Well-Founded Strategies. TLCA 1999: 54-68 - 1998
- [j12]Stefano Berardi, Marc Bezem, Thierry Coquand:
On the Computational Content of the Axiom of Choice. J. Symb. Log. 63(2): 600-622 (1998) - [j11]Stefano Baratella
Approximating Classical Theorems. J. Log. Comput. 8(6): 839-854 (1998) - [c8]Stefano Berardi, Chantal Berline:
Building continuous webbed models for system F. Workshop on Domains 1998: 3-33 - 1997
- [j10]Stefano Baratella
A parallel game semantics for Linear Logic. Arch. Math. Log. 36(3): 189-217 (1997) - [j9]Franco Barbanera, Stefano Berardi:
The Simply-Typed Theory of Beta-Conversion has no Maximum Extension. Inf. Comput. 139(1): 57-61 (1997) - [c7]Franco Barbanera, Stefano Berardi, Massimo Schivalocchi:
"Classical" Programming-with-Proofs in lambdaPASym: An Analysis of Non-confluence. TACS 1997: 365-390 - [c6]Stefano Berardi, Luca Boerio:
Minimum Information Code in a Pure Functional Language with Data Types. TLCA 1997: 30-45 - 1996
- [j8]Franco Barbanera, Stefano Berardi:
A Symmetric Lambda Calculus for Classical Program Extraction. Inf. Comput. 125(2): 103-117 (1996) - [j7]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) - [j6]Stefano Berardi:
Pruning Simply Typed Lambda-Terms. J. Log. Comput. 6(5): 663-681 (1996) - [j5]Franco Barbanera, Stefano Berardi:
A Constructive Valuation Semantics for Classical Logic. Notre Dame J. Formal Log. 37(3): 462-482 (1996) - [e1]Stefano Berardi, Mario Coppo:
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 [contents] - 1995
- [j4]Franco Barbanera, Stefano Berardi:
A Strong Normalization Result for Classical Logic. Ann. Pure Appl. Log. 76(2): 99-116 (1995) - [c5]Stefano Berardi, Marc Bezem, Thierry Coquand:
A realization of the negative interpretation of the Axiom of Choice. TLCA 1995: 47-62 - [c4]Stefano Berardi, Luca Boerio:
Using Subtyping in Program Optimization. TLCA 1995: 63-77 - 1994
- [c3]Franco Barbanera, Stefano Berardi:
A Symmetric Lambda Calculus for "Classical" Program Extraction. TACS 1994: 495-515 - 1993
- [j3]Stefano Berardi:
An Application of PER Models to Program Extraction. Math. Struct. Comput. Sci. 3(3): 309-331 (1993) - [c2]Franco Barbanera, Stefano Berardi:
Extracting Constructive Content from Classical Logic via Control-like Reductions. TLCA 1993: 45-59 - 1992
- [c1]Franco Barbanera, Stefano Berardi:
A Constructive Valuation Interpretation for Classical Logic and its Use in Witness Extraction. CAAP 1992: 1-23 - 1991
- [j2]Stefano Berardi:
Retractions on dI-domains as a model for Type:Type. Inf. Comput. 94(2): 204-231 (1991)
1980 – 1989
- 1988
- [j1]Stefano Berardi:
Equalization of Finite Flowers. J. Symb. Log. 53(1): 105-123 (1988)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:22 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: