
Formal Methods in Computing (Most of the papers antecedent to 1995 are not included in the list) 

FRAMES NO FRAME 
Stefano Berardi  

Personal Home Page TypeHierarchical Overview  
Chronological Overview 
2017  
Berardi and de' Liguoro  "Nonmonotonic prefix points and Learning" Article: Fundamenta Informaticae. 
2014  
Berardi and de' Liguoro  "Knowledge Spaces and the Completeness of Learning Strategies (full version)" Article: Logical Methods in Computer Science. 
2013  
Berardi and de' Liguoro  "Nonmonotonic prefix points and Learning" In proceedings: FICS'13. 
2012  
Berardi and de' Liguoro  "Interactive realizers. A new approach to program extraction from non constructive proofs" Article: ACM Transactions on Computational Logic. 
Berardi and de' Liguoro  "Knowledge Spaces and the Completeness of Learning Strategies" In proceedings: CSL'12. 
2010  
Berardi and de' Liguoro  "Interactive Realizers and Monads" Unpublished. 
2009  
Berardi and de' Liguoro  "Toward the interpretation of nonconstructive reasoning as nonmonotonic learning" Article: Information and Computation. 
Berardi, Damiani and de' Liguoro  "Types for Proofs and Programs (International Conference TYPES 2008, Revised Selected Papers)" Book: LNCS, volume 5497, Springer. 
2008  
Berardi and de' Liguoro  "A Calculus of Realizers for EM1 Arithmetic" In proceedings: CSL'8. 
Berardi and Yamagata  "A sequent calculus for limit computable mathematics" Article. 
2007  
Berardi and de' Liguoro  "Limit of learning sequences with retractable guesses" Technical report. 
Berardi and Tatsuta  "Positive Arithmetic Without Exchange Is a Subclassical Logic" In proceedings. 
Berardi  "Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves" In proceedings. 
2006  
Berardi  "Some intuitionistic equivalents of classical principles for degree 2 formulas " Article. 
2005  
Berardi  "Classical Logic as Limit Completion" Article. 
2004  
Berardi  "A generalization of conservativity theorem for classical versus intuitionistic arithmetic" Article. 
Berardi and Berline  "Building continuous webbed models for System F" Article. 
Berardi and Valentini  "Krivine's intuitionistic proof of Classical Completeness" Article. 
Berardi, Coppo and Damiani  "Types for Proofs and Programs (International Workshop TYPES'03, Selected Papers)" Book: LNCS, volume 3085, Springer. 
2003  
Barbanera and Berardi  "A full continuous model of polymorphism" Article. 
2002  
Berardi and Berline  "Betaeta complete models for system F" Article. 
2000  
Berardi, Coppo, Damiani and Giannini  "TypeBased UselessCode Elimination for Functional Programs" In proceedings: Workshop SAIG'00, LNCS 1924, pages 172189, Springer. 
1999  
Berardi  "Intuitionistic Completness for First Order Classical Logic" Article. 
Berardi and de' Liguoro  "Total Functionals and WellFounded Strategies" In proceedings: TLCA'99. 
1998  
Baratella and Berardi  "Approximating Classical Theorems" Article. 
Baratella and Berardi  "Constructivization via Approximations and Examples" In proceedings. 
Berardi, Bezem and Coquand  "On the Computational Content of the Axiom of Choice" Article. 
1997  
Baratella and Berardi  "A Parallel Game Semantic for Linear Logic" Article. 
Baratella and Berardi  "Yet Another Constructivization of Classical logic" In proceedings. 
Barbanera and Berardi  "The SimplyTyped Theory of betaconversion has no Maximum Extension" Article. 
Barbanera, Berardi and Schivalocchi  "``Classical'' programmingwithproofs in $\lambda Sym$_{PA}:an analysis of nonconfluence" In proceedings. 
Berardi and Boerio  "Minimum Information Code in a Pure Functional Language with Data Types" In proceedings. 
1996  
Barbanera and Berardi  "A Constructive Valuation Semantics for Classical Logic" Article. 
Barbanera and Berardi  "A Symmetric LambdaCalculus for Classical Program Extraction" Article. 
Barbanera and Berardi  "Proofirrelevance out of Excludedmiddle and Choice in the Calculus of Constructions" Article. 
Berardi  "Pruning Simply Typed Lambda Terms" Article. 
Berardi and Coppo  "Types for Proofs and Programs 95'" Book. 
1995  
Barbanera and Berardi  "A Strong Normalization Result for Classical Logic" Article. 
Berardi, Bezem and Coquand  "A realization of the negative interpretation of the Axiom of Choice" In proceedings. 
Berardi and Coppo  "Types for Proofs and Programs (International Workshop TYPES'95, Selected Papers)" Book. 
Berardi and Boerio  "Using Subtyping in Program Optimization" In proceedings. 
1994  
Barbanera and Berardi  "A Symmetric LambdaCalculus for Classical Program Extraction" In proceedings. 
1993  
Barbanera and Berardi  "Extracting Constructive Content from Classical Logic via Controllike Reductions" In proceedings. 
Barbanera and Berardi  "Witness Extraction in Classical Logic through Normalization" In a collection. 
Berardi  "An application of PER model to Program Extraction" Article. 
Berardi  "Encoding of Data Types in Pure Construction Calculus: a semantic justification" In proceedings. 
1992  
Barbanera and Berardi  "A Constructive Valuation Interpretation for Classical Logic and its Use in Witness Extraction" In proceedings. 
Barbanera and Berardi  "Continuations and Simple Types: A strong Normalization Result" In proceedings. 
1991  
Berardi  "Retraction on dIdomains as a Model of Type:Type" Article. 
1988  
Berardi  "Equalization of Finite Flowers" Article. 
Berardi  "Equalization of Finite Flowers" Article. 

Formal Methods in Computing (Most of the papers antecedent to 1995 are not included in the list) 

FRAMES NO FRAME 
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)