@InProceedings{BB1,
  author =       "F. Barbanera and S. Berardi",
  title =        "Witness Extraction in Classical logic through
                 normalization",
  booktitle =    "To appear in Proceeding of the 2nd BRA meeting on
                 Logical Frameworks",
  year =         "1992",
  classification = "LF",
  annote =       "\\In this paper we study strong normalization for
                 reductions on proofs in classical higher order systems,
                 improving a result of D. Prawitz. We show how such
                 property can be used to extract witnesses from
                 classical proofs of simply existential (i.e., $\sum
                 _{1}^{0} $) formulas.",
}

@InProceedings{BB2,
author =       "F. Barbanera and S. Berardi",
  title =        "A constructive semantic for Classical Logic and its
                 use in extracting witnesses from proofs.",
  booktitle =    "Proceedings of CAAP '92, Lecture Notes in Computer
                 Science 581",
  publisher =    "Springer Verlag",
  year =         "1992",
  classification = "LF",
  annote =       "\\A constructive interpretation of classical
                 arithmetic in terms of a Kripke-like valuation
                 semantics of proofs is presented. We use this
                 interpretation for motivating a constructive procedure,
                 based on reduction rules, for extracting witnesses from
                 proofs of Sigma-0-1 sentences in classical
                 arithmetic.",
}

@InProceedings{BaDe,
  author =       "Barbanera F. and Dezani M.",
  title =        "Intersection and Union Types",
  booktitle =    "Proc. of TACS '91, Lecture Notes in Computer Science
                 526",
  year =         "1991",
  publisher =    "Springer Verlag",
  classification = "LF",
  annote =       "\\An extension of the type assignment system with
                 intersection types is introduced and its syntactical
                 properties, as well as the semantic ones, are
                 investigated. The extension consists in the
                 introduction of a new type operator {"}union{"},
                 allowing to form, so to speak, finite unions of types.
                 The possibility of introducing even infinite union is
                 investigated as well.",
}

@Article{barbanera90ijfcs,
  topics =       "l-calculus, rewriting",
  location =     MF,
  author =       "F. Barbanera",
  title =        "Combining Term Rewriting and Type Assignment Systems",
  journal =      "IJFCS",
  year =         "1990",
  volume =       "1",
  pages =        "165--184",
}


@InProceedings{barbanera93icalp,
  author =       "Franco Barbanera and Maribel Fern{\'a}ndez",
 topics =       "l-calculus rewriting teamp",
  title =        "Modularity of termination and confluence in
                 combinations of rewrite systems with
                 {$\lambda_\omega$}",
  booktitle =    "Proceedings of the 20th International Colloquium on
                 Automata, Languages, and Programming",
  year =         "1993",
}

@InProceedings{barbanera93tlca,
  author =       "Franco Barbanera and Maribel Fern{\'a}ndez",
  topics =       "l-calculus rewriting teamp",
  title =        "Combining first and higher order rewrite systems with
                 type assignment systems",
  booktitle =    "Proceedings of the International Conference on Typed
                 Lambda Calculi and Applications, Utrecht, Holland",
  year =         "1993",
}

@Unpublished{BarbaneraB9+,
  title =        "A Symmetric Lambda Calculus for ``Classical'' Program
                 Extraction",
  author =       "Franco Barbanera and Stefano Berardi",
  journal =      "Information and Computation",
  note =         "Received for publication January 4, 1996",
}