|
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 Type-Hierarchical Overview | |
| Chronological Overview | |
| 2017 | |
| Berardi and de' Liguoro | "Non-monotonic pre-fix 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 | "Non-monotonic pre-fix 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 non-constructive reasoning as non-monotonic 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 | "Beta-eta complete models for system F" Article. |
| 2000 | |
| Berardi, Coppo, Damiani and Giannini | "Type-Based Useless-Code Elimination for Functional Programs" In proceedings: Workshop SAIG'00, LNCS 1924, pages 172-189, Springer. |
| 1999 | |
| Berardi | "Intuitionistic Completness for First Order Classical Logic" Article. |
| Berardi and de' Liguoro | "Total Functionals and Well-Founded 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 Simply-Typed Theory of beta-conversion has no Maximum Extension" Article. |
| Barbanera, Berardi and Schivalocchi | "``Classical'' programming-with-proofs in :an analysis of non-confluence" 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 Lambda-Calculus for Classical Program Extraction" Article. |
| Barbanera and Berardi | "Proof-irrelevance out of Excluded-middle 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 Lambda-Calculus for Classical Program Extraction" In proceedings. |
| 1993 | |
| Barbanera and Berardi | "Extracting Constructive Content from Classical Logic via Control-like 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 dI-domains 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)