@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", }