File Download

There are no files associated with this item.

  Links for fulltext
     (May Require Subscription)
Supplementary

Article: A dependently typed calculus with polymorphic subtyping

TitleA dependently typed calculus with polymorphic subtyping
Authors
KeywordsDependent types
Polymorphism
Subtyping
Type systems
Issue Date2021
PublisherElsevier BV. The Journal's web site is located at http://www.elsevier.com/locate/scico
Citation
Science of Computer Programming, 2021, v. 208, p. article no. 102655 How to Cite?
AbstractA polymorphic subtyping relation, which relates more general types to more specific ones, is at the core of many modern functional languages. As those languages start moving towards dependently typed programming a natural question is how can polymorphic subtyping be adapted to such settings. This paper presents the dependent implicitly polymorphic calculus (λI∀): a simple dependently typed calculus with polymorphic subtyping. The subtyping relation in λI∀ generalizes the well-known polymorphic subtyping relation by Odersky and Läufer (1996). Because λI∀ is dependently typed, integrating subtyping in the calculus is non-trivial. To overcome many of the issues arising from integrating subtyping with dependent types, the calculus employs unified subtyping, which is a technique that unifies typing and subtyping into a single relation. Moreover, λI∀ employs explicit casts instead of a conversion rule, allowing unrestricted recursion to be naturally supported. We prove various non-trivial results, including type soundness and transitivity of unified subtyping. λI∀ and all corresponding proofs are mechanized in the Coq theorem prover. © 2021 Elsevier B.V.
Persistent Identifierhttp://hdl.handle.net/10722/301198
ISSN
2023 Impact Factor: 1.5
2023 SCImago Journal Rankings: 0.511
ISI Accession Number ID

 

DC FieldValueLanguage
dc.contributor.authorXUE, M-
dc.contributor.authorDos Santos Oliveira, BCDS-
dc.date.accessioned2021-07-27T08:07:35Z-
dc.date.available2021-07-27T08:07:35Z-
dc.date.issued2021-
dc.identifier.citationScience of Computer Programming, 2021, v. 208, p. article no. 102655-
dc.identifier.issn0167-6423-
dc.identifier.urihttp://hdl.handle.net/10722/301198-
dc.description.abstractA polymorphic subtyping relation, which relates more general types to more specific ones, is at the core of many modern functional languages. As those languages start moving towards dependently typed programming a natural question is how can polymorphic subtyping be adapted to such settings. This paper presents the dependent implicitly polymorphic calculus (λI∀): a simple dependently typed calculus with polymorphic subtyping. The subtyping relation in λI∀ generalizes the well-known polymorphic subtyping relation by Odersky and Läufer (1996). Because λI∀ is dependently typed, integrating subtyping in the calculus is non-trivial. To overcome many of the issues arising from integrating subtyping with dependent types, the calculus employs unified subtyping, which is a technique that unifies typing and subtyping into a single relation. Moreover, λI∀ employs explicit casts instead of a conversion rule, allowing unrestricted recursion to be naturally supported. We prove various non-trivial results, including type soundness and transitivity of unified subtyping. λI∀ and all corresponding proofs are mechanized in the Coq theorem prover. © 2021 Elsevier B.V.-
dc.languageeng-
dc.publisherElsevier BV. The Journal's web site is located at http://www.elsevier.com/locate/scico-
dc.relation.ispartofScience of Computer Programming-
dc.subjectDependent types-
dc.subjectPolymorphism-
dc.subjectSubtyping-
dc.subjectType systems-
dc.titleA dependently typed calculus with polymorphic subtyping-
dc.typeArticle-
dc.identifier.emailDos Santos Oliveira, BCDS: bruno@cs.hku.hk-
dc.identifier.authorityDos Santos Oliveira, BCDS=rp01786-
dc.description.naturelink_to_subscribed_fulltext-
dc.identifier.doi10.1016/j.scico.2021.102655-
dc.identifier.scopuseid_2-s2.0-85104134831-
dc.identifier.hkuros323743-
dc.identifier.volume208-
dc.identifier.spagearticle no. 102655-
dc.identifier.epagearticle no. 102655-
dc.identifier.isiWOS:000652847700001-
dc.publisher.placeNetherlands-

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats