BERARDI, Stefano
BERARDI, Stefano
INFORMATICA
"A Symmetric Lambda-Calculus for ``Classical'' Program Extraction"
1996-01-01 F. BARBANERA; S. BERARDI
"On the Constructive Content of the Axiom of Choice."
1998-01-01 S. BERARDI; M. BEZEM; T. COQUAND
"Proof-irrelevance out of Excluded Middle and Choice in the Calculus of Constructions."
1996-01-01 F. BARBANERA; S. BERARDI
"Pruning Simply Typed Lambda Terms"
1996-01-01 S. BERARDI
"Termination of Rewriting on Reversible Boolean Circuits as a free 3-Category problem" Adriano Barile, Stefano Berardi and Luca Roversi ICTCS 2023 24th Italian Conference on Theoretical Computer Science 2023, Manuela Flore, Giuseppe Romana Editors CEUR Workshop Proceedings
2023-01-01 Adriano Barile, Stefano Berardi, Luca Roversi
26th International Conference on Types for Proofs and Programs, TYPES 2020
2021-01-01 Ugo de'Liguoro, Stefano Berardi, Thorsten Altenkirch
A Calculus of Realizers for EM1-Arithmetic
2008-01-01 Stefano Berardi; Ugo De' Liguoro
A Full Continuous Model of Polymorphism
2003-01-01 F. BARBANERA.; S. BERARDI
A generalization of conservativity theorem for classical versus intuitionistic arithmetic
2004-01-01 S. BERARDI
A sequent calculus for limit computable mathematics
2008-01-01 Stefano Berardi; Yoriyuki Yamagata
An analysis of the Podelski–Rybalchenko termination theorem via bar recursion
2019-01-01 Berardi, Stefano; Oliva, Paulo; Steila, Silvia
An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles
2004-01-01 S. BERARDI; Y. AKAMA; S. HAYASHI; U. KOHLENBACK
An intuitionistic version of Ramsey Theorem and its use in Program Termination
2015-01-01 Stefano, Berardi; Silvia, Steila
Beta-eta-complete models for System F
2002-01-01 S. BERARDI; C. BERLINE
Building Continuous Webbed Model for system F
2004-01-01 S. BERARDI; C. BERLINE
Calculi, types and applications: Essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi Della Rocca
2008-01-01 Stefano Berardi; Ugo de' Liguoro
Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness
2015-01-01 BERARDI, Stefano
Classical Logic as Limit Completion
2005-01-01 S. BERARDI
Classical system of Martin-Lof's inductive definitions is not equivalent to cyclic proof system
2017-01-01 Berardi, Stefano; Tatsuta, Makoto
Equivalence of inductive definitions and cyclic proofs under arithmetic
2017-01-01 Berardi, Stefano; Tatsuta, Makoto