File Download
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.1145/3428291
- Scopus: eid_2-s2.0-85097587094
- WOS: WOS:000685203900100
- Find via
Supplementary
- Citations:
- Appears in Collections:
Article: Revisiting iso-recursive subtyping
Title | Revisiting iso-recursive subtyping |
---|---|
Authors | |
Keywords | Formalization Iso-recursive types Subtyping |
Issue Date | 2020 |
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, 2020, v. 4 n. OOPSLA, article no. 223 How to Cite? |
Abstract | The Amber rules are well-known and widely used for subtyping iso-recursive types. They were first briefly and informally introduced in 1985 by Cardelli in a manuscript describing the Amber language. Despite their use over many years, important aspects of the metatheory of the iso-recursive style Amber rules have not been studied in depth or turn out to be quite challenging to formalize.
This paper aims to revisit the problem of subtyping iso-recursive types. We start by introducing a novel declarative specification that we believe captures the “spirit” of Amber-style iso-recursive subtyping. Informally, the specification states that two recursive types are subtypes if all their finite unfoldings are subtypes. The Amber rules are shown to be sound with respect to this declarative specification. We then derive a sound, complete and decidable algorithmic formulation of subtyping that employs a novel double unfolding rule. Compared to the Amber rules, the double unfolding rule has the advantage of: 1) being modular; 2) not requiring reflexivity to be built in; and 3) leading to an easy proof of transitivity of subtyping. This work sheds new insights on the theory of subtyping iso-recursive types, and the new double unfolding rule has important advantages over the original Amber rules for both implementations and metatheoretical studies involving recursive types. All results are mechanically formalized in the Coq theorem prover. As far as we know, this is the first comprehensive treatment of iso-recursive subtyping dealing with unrestricted recursive types in a theorem prover. |
Persistent Identifier | http://hdl.handle.net/10722/301197 |
ISSN | 2023 Impact Factor: 2.2 2023 SCImago Journal Rankings: 1.242 |
ISI Accession Number ID |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | ZHOU, Y | - |
dc.contributor.author | Dos Santos Oliveira, BCDS | - |
dc.contributor.author | ZHAO, J | - |
dc.date.accessioned | 2021-07-27T08:07:34Z | - |
dc.date.available | 2021-07-27T08:07:34Z | - |
dc.date.issued | 2020 | - |
dc.identifier.citation | Proceedings of the ACM on Programming Languages, 2020, v. 4 n. OOPSLA, article no. 223 | - |
dc.identifier.issn | 2475-1421 | - |
dc.identifier.uri | http://hdl.handle.net/10722/301197 | - |
dc.description.abstract | The Amber rules are well-known and widely used for subtyping iso-recursive types. They were first briefly and informally introduced in 1985 by Cardelli in a manuscript describing the Amber language. Despite their use over many years, important aspects of the metatheory of the iso-recursive style Amber rules have not been studied in depth or turn out to be quite challenging to formalize. This paper aims to revisit the problem of subtyping iso-recursive types. We start by introducing a novel declarative specification that we believe captures the “spirit” of Amber-style iso-recursive subtyping. Informally, the specification states that two recursive types are subtypes if all their finite unfoldings are subtypes. The Amber rules are shown to be sound with respect to this declarative specification. We then derive a sound, complete and decidable algorithmic formulation of subtyping that employs a novel double unfolding rule. Compared to the Amber rules, the double unfolding rule has the advantage of: 1) being modular; 2) not requiring reflexivity to be built in; and 3) leading to an easy proof of transitivity of subtyping. This work sheds new insights on the theory of subtyping iso-recursive types, and the new double unfolding rule has important advantages over the original Amber rules for both implementations and metatheoretical studies involving recursive types. All results are mechanically formalized in the Coq theorem prover. As far as we know, this is the first comprehensive treatment of iso-recursive subtyping dealing with unrestricted recursive types in a theorem prover. | - |
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.subject | Formalization | - |
dc.subject | Iso-recursive types | - |
dc.subject | Subtyping | - |
dc.title | Revisiting iso-recursive 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/3428291 | - |
dc.identifier.scopus | eid_2-s2.0-85097587094 | - |
dc.identifier.hkuros | 323742 | - |
dc.identifier.hkuros | 327021 | - |
dc.identifier.volume | 4 | - |
dc.identifier.issue | OOPSLA | - |
dc.identifier.spage | article no. 223 | - |
dc.identifier.epage | article no. 223 | - |
dc.identifier.isi | WOS:000685203900100 | - |
dc.publisher.place | United States | - |