1. Andreas Abel (2008): Polarized Subtyping for Sized Types. Mathematical Structures in Computer Science 18(5), pp. 797–822.
  2. Henk Barendregt (1992): Lambda Calculi with Types. In: Handbook of Logic in Computer Science, Volumes 1 (Background: Mathematical Structures) and 2 (Background: Computational Structures), Abramsky & Gabbay & Maibaum (Eds.), Clarendon 2. Oxford University Press. Available at
  3. Luca Cardelli (1990): Notes about F^ω_<:. Unpublished manuscript.
  4. Luca Cardelli & Giuseppe Longo (1991): A semantic basis for Quest. Journal of Functional Programming 1(4), pp. 417–458.
  5. Adriana Compagnoni (1995): Higher-Order Subtyping with Intersection Types. University of Nijmegen.
  6. Adriana Compagnoni & Healfdene Goguen (1997): Decidability of Higher-Order Subtyping via Logical Relations. Available at A later version is published as CompagnoniAGoguenH:TOSHOSInfComp..
  7. Adriana Compagnoni & Healfdene Goguen (2003): Typed Operational Semantics for Higher-Order Subtyping. Information and Computation 184(2), pp. 242–297.
  8. Adriana Compagnoni & Healfdene Goguen (2006): Anti-symmetry of Higher-Order Subtyping. Mathematical Structures in Computer Science 16(1), pp. 41–65.
  9. Adriana Compagnoni & Healfdene Goguen (2007): Subtyping à la Church. In: Erik Barendsen, Venanzio Capretta, Herman Geuvers & Milad Niqui: Reflections on Type Theory, λ-calculus, and the Mind. Essays dedicated to Henk Barendregt on the Occasion of his 60th Birthday. Radboud University Nijmegen.
  10. Robert Harper & Frank Pfenning (2005): On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Logic 6(1), pp. 61–101, doi:
  11. John C. Mitchell (1990): Toward a Typed Foundation for Method Specialization and Inheritance. In: Proceedings of the 17th ACM Symposium on Principles of Programming Languages, pp. 109–124.
  12. Martin Steffen & Benjamin Pierce (1997): Higher-Order Subtyping. Theoretical Computer Science 176(1–2), pp. 235–282. Corrigendum in TCS vol. 184 (1997), p. 247.
  13. Christopher A. Stone & Robert Harper (2006): Extensional equivalence and singleton types.. ACM Trans. Comput. Log. 7(4), pp. 676–722. Available at
  14. Thomas Streicher (1991): Semantics of Type Theory: Correctness, Completeness and Independence Results. Birkhäuser.

Comments and questions to:
For website issues: