| 2024 | CSL | A General Constructive Form of Higman's Lemma. | Stefano Berardi, Gabriele Buriola, Peter Schuster |
| 2017 | FOSSACS | Classical System of Martin-Lf's Inductive Definitions Is Not Equivalent to Cyclic Proof System. | Stefano Berardi, Makoto Tatsuta |
| 2017 | LICS | Equivalence of inductive definitions and cyclic proofs under arithmetic. | Stefano Berardi, Makoto Tatsuta |
| 2015 | CSL | Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness. | Stefano Berardi |
| 2013 | CSL | Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1. | Federico Aschieri, Stefano Berardi, Giovanni Birolo |
| 2012 | CSL | Knowledge Spaces and the Completeness of Learning Strategies. | Stefano Berardi, Ugo de'Liguoro |
| 2011 | CSL | Non-Commutative Infinitary Peano Arithmetic. | Makoto Tatsuta, Stefano Berardi |
| 2010 | FLOPS | Internal Normalization, Compilation and Decompilation for System | Stefano Berardi, Makoto Tatsuta |
| 2008 | CSL | A Calculus of Realizers for EM1 Arithmetic (Extended Abstract). | Stefano Berardi, Ugo de'Liguoro |
| 2007 | APLAS | Positive Arithmetic Without Exchange Is a Subclassical Logic. | Stefano Berardi, Makoto Tatsuta |
| 2004 | LICS | An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. | Yohji Akama, Stefano Berardi, Susumu Hayashi, Ulrich Kohlenbach |