File Download
There are no files associated with this item.
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.1007/978-3-319-94821-8_36
- Scopus: eid_2-s2.0-85049883804
- WOS: WOS:000490904100036
Supplementary
- Citations:
- Appears in Collections:
Conference Paper: Formalization of a Polymorphic Subtyping Algorithm
Title | Formalization of a Polymorphic Subtyping Algorithm |
---|---|
Authors | |
Keywords | Subtyping Algorithm Higher-order Polymorphism Worklist Modern Functional Programming Languages Type-inference Algorithm |
Issue Date | 2018 |
Publisher | Springer. |
Citation | Proceedings of the 9th International Conference on Interactive Theorem Proving (ITP 2018), Oxford, UK, 9-12 July 2018, p. 604-622 How to Cite? |
Abstract | Modern functional programming languages such as Haskell support sophisticated forms of type-inference, even in the presence of higher-order polymorphism. Central to such advanced forms of type-inference is an algorithm for polymorphic subtyping. This paper formalizes an algorithmic specification for polymorphic subtyping in the Abella theorem prover. The algorithmic specification is shown to be decidable, and sound and complete with respect to Odersky and Läufer’s well-known declarative formulation of polymorphic subtyping.
While the meta-theoretical results are not new, as far as we know our work is the first to mechanically formalize them. Moreover, our algorithm differs from those currently in the literature by using a novel approach based on worklist judgements. Worklist judgements simplify the propagation of information required by the unification process during subtyping. Furthermore they enable a simple formulation of the meta-theoretical properties, which can be easily encoded in theorem provers. |
Description | Held as Part of the Federated Logic Conference, FloC 2018 |
Persistent Identifier | http://hdl.handle.net/10722/301425 |
ISBN | |
ISI Accession Number ID | |
Series/Report no. | Lecture Notes in Computer Science (LNCS) ; v. 10895 |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Zhao, J | - |
dc.contributor.author | Dos Santos Oliveira, BC | - |
dc.contributor.author | Schrijvers, T | - |
dc.date.accessioned | 2021-07-27T08:10:53Z | - |
dc.date.available | 2021-07-27T08:10:53Z | - |
dc.date.issued | 2018 | - |
dc.identifier.citation | Proceedings of the 9th International Conference on Interactive Theorem Proving (ITP 2018), Oxford, UK, 9-12 July 2018, p. 604-622 | - |
dc.identifier.isbn | 9783319948201 | - |
dc.identifier.uri | http://hdl.handle.net/10722/301425 | - |
dc.description | Held as Part of the Federated Logic Conference, FloC 2018 | - |
dc.description.abstract | Modern functional programming languages such as Haskell support sophisticated forms of type-inference, even in the presence of higher-order polymorphism. Central to such advanced forms of type-inference is an algorithm for polymorphic subtyping. This paper formalizes an algorithmic specification for polymorphic subtyping in the Abella theorem prover. The algorithmic specification is shown to be decidable, and sound and complete with respect to Odersky and Läufer’s well-known declarative formulation of polymorphic subtyping. While the meta-theoretical results are not new, as far as we know our work is the first to mechanically formalize them. Moreover, our algorithm differs from those currently in the literature by using a novel approach based on worklist judgements. Worklist judgements simplify the propagation of information required by the unification process during subtyping. Furthermore they enable a simple formulation of the meta-theoretical properties, which can be easily encoded in theorem provers. | - |
dc.language | eng | - |
dc.publisher | Springer. | - |
dc.relation.ispartof | Proceedings of the 9th International Conference on Interactive Theorem Proving (ITP 2018) | - |
dc.relation.ispartofseries | Lecture Notes in Computer Science (LNCS) ; v. 10895 | - |
dc.subject | Subtyping Algorithm | - |
dc.subject | Higher-order Polymorphism | - |
dc.subject | Worklist | - |
dc.subject | Modern Functional Programming Languages | - |
dc.subject | Type-inference Algorithm | - |
dc.title | Formalization of a Polymorphic Subtyping Algorithm | - |
dc.type | Conference_Paper | - |
dc.identifier.email | Dos Santos Oliveira, BC: bruno@cs.hku.hk | - |
dc.identifier.authority | Dos Santos Oliveira, BC=rp01786 | - |
dc.description.nature | link_to_subscribed_fulltext | - |
dc.identifier.doi | 10.1007/978-3-319-94821-8_36 | - |
dc.identifier.scopus | eid_2-s2.0-85049883804 | - |
dc.identifier.hkuros | 323722 | - |
dc.identifier.spage | 604 | - |
dc.identifier.epage | 622 | - |
dc.identifier.isi | WOS:000490904100036 | - |
dc.publisher.place | Cham | - |