Notice:

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have o ffered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Publications (most of the papers antecedent to 1995 are not included in the list below.)

• F. Barbanera. Combining term-rewriting and type-assignment systems. In Proceedings of the Third Italian Conference on Theoretical Computer Science. World Scientific Publishing Company, 1989.

• F. Barbanera. Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved. In Proceedings of Conditional and typed Term Rewriting Systems (CTRS '90), volume 516 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

• F. Barbanera. Combining term-rewriting and type-assignment systems. International Journal of Foundations of Computer Science, 1(3):165-184, 1990.

• F. Alessi and F. Barbanera. Strong conjunction and intersection types. In Proceedings of 16h international symposium on Mathematical Foundation of Computer Science (MFCS '91), volume 520 of Lecture Notes in Computer Science. Springer Verlag, 1991.

• F. Alessi and F. Barbanera. Toward a semantics for the quest language. In Proceedings of sixth annual symposium on Logic in Computer Science (LICS'91). IEEE, 1991.

• F. Barbanera and S. Berardi. A constructive valuation interpretation for classical logic and its use in witness extraction. In Proceedings of Colloquium on Trees in Algebra and programming (CAAP '92), volume 581 of Lecture Notes in Computer Science. Springer Verlag, 1992.

• F. Barbanera and S. Berardi. Continuations and simple types : A strong normalization result. In Proceedings of the ACM SIGPLAN Workshop on Continuations CW'92, Report No. STAN-CS-92-1426. University of Stanford, 1992.

• F. Barbanera and S. Berardi. Extracting constructive content from classical logic via control-like reductions. In Proceedings of first international Conference on Typed Lambda Calculus and Applications TLCA'93, volume 664 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

• F. Barbanera and S. Berardi. Witness extraction in classical logic through normalization. In G.Huet and G.Plotkin, editors, Logical Environments. Cambridge University Press, 1993.

• F. Barbanera and M. Fernandez. Combining first and higher-order rewrite systems with type assignment systems. In Proceedings of first international Conference on Typed Lambda Calculus and Applications (TLCA'93), volume 664 of Lecture Notes in Computer Science. Springer Verlag, 1993.

• F. Barbanera and M. Fernandez. Modularity of termination and confluence in combinations of rewrite systems with lambda _omega . In Proceedings of 20^th International Colloquium on Automata,Languages and Programming (ICALP'93), volume 700 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

• F. Alessi and F. Barbanera. Toward a semantics for the quest language. Informatique theorique et Applications/Theoretical Informatics and Applications, 28(6):513-555, 1994.

• F. Barbanera and S. Berardi. A symmetric lambda-calculus for ``classical'' program extraction. In Proceedings of TACS '94, number 789 in Lecture Notes in Computer Science. Springer-Verlag, 1994.

• F. Barbanera and S. Berardi. A strong normalization result for classical logic. Annals of Pure and Applied Logic, 76:99-116, 1995.

• F. Barbanera, M. Dezani-Ciancaglini, and U. de'Liguoro. ``Intersection and union types:syntax and semantics''. Information and Computation, 119:202-230, 1995.

• F. Barbanera and S. Berardi. A constructive valuation semantics for classical logic. Notre Dame Journal of Formal Logic, 37(3):462-482, 1996.

• F. Barbanera and S. Berardi. Proof-irrelevance out of excluded-middle and choice in the calculus of constructions. Journal of Functional Programming, 6(3):519-525, 1996.

• F. Barbanera and S. Berardi. A symmetric lambda-calculus for ``classical'' program extraction. Information and Computation, 125(2):103-117, 1996.

• F. Barbanera and M. Fernandez. Intersection type assignment systems with higher-order algebraic rewriting. Theoretical Computer Science, 170:173-207, 1996.

• F. Barbanera, S. Berardi, and M. Schivalocchi. ``classical'' programming-with-proofs in lambda ^Sym_PA:an analysis of non-confluence. Technical Report UTM 495, Dipartimento di Matematica, Universita' degli Studi di Trento, 1996.

• F. Barbanera, M. Fernandez, and H. Geuvers. Modularity of strong normalization in the algebraic- lambda -cube. Technical Report LIENS-96-8, Ecole Normale Superieure, 1996.

• S. van Bakel, F. Barbanera, and M. Fernandez. Approximation and normalization results for typable term rewriting systems with beta rule. In Proceedings of 6th European Symposium on Programming (ESOP'96), number 1058 in Lecture Notes in Computer Science. Springer-Verlag, 1996.

• A. Aoun, F. Barbanera, M. Dezani-Ciancaglini, and S. Mirasyedioglu. Principal typying for parallel and non-deterministic lambda calculus. Journal of Computing and Information Technology, 5(2):129-138, 1997.

• F. Barbanera and S. Berardi. The simply-typed theory of beta-conversion has no maximum extension. Information and Computation, 139(1):57-61, 1997.

• F. Barbanera, S. Berardi, and M. Schivalocchi. ``classical'' programming-with-proofs in lambda ^Sym_PA:an analysis of non-confluence. In Proceedings of TACS'97, number 1281 in Lecture Notes in Computer Science. Springer-Verlag, 1997.

• F. Barbanera, M. Fernandez, and H. Geuvers. Modularity of strong normalization in the algebraic- lambda -cube. Journal of Functional Programming, 7(6):613-660, 1997.

• F. Barbanera, M. Dezani-Ciancaglini, and F.-J. de Vries. Types for trees. In Proceedings of PROCOMET '98, pages 11-29. Chapman & Hall, London, 1998.

• S. van Bakel, F. Barbanera, M. Dezani-Ciancaglini, and F.-J. de Vries. Intersection types for lambda-trees. Theoretical Computer Science, 272, 3-40, 2002..

• S. van Bakel, F. Barbanera and M. Fernandez. Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and beta-rule . In Types for Proofs and Programs, LNCS 1956. Springer, 2000

• F. Barbanera and S. Berardi. A Full Continuous Model of Polymorphism. Theoretical Computer Science, 290, 407-428, 2003.

• Franco Barbanera, Mariangiola Dezani, Ivano Salvo, Vladimiro Sassone. A Type Inference Algorithm for Secure Ambients. In TOSCA 2001 Theory of Concurrency, Higher Order Languages and Types. Electronic Notes in Computer Science 62, 2002.

• Fabio Alessi, Franco Barbanera, Mariangiola Dezani-Ciancaglini. Intersection Types and Computational Rules. In proceedings 10th Workshop on Logic, Language, Information and Computation (WoLLIC'2003), ENTCS 84, 2003.

• Christopher Anderson, Franco Barbanera, Mariangiola Dezani-Ciancaglini, Sophia Drossopoulou. Can Addresses be Types? (a case study: objects with delegation). In proceedings WOOD'03, Electronic Notes in Computer Science. Elsevier, 82 No.8, 2003.

• Franco Barbanera, Mariangiola Dezani, Michele Bugliesi, Vladimiro Sassone. BoCa: A calculus of bounded capacities. In Proceedings ASIAN'03, volume 2896 of LNCS, pages 205-223, Springer, 2003.

• Christopher Anderson, Franco Barbanera, Mariangiola Dezani-Ciancaglini. Alias and Union Types for Delegation. Annals of Mathematics, Computing and Teleinformatics, Vol 1, No 1, 2003.

• Fabio Alessi, Franco Barbanera, Mariangiola Dezani-Ciancaglini. Tailoring Filter Models. In Proceedings Types 2003, LNCS n.3085, Springer-Verlag, 2003.

• Franco Barbanera, Ugo de'Liguoro. Type assignment for mobile objects Proceedings of the Final Workshop of the COMETA Project on Computational Metamodels, Electronic Notes in Theoretical Computer Science, Vol. 104C, pp. 25-38, 2004.