Andreas Abel (2008):
Polarized Subtyping for Sized Types.
Mathematical Structures in Computer Science 18(5),
pp. 797–822.
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 citeseer.ist.psu.edu/barendregt92lambda.html.
Luca Cardelli (1990):
Notes about F^ω_<:.
Unpublished manuscript.
Luca Cardelli & Giuseppe Longo (1991):
A semantic basis for Quest.
Journal of Functional Programming 1(4),
pp. 417–458.
Adriana Compagnoni (1995):
Higher-Order Subtyping with Intersection Types.
University of Nijmegen.
Adriana Compagnoni & Healfdene Goguen (1997):
Decidability of Higher-Order Subtyping via Logical Relations.
Available at ftp://www.dcs.ed.ac.uk/pub/hhg/hosdec.ps.gz.
A later version is published as CompagnoniAGoguenH:TOSHOSInfComp..
Adriana Compagnoni & Healfdene Goguen (2003):
Typed Operational Semantics for Higher-Order Subtyping.
Information and Computation 184(2),
pp. 242–297.
Adriana Compagnoni & Healfdene Goguen (2006):
Anti-symmetry of Higher-Order Subtyping.
Mathematical Structures in Computer Science 16(1),
pp. 41–65.
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.
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:http://doi.acm.org/10.1145/1042038.1042041.
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.
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.
Christopher A. Stone & Robert Harper (2006):
Extensional equivalence and singleton types..
ACM Trans. Comput. Log. 7(4),
pp. 676–722.
Available at http://doi.acm.org/10.1145/1183278.1183281.
Thomas Streicher (1991):
Semantics of Type Theory: Correctness, Completeness and Independence Results.
Birkhäuser.