{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:40:58Z","timestamp":1780994458752,"version":"3.54.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Hong Kong Research Grant Council","award":["17210617,17258816"],"award-info":[{"award-number":["17210617,17258816"]}]},{"DOI":"10.13039\/501100003130","name":"Research Foundation Flanders","doi-asserted-by":"crossref","award":["G0D1419N"],"award-info":[{"award-number":["G0D1419N"]}],"id":[{"id":"10.13039\/501100003130","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>Modern 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.<\/jats:p>\n          <jats:p>\n            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\n            <jats:italic>manually<\/jats:italic>\n            proven\n            <jats:italic>sound<\/jats:italic>\n            ,\n            <jats:italic>complete<\/jats:italic>\n            and\n            <jats:italic>decidable<\/jats:italic>\n            . We present a mechanical formalization in the Abella theorem prover of DK\u2019s declarative type system with a novel algorithmic system. We have a few reasons to use a new algorithm. Firstly, our new algorithm employs\n            <jats:italic>worklist judgments<\/jats:italic>\n            , which precisely capture the scope of variables and simplify the formalization of scoping in a theorem prover. Secondly, while DK\u2019s 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.\n          <\/jats:p>","DOI":"10.1145\/3341716","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["A mechanical formalization of higher-ranked polymorphic type inference"],"prefix":"10.1145","volume":"3","author":[{"given":"Jinxu","family":"Zhao","sequence":"first","affiliation":[{"name":"University of Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bruno C. d. S.","family":"Oliveira","sequence":"additional","affiliation":[{"name":"University of Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tom","family":"Schrijvers","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"POPLMark Reloaded: Mechanizing Proofs by Logical Relations. Submitted to the Journal of functional programming","author":"Abel Andreas","year":"2018","unstructured":"Andreas Abel , Guillaume Allais , Aliya Hameer , Brigitte Pientka , Alberto Momigliano , Steven Sch\u00e4fer , and Kathrin Stark . 2018. POPLMark Reloaded: Mechanizing Proofs by Logical Relations. Submitted to the Journal of functional programming ( 2018 ). Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Sch\u00e4fer, and Kathrin Stark. 2018. POPLMark Reloaded: Mechanizing Proofs by Logical Relations. Submitted to the Journal of functional programming (2018)."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/2021953.2021960"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_5"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_12"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_2_2_8_1","unstructured":"Paul Chiusano and Runar Bjarnason. 2015. Unison. http:\/\/unisonweb.org  Paul Chiusano and Runar Bjarnason. 2015. Unison. http:\/\/unisonweb.org"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_2_11_1","volume-title":"Proving ML type soundness within Coq. Theorem Proving in Higher Order Logics","author":"Dubois Catherine","year":"2000","unstructured":"Catherine Dubois . 2000. Proving ML type soundness within Coq. Theorem Proving in Higher Order Logics ( 2000 ), 126\u2013144. Catherine Dubois. 2000. Proving ML type soundness within Coq. Theorem Proving in Higher Order Logics (2000), 126\u2013144."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006285817788"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290322"},{"key":"e_1_2_2_15_1","unstructured":"Phil Freeman. 2017. PureScript. http:\/\/www.purescript.org\/  Phil Freeman. 2017. PureScript. http:\/\/www.purescript.org\/"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_13"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000066"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863597.1863608"},{"key":"e_1_2_2_19_1","first-page":"29","article-title":"The principal type-scheme of an object in combinatory logic","volume":"146","author":"Hindley Roger","year":"1969","unstructured":"Roger Hindley . 1969 . The principal type-scheme of an object in combinatory logic . Transactions of the american mathematical society 146 (1969), 29 \u2013 60 . Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Transactions of the american mathematical society 146 (1969), 29\u201360.","journal-title":"Transactions of the american mathematical society"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103691"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944709"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411245"},{"key":"e_1_2_2_23_1","unstructured":"Xavier Leroy et al. 2012. The CompCert verified compiler. Documentation and user\u2019s manual. INRIA Paris-Rocquencourt (2012).  Xavier Leroy et al. 2012. The CompCert verified compiler. Documentation and user\u2019s manual. INRIA Paris-Rocquencourt (2012)."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"key":"e_1_2_2_25_1","volume-title":"Abstract Syntax for Variable Binders: An Overview. In CL 2000: Computational Logic (Lecture Notes in Artificial Intelligence).","author":"Miller Dale","year":"2000","unstructured":"Dale Miller . 2000 . Abstract Syntax for Variable Binders: An Overview. In CL 2000: Computational Logic (Lecture Notes in Artificial Intelligence). Dale Miller. 2000. Abstract Syntax for Variable Binders: An Overview. In CL 2000: Computational Logic (Lecture Notes in Artificial Intelligence)."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006277616879"},{"key":"e_1_2_2_28_1","volume-title":"a proof assistant for higher-order logic","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence C Paulson , and Markus Wenzel . 2002. Isabelle\/HOL : a proof assistant for higher-order logic . Vol. 2283 . Springer Science & amp; Business Media. Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. Vol. 2283. Springer Science &amp; Business Media."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237729"},{"key":"e_1_2_2_30_1","unstructured":"Simon Peyton Jones and Mark Shields. 2004. Lexically-scoped type variables. (2004). http:\/\/research.microsoft.com\/enus\/um\/people\/simonpj\/papers\/scoped- tyvars\/ Draft.  Simon Peyton Jones and Mark Shields. 2004. Lexically-scoped type variables. (2004). http:\/\/research.microsoft.com\/enus\/um\/people\/simonpj\/papers\/scoped- tyvars\/ Draft."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_2_2_32_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pottier Fran\u00e7ois","unstructured":"Fran\u00e7ois Pottier and Didier R\u00e9my . 2005. Advanced Topics in Types and Programming Languages . The MIT Press , Chapter The Essence of ML Type Inference, 387\u2013489. Fran\u00e7ois Pottier and Didier R\u00e9my. 2005. Advanced Topics in Types and Programming Languages. The MIT Press, Chapter The Essence of ML Type Inference, 387\u2013489."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1577824.1577832"},{"key":"e_1_2_2_34_1","volume-title":"Abstraction and Parametric Polymorphism. Information Processing","author":"Reynolds John C","year":"1983","unstructured":"John C Reynolds . 1983. Types , Abstraction and Parametric Polymorphism. Information Processing ( 1983 ), 513\u2013523. John C Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. Information Processing (1983), 513\u2013523."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192389"},{"key":"e_1_2_2_36_1","unstructured":"The Coq development team. 2017. The Coq proof assistant. https:\/\/coq.inria.fr\/  The Coq development team. 2017. The Coq proof assistant. https:\/\/coq.inria.fr\/"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788837"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"e_1_2_2_39_1","volume-title":"Nominal verification of algorithm W. From Semantics to Computer Science. Essays in Honour of Gilles Kahn","author":"Urban Christian","year":"2008","unstructured":"Christian Urban and Tobias Nipkow . 2008. Nominal verification of algorithm W. From Semantics to Computer Science. Essays in Honour of Gilles Kahn ( 2008 ), 363\u2013382. Christian Urban and Tobias Nipkow. 2008. Nominal verification of algorithm W. From Semantics to Computer Science. Essays in Honour of Gilles Kahn (2008), 363\u2013382."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411246"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00047-5"},{"key":"e_1_2_2_42_1","volume-title":"d. S. Oliveira","author":"Xie Ningning","year":"2018","unstructured":"Ningning Xie and Bruno C . d. S. Oliveira . 2018 . Let Arguments Go First. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing , Cham, 272\u2013299. Ningning Xie and Bruno C. d. S. Oliveira. 2018. Let Arguments Go First. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham, 272\u2013299."},{"key":"e_1_2_2_43_1","volume-title":"d. S. Oliveira, and Tom Schrijvers","author":"Zhao Jinxu","year":"2018","unstructured":"Jinxu Zhao , Bruno C. d. S. Oliveira, and Tom Schrijvers . 2018 . Formalization of a Polymorphic Subtyping Algorithm. In ITP (Lecture Notes in Computer Science), Vol. 10895 . Springer , 604\u2013622. Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018. Formalization of a Polymorphic Subtyping Algorithm. In ITP (Lecture Notes in Computer Science), Vol. 10895. Springer, 604\u2013622."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341716","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341716","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:24Z","timestamp":1750207404000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341716"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":43,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341716"],"URL":"https:\/\/doi.org\/10.1145\/3341716","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}