Paper Info
Title
Higher-Order Subtyping
Abstract
System F! is an extension with subtyping of Girard's higher-order polymorphic -calculus. We developthe fundamental metatheory of this calculus: decidability of fi-conversion on well-kinded types, eliminationof the "cut-rule" of transitivity from the subtype relation, and the soundness, completeness, andtermination of algorithms for subtyping and typechecking.Keywords: lambda-calculus, type systems, subtyping, polymorphism, bounded quantification,typechecking.1 IntroductionSince the ...
Year
Venue
Keywords
1994
PROCOMET
higher-order subtyping,polymorphism,higher order,type system,lambda calculus
Field
DocType
ISBN
Programming language,Subtyping,Mathematics
Conference
0-444-82020-5
Citations 
PageRank 
References 
19
1.36
17
Authors
2
Name
Order
Citations
PageRank
Martin Steffen112210.32
Benjamin C. Pierce24196302.91