Paper Info
Title
Subtyping, recursion, and parametric polymorphism in kernel fun
Abstract
We study subtype checking for recursive types in system kernel Fun, a typed λ-calculus with subtyping and bounded second-order polymorphism. Along the lines of [ACM Transactions on Programming Languages and Systems, 15(4) (1993) 575], we define a subtype relation over kernel Fun recursive types, and prove it to be transitive. We then show that the natural extension of the algorithm introduced in [ACM Transactions on Programming Languages and Systems, 15(4) (1993) 575] to compare first-order recursive types yields a non-complete algorithm. Finally, we prove the completeness and correctness of a different algorithm, which lends itself to efficient implementations.
Year
DOI
Venue
2005
10.1016/j.ic.2004.11.003
Inf. Comput.
Keywords
Field
DocType
subtyping,kernel fun,different algorithm,type theory and type systems,programming languages,non-complete algorithm,subtype checking,recursive types,subtype relation,acm transactions,kernel fun recursive type,kernel fun.,recursive type,first-order recursive types yield,subtyping recursion,system kernel fun,non complete algorithm,parametric polymorphism,polymorphism,type theory,second order,type system,first order
Kernel (linear algebra),Discrete mathematics,System programming,Parametric polymorphism,Correctness,Subtyping,Completeness (statistics),Recursion,Mathematics,Bounded function
Journal
Volume
Issue
ISSN
198
2
Information and Computation
Citations 
PageRank 
References 
3
0.43
22
Authors
2
Name
Order
Citations
PageRank
Dario Colazzo128334.21
Giorgio Ghelli21300255.19