2009 |
41 | EE | Stefano Berardi,
Ugo de'Liguoro:
Toward the interpretation of non-constructive reasoning as non-monotonic learning.
Inf. Comput. 207(1): 63-81 (2009) |
2008 |
40 | EE | Stefano Berardi,
Ugo de'Liguoro:
A Calculus of Realizers for EM1 Arithmetic (Extended Abstract).
CSL 2008: 215-229 |
39 | EE | Steffen van Bakel,
Stefano Berardi:
Preface.
Ann. Pure Appl. Logic 153(1-3): 1-2 (2008) |
38 | EE | Stefano Berardi,
Yoriyuki Yamagata:
A sequent calculus for limit computable mathematics.
Ann. Pure Appl. Logic 153(1-3): 111-126 (2008) |
37 | EE | 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) |
2007 |
36 | EE | Stefano Berardi,
Makoto Tatsuta:
Positive Arithmetic Without Exchange Is a Subclassical Logic.
APLAS 2007: 271-285 |
35 | EE | Stefano Berardi:
Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves.
TLCA 2007: 23-38 |
2006 |
34 | EE | Stefano Berardi:
Some intuitionistic equivalents of classical principles for degree 2 formulas.
Ann. Pure Appl. Logic 139(1-3): 185-200 (2006) |
2005 |
33 | | Stefano Berardi,
Thierry Coquand,
Susumu Hayashi:
Games with 1-backtracking.
GALOP 2005: 210-225 |
32 | EE | Stefano Berardi:
Classical logic as limit completion.
Mathematical Structures in Computer Science 15(1): 167-200 (2005) |
2004 |
31 | | 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
Springer 2004 |
30 | EE | Yohji Akama,
Stefano Berardi,
Susumu Hayashi,
Ulrich Kohlenbach:
An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles.
LICS 2004: 192-201 |
29 | EE | Stefano Berardi,
Silvio Valentini:
Krivine's intuitionistic proof of classical completeness (for countable languages).
Ann. Pure Appl. Logic 129(1-3): 93-106 (2004) |
28 | EE | Stefano Berardi:
A generalization of a conservativity theorem for classical versus intuitionistic arithmetic.
Math. Log. Q. 50(1): 41-46 (2004) |
27 | EE | Stefano Berardi,
Chantal Berline:
Building continuous webbed models for system F.
Theor. Comput. Sci. 315(1): 3-34 (2004) |
2003 |
26 | | Franco Barbanera,
Stefano Berardi:
A full continuous model of polymorphism.
Theor. Comput. Sci. 290(1): 407-428 (2003) |
2002 |
25 | | Stefano Berardi,
Chantal Berline:
BetaEta-Complete Models for System F.
Mathematical Structures in Computer Science 12(6): 823-874 (2002) |
2000 |
24 | EE | Stefano Berardi,
Mario Coppo,
Ferruccio Damiani,
Paola Giannini:
Type-Based Useless-Code Elimination for Functional Programs.
SAIG 2000: 172-189 |
23 | EE | Stefano Berardi,
Chantal Berline:
Building continuous webbed models for system F.
Electr. Notes Theor. Comput. Sci. 35: (2000) |
1999 |
22 | EE | Stefano Berardi,
Ugo de'Liguoro:
Total Functionals and Well-Founded Strategies.
TLCA 1999: 54-68 |
21 | | Stefano Berardi:
Intuitionistic Completeness for First Order Classical Logic.
J. Symb. Log. 64(1): 304-312 (1999) |
1998 |
20 | | Stefano Baratella,
Stefano Berardi:
Approximating Classical Theorems.
J. Log. Comput. 8(6): 839-854 (1998) |
19 | | Stefano Berardi,
Marc Bezem,
Thierry Coquand:
On the Computational Content of the Axiom of Choice.
J. Symb. Log. 63(2): 600-622 (1998) |
1997 |
18 | | Franco Barbanera,
Stefano Berardi,
Massimo Schivalocchi:
"Classical" Programming-with-Proofs in lambdaPASym: An Analysis of Non-confluence.
TACS 1997: 365-390 |
17 | | Stefano Berardi,
Luca Boerio:
Minimum Information Code in a Pure Functional Language with Data Types.
TLCA 1997: 30-45 |
16 | EE | Stefano Baratella,
Stefano Berardi:
A parallel game semantics for Linear Logic.
Arch. Math. Log. 36(3): 189-217 (1997) |
15 | | Franco Barbanera,
Stefano Berardi:
The Simply-Typed Theory of Beta-Conversion has no Maximum Extension.
Inf. Comput. 139(1): 57-61 (1997) |
1996 |
14 | | Stefano Berardi,
Mario Coppo:
Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers
Springer 1996 |
13 | | Franco Barbanera,
Stefano Berardi:
A Symmetric Lambda Calculus for Classical Program Extraction.
Inf. Comput. 125(2): 103-117 (1996) |
12 | | 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) |
11 | | Stefano Berardi:
Pruning Simply Typed Lambda-Terms.
J. Log. Comput. 6(5): 663-681 (1996) |
10 | | Franco Barbanera,
Stefano Berardi:
A Constructive Valuation Semantics for Classical Logic.
Notre Dame Journal of Formal Logic 37(3): 462-482 (1996) |
1995 |
9 | | Stefano Berardi,
Marc Bezem,
Thierry Coquand:
A realization of the negative interpretation of the Axiom of Choice.
TLCA 1995: 47-62 |
8 | | Stefano Berardi,
Luca Boerio:
Using Subtyping in Program Optimization.
TLCA 1995: 63-77 |
7 | | Franco Barbanera,
Stefano Berardi:
A Strong Normalization Result for Classical Logic.
Ann. Pure Appl. Logic 76(2): 99-116 (1995) |
1994 |
6 | | Franco Barbanera,
Stefano Berardi:
A Symmetric Lambda Calculus for "Classical" Program Extraction.
TACS 1994: 495-515 |
1993 |
5 | | Franco Barbanera,
Stefano Berardi:
Extracting Constructive Content from Classical Logic via Control-like Reductions.
TLCA 1993: 45-59 |
4 | | Stefano Berardi:
An Application of PER Models to Program Extraction.
Mathematical Structures in Computer Science 3(3): 309-331 (1993) |
1992 |
3 | | Franco Barbanera,
Stefano Berardi:
A Constructive Valuation Interpretation for Classical Logic and its Use in Witness Extraction.
CAAP 1992: 1-23 |
1991 |
2 | | Stefano Berardi:
Retractions on dI-domains as a model for Type:Type
Inf. Comput. 94(2): 204-231 (1991) |
1988 |
1 | | Stefano Berardi:
Equalization of Finite Flowers.
J. Symb. Log. 53(1): 105-123 (1988) |