File Download
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.1145/3133871
- Scopus: eid_2-s2.0-85120116208
- WOS: WOS:000688014000003
- Find via
Supplementary
- Citations:
- Appears in Collections:
Article: Unifying typing and subtyping
Title | Unifying typing and subtyping |
---|---|
Authors | |
Issue Date | 2017 |
Publisher | Association for Computing Machinery: Open Access Journals. The Journal's web site is located at https://dl.acm.org/journal/pacmpl |
Citation | Proceedings of the ACM on Programming Languages, 2017, v. 1 n. OOPSLA, p. article no. 47 How to Cite? |
Abstract | In recent years dependent types have become a hot topic in programming language research. A key reason why dependent types are interesting is that they allow unifying types and terms, which enables both additional expressiveness and economy of concepts. Unfortunately there has been much less work on dependently typed calculi for object-oriented programming. This is partly because it is widely acknowledged that the combination between dependent types and subtyping is particularly challenging.
This paper presents λ I≤, which is a dependently typed generalization of System F≤. The resulting calculus follows the style of Pure Type Systems, and contains a single unified syntactic sort that accounts for expressions, types and kinds. To address the challenges posed by the combination of dependent types and subtyping, λ I≤ employs a novel technique that unifies typing and subtyping. In λ I≤ there is only a judgement that is akin to a typed version of subtyping. Both the typing relation, as well as type well-formedness are just special cases of the subtyping relation. The resulting calculus has a rich metatheory and enjoys of several standard and desirable properties, such as subject reduction, transitivity of subtyping, narrowing as well as standard substitution lemmas. All the metatheory of λ I≤ is mechanically proved in the Coq theorem prover. Furthermore, (and as far as we are aware) λ I≤ is the first dependently typed calculus that completely subsumes System F≤, while preserving various desirable properties. |
Persistent Identifier | http://hdl.handle.net/10722/301339 |
ISSN | 2023 Impact Factor: 2.2 2023 SCImago Journal Rankings: 1.242 |
ISI Accession Number ID |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | YANG, Y | - |
dc.contributor.author | Dos Santos Oliveira, BCDS | - |
dc.date.accessioned | 2021-07-27T08:09:38Z | - |
dc.date.available | 2021-07-27T08:09:38Z | - |
dc.date.issued | 2017 | - |
dc.identifier.citation | Proceedings of the ACM on Programming Languages, 2017, v. 1 n. OOPSLA, p. article no. 47 | - |
dc.identifier.issn | 2475-1421 | - |
dc.identifier.uri | http://hdl.handle.net/10722/301339 | - |
dc.description.abstract | In recent years dependent types have become a hot topic in programming language research. A key reason why dependent types are interesting is that they allow unifying types and terms, which enables both additional expressiveness and economy of concepts. Unfortunately there has been much less work on dependently typed calculi for object-oriented programming. This is partly because it is widely acknowledged that the combination between dependent types and subtyping is particularly challenging. This paper presents λ I≤, which is a dependently typed generalization of System F≤. The resulting calculus follows the style of Pure Type Systems, and contains a single unified syntactic sort that accounts for expressions, types and kinds. To address the challenges posed by the combination of dependent types and subtyping, λ I≤ employs a novel technique that unifies typing and subtyping. In λ I≤ there is only a judgement that is akin to a typed version of subtyping. Both the typing relation, as well as type well-formedness are just special cases of the subtyping relation. The resulting calculus has a rich metatheory and enjoys of several standard and desirable properties, such as subject reduction, transitivity of subtyping, narrowing as well as standard substitution lemmas. All the metatheory of λ I≤ is mechanically proved in the Coq theorem prover. Furthermore, (and as far as we are aware) λ I≤ is the first dependently typed calculus that completely subsumes System F≤, while preserving various desirable properties. | - |
dc.language | eng | - |
dc.publisher | Association for Computing Machinery: Open Access Journals. The Journal's web site is located at https://dl.acm.org/journal/pacmpl | - |
dc.relation.ispartof | Proceedings of the ACM on Programming Languages | - |
dc.rights | This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. | - |
dc.title | Unifying typing and subtyping | - |
dc.type | Article | - |
dc.identifier.email | Dos Santos Oliveira, BCDS: bruno@cs.hku.hk | - |
dc.identifier.authority | Dos Santos Oliveira, BCDS=rp01786 | - |
dc.description.nature | published_or_final_version | - |
dc.identifier.doi | 10.1145/3133871 | - |
dc.identifier.scopus | eid_2-s2.0-85120116208 | - |
dc.identifier.hkuros | 323720 | - |
dc.identifier.volume | 1 | - |
dc.identifier.issue | OOPSLA | - |
dc.identifier.spage | article no. 47 | - |
dc.identifier.epage | article no. 47 | - |
dc.identifier.isi | WOS:000688014000003 | - |
dc.publisher.place | United States | - |