@inproceedings{4307e9af362748bd87356d0ee429944a,
title = "Syntactically Restricting Bounded Polymorphism for Decidable Subtyping",
abstract = "Subtyping of Bounded Polymorphism has long been known to be undecidable when coupled with contra-variance. While decidable forms of bounded polymorphism exist, they all sacrifice either useful properties such as contra-variance (Kernel F< :), or useful metatheoretic properties (F<:⊤). In this paper we show how, by syntactically separating contra-variance from the recursive aspects of subtyping in System F< :, decidable subtyping can be ensured while also allowing for both contra-variant subtyping of certain instances of bounded polymorphism, and many of System F< :{\textquoteright}s desirable metatheoretic properties. We then show that this approach can be applied to the related polymorphism present in D< :, a minimal calculus that models core features of the Scala type system.",
keywords = "Functional languages, Language design, Object oriented languages, Polymorphism",
author = "Julian Mackay and Alex Potanin and Jonathan Aldrich and Lindsay Groves",
note = "Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 18th Asian Symposium on Programming Languages and Systems, APLAS 2020 ; Conference date: 30-11-2020 Through 02-12-2020",
year = "2020",
doi = "10.1007/978-3-030-64437-6\_7",
language = "English",
isbn = "978-3-030-64436-9",
series = "Lecture Notes in Computer Science ",
publisher = "Springer Science+Business Media B.V.",
pages = "125--144",
editor = "Oliveira, \{Bruno C.\}",
booktitle = "Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings",
address = "Netherlands",
}