File Download
  Links for fulltext
     (May Require Subscription)
Supplementary

Article: A mechanical formalization of higher-ranked polymorphic type inference

TitleA mechanical formalization of higher-ranked polymorphic type inference
Authors
Issue Date2019
PublisherAssociation 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, 2019, v. 3 n. ICFP, p. article no. 112 How to Cite?
AbstractModern functional programming languages, such as Haskell or OCaml, use sophisticated forms of type inference. While an important topic in the Programming Languages research, there is little work on the mechanization of the metatheory of type inference in theorem provers. In particular we are unaware of any complete formalization of the type inference algorithms that are the backbone of modern functional languages. This paper presents the first full mechanical formalization of the metatheory for higher-ranked polymorphic type inference. The system that we formalize is the bidirectional type system by Dunfield and Krishnaswami (DK). The DK type system has two variants (a declarative and an algorithmic one) that have been manually proven sound, complete and decidable. We present a mechanical formalization in the Abella theorem prover of DK’s declarative type system with a novel algorithmic system. We have a few reasons to use a new algorithm. Firstly, our new algorithm employs worklist judgments, which precisely capture the scope of variables and simplify the formalization of scoping in a theorem prover. Secondly, while DK’s original formalization comes with very well-written manual proofs, there are several details missing and some incorrect proofs, which complicate the task of writing a mechanized proof. Despite the use of a different algorithm we prove the same results as DK, although with significantly different proofs and proof techniques. Since such type inference algorithms are quite subtle and have a complex metatheory, mechanical formalizations are an important advance in type-inference research.
Persistent Identifierhttp://hdl.handle.net/10722/301194
ISSN
2020 SCImago Journal Rankings: 0.362

 

DC FieldValueLanguage
dc.contributor.authorZHAO, J-
dc.contributor.authorDos Santos Oliveira, BCDS-
dc.contributor.authorSchrijvers, T-
dc.date.accessioned2021-07-27T08:07:31Z-
dc.date.available2021-07-27T08:07:31Z-
dc.date.issued2019-
dc.identifier.citationProceedings of the ACM on Programming Languages, 2019, v. 3 n. ICFP, p. article no. 112-
dc.identifier.issn2475-1421-
dc.identifier.urihttp://hdl.handle.net/10722/301194-
dc.description.abstractModern functional programming languages, such as Haskell or OCaml, use sophisticated forms of type inference. While an important topic in the Programming Languages research, there is little work on the mechanization of the metatheory of type inference in theorem provers. In particular we are unaware of any complete formalization of the type inference algorithms that are the backbone of modern functional languages. This paper presents the first full mechanical formalization of the metatheory for higher-ranked polymorphic type inference. The system that we formalize is the bidirectional type system by Dunfield and Krishnaswami (DK). The DK type system has two variants (a declarative and an algorithmic one) that have been manually proven sound, complete and decidable. We present a mechanical formalization in the Abella theorem prover of DK’s declarative type system with a novel algorithmic system. We have a few reasons to use a new algorithm. Firstly, our new algorithm employs worklist judgments, which precisely capture the scope of variables and simplify the formalization of scoping in a theorem prover. Secondly, while DK’s original formalization comes with very well-written manual proofs, there are several details missing and some incorrect proofs, which complicate the task of writing a mechanized proof. Despite the use of a different algorithm we prove the same results as DK, although with significantly different proofs and proof techniques. Since such type inference algorithms are quite subtle and have a complex metatheory, mechanical formalizations are an important advance in type-inference research.-
dc.languageeng-
dc.publisherAssociation for Computing Machinery: Open Access Journals. The Journal's web site is located at https://dl.acm.org/journal/pacmpl-
dc.relation.ispartofProceedings of the ACM on Programming Languages-
dc.rightsThis work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.-
dc.titleA mechanical formalization of higher-ranked polymorphic type inference-
dc.typeArticle-
dc.identifier.emailDos Santos Oliveira, BCDS: bruno@cs.hku.hk-
dc.identifier.authorityDos Santos Oliveira, BCDS=rp01786-
dc.description.naturepublished_or_final_version-
dc.identifier.doi10.1145/3341716-
dc.identifier.hkuros323731-
dc.identifier.volume3-
dc.identifier.issueICFP-
dc.identifier.spagearticle no. 112-
dc.identifier.epagearticle no. 112-
dc.publisher.placeUnited States-

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats