My research interests include programming language semantics, type theory, subtyping, and object oriented programming.

I am teaching a course on Foundations Of Calculi With Subtypes And Objects (in Spanish). From 22nd to 30th of June, 1998 , at University of La Plata, Argentina.

• Adriana Compagnoni and Healfdene Goguen. Decidability of Higher-Order Subtyping via Logical Relations (.ps). December 1997.

• Adriana Compagnoni. Decidable Higher Order Subtyping. University of Edinburgh, LFCS report ECS-LFCS-97-365. Submitted for publication. September 1997.

• Adriana Compagnoni. Subject Reduction and Minimal Types for Higher Order Subtyping. University of Edinburgh, LFCS report ECS-LFCS-97-363. Submitted for publication. August 1997.

• Adriana Compagnoni and Healfdene Goguen. Typed Operational Semantics for Higher Order Subtyping. Revised version of University of Edinburgh, LFCS report ECS-LFCS-97-361. Submitted for publication. April 1997.

• Adriana Compagnoni and Maribel Fernández. An object calculus with algebraic rewriting (ps). April 1997. In Proceedings of the 9th International Symposium PLILP'97, Southampton, UK, September 3-5, 1997. Number 1292 in Lecture Notes in Computer Science. Springer-Verlag.

• Adriana Compagnoni, Ole Jensen, James Leifer, and Peter Sewell. Action calculus semantics for a functional programming language with mutable store. Technical report, University of Cambridge, Computer Laboratory, 1997. Forthcoming.

• David Aspinall and Adriana Compagnoni. Subtyping dependent types(.ps) or small ps for small-memory printers. July 1995. In Proceedings of the eleventh IEEE Symposium on Logic in Computer Science, July 27-30, 1996, New Brunswick, New Jersey, USA. Long version: LFCS report ECS-LFCS-97-370. October 1997. To appear in Theoretical Computer Science.

• Adriana B. Compagnoni. Higher-Order Subtyping with Intersection Types (ps) or dvi. Front cover (ps).PhD thesis, University of Nijmegen, The Netherlands, January 1995. ISBN 90-9007860-6.

• Adriana B. Compagnoni. Decidability of higher-order subtyping with intersection types. In Proceedings of the Annual Conference of the European Association for Computer Science Logic, CSL'94, Kazimierz, Poland, number 933 in Lecture Notes in Computer Science. Springer-Verlag, June 1995. Preliminary version available as University of Edinburgh technical report ECS-LFCS-94-281, January 1994, under the title: Subtyping in F-omega-meet is decidable.

• Adriana B. Compagnoni and Benjamin C. Pierce. Higher Order Intersection Types and Multiple Inheritance. Mathematical Structures in Computer Science, 1996, volume 6, pp 469-501. An earlier version appeared under the title: Multiple inheritance via intersection types as University of Edinburgh technical report ECS-LFCS-93-275 and Catholic University Nijmegen computer science technical report 93-18., Aug. 1993.

• Adriana B. Compagnoni and Veronica Gaspes. A type theory for ML. In Proceedings of the Tenth International Conference of the Chilean Computer Science Society. Ed. Dr. David Fuller. Pontificia Universidad Catolica de Chile, 1990.

My research is concentrated on the study of subtyping, a primitive relation important to many different areas of computer science, including software specification, object-oriented programming, modular software design, and computer-assisted proof.

My first research goal is to provide a theoretical basis for enriching proof-checking systems with subtyping. Existing proof checkers, such as Lego, Coq, NuPrl, and Alf do not incorporate subtyping. Joint work with David Aspinall proved that the addition of subtyping to type theories with dependent types preserves the decidability of typechecking.

My second research goal is to study subtyping systems for programming languages. Sustained research over the last decade has led recently to powerful new type systems for a broad range of object-oriented features. My research will have applications to Standard ML's successor ML2000 and to object calculi. In recent joint work with Healfdene Goguen we studied Typed Operational Semantics for Higher-Order Subtyping, and in Decidability of Higher-Order Subtyping via Logical Relations we used logical relations for the first time to establish a decidability result for subtyping. Maribel Fernández and I defined and studied and extension of Abadi and Cardelli's Object Calculi with Algebraic Rewriting.

My third research goal is to investigate the applications of typing and subtyping in concurrency.