{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T22:21:03Z","timestamp":1770243663459,"version":"3.49.0"},"reference-count":80,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100019180","name":"HORIZON EUROPE European Research Council","doi-asserted-by":"publisher","award":["101040088"],"award-info":[{"award-number":["101040088"]}],"id":[{"id":"10.13039\/100019180","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>Type inference is essential for statically-typed languages such as OCaml and Haskell. It can be decomposed into two (possibly interleaved) phases: a generator converts programs to constraints; a solver decides whether a constraint is satisfiable. Elaboration, the task of decorating a program with explicit type annotations, can also be structured in this way. Unfortunately, most machine-checked implementations of type inference do not follow this phase-separated, constraint-based approach. Those that do are rarely executable, lack effectful abstractions, and do not include elaboration.<\/jats:p>\n                  <jats:p>\n                    To close the gap between common practice in real-world implementations and mechanizations inside proof assistants, we propose an approach that enables modular reasoning about monadic constraint generation in the presence of elaboration. Our approach includes a domain-specific base logic for reasoning about metavariables and a program logic that allows us to reason abstractly about the meaning of constraints. To evaluate it, we report on a machine-checked implementation of our techniques inside the\n                    <jats:sc>Coq<\/jats:sc>\n                    proof assistant. As a case study, we verify both soundness and completeness for three elaborating type inferencers for the simply typed\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>\u03bb<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    -calculus with Booleans. Our results are the first demonstration that type inference algorithms can be verified in the same form as they are implemented in practice: in an imperative style, modularly decomposed into constraint generation and solving, and delivering elaborated terms to the remainder of the compiler chain.\n                  <\/jats:p>","DOI":"10.1145\/3689786","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"2125-2155","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Type Inference Logics"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2148-5193","authenticated-orcid":false,"given":"Denis","family":"Carnier","sequence":"first","affiliation":[{"name":"KU Leuven, Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4069-1235","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6411-438X","authenticated-orcid":false,"given":"Steven","family":"Keuchel","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Brussel, Brussels, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/3-540-36576-1_2","volume-title":"Foundations of Software Science and Computation Structures (FoSSaCS\u201903)","author":"Abbott Michael","year":"2003","unstructured":"Michael Abbott, Thorsten Altenkirch, and Neil Ghani. 2003. Categories of Containers. In Foundations of Software Science and Computation Structures (FoSSaCS\u201903), Andrew D. Gordon (Ed.). Springer, 23\u201338."},{"key":"e_1_3_1_3_1","doi-asserted-by":"crossref","unstructured":"Danel Ahman Catalin Hritcu Kenji Maillard Guido Mart\u00ednez Gordon D. Plotkin Jonathan Protzenko Aseem Rastogi and Nikhil Swamy. 2017. Dijkstra monads for free. In Principles of Programming Languages (POPL). 515\u2013529. https:\/\/arxiv.org\/abs\/1608.06499.","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_3_1_4_1","first-page":"109","volume-title":"Functional and Logic Programming (Lecture Notes in Computer Science, Vol. 9613)","author":"Ahn Ki Yung","year":"2016","unstructured":"Ki Yung Ahn and Andrea Vezzosi. 2016. Executable Relational Specifications of Polymorphic Type Systems Using Prolog. In Functional and Logic Programming (Lecture Notes in Computer Science, Vol. 9613). Springer, 109\u2013125. https:\/\/doi.org\/10.1007\/978-3-319-29604-3_8 10.1007\/978-3-319-29604-3_8"},{"key":"e_1_3_1_5_1","article-title":"A type and scope safe universe of syntaxes with binding: their semantics and proofs","volume":"2","author":"Allais Guillaume","year":"2018","unstructured":"Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. 2018. A type and scope safe universe of syntaxes with binding: their semantics and proofs. Proc. ACM Program. Lang. 2, ICFP, Article 90 (jul 2018), 30 pages. https:\/\/doi.org\/10.1145\/3236785 10.1145\/3236785","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_6_1","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1007\/3-540-48168-0_32","volume-title":"Computer Science Logic","author":"Altenkirch Thorsten","year":"1999","unstructured":"Thorsten Altenkirch and Bernhard Reus. 1999. Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In Computer Science Logic, J\u00f6rg Flum and Mario Rodriguez-Artalejo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 453\u2013468."},{"issue":"1","key":"e_1_3_1_7_1","first-page":"83","article-title":"Ten years of Hoare\u2019s logic: A survey-part II: Nondeterminism","volume":"28","author":"Apt Krzysztof R.","year":"1983","unstructured":"Krzysztof R. Apt. 1983. Ten years of Hoare\u2019s logic: A survey-part II: Nondeterminism. Theoretical Computer Science 28, 1 (1983), 83\u2013109. https:\/\/doi.org\/10.1016\/0304-3975(83)90066-X 10.1016\/0304-3975(83)90066-X","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_1_8_1","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-3-642-14052-5_8","volume-title":"Interactive Theorem Proving","author":"Armand Micha\u00ebl","year":"2010","unstructured":"Micha\u00ebl Armand, Benjamin Gr\u00e9goire, Arnaud Spiwack, and Laurent Th\u00e9ry. 2010. Extending Coq with Imperative Features and Its Application to SAT Verification. In Interactive Theorem Proving, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 83\u201398."},{"key":"e_1_3_1_9_1","unstructured":"Kenichi Asai and Kyoko Kadowaki. 2017. A Type Theoretic Specification of Type Inference. (2017). http:\/\/pllab.is.ocha.ac.jp\/~asai\/papers\/paper2017.pdf Unpublished."},{"key":"e_1_3_1_10_1","volume-title":"Handbook of Automated Reasoning","author":"Baader Franz","year":"2001","unstructured":"Franz Baader, Wayne Snyder, Paliath Narendran, Manfred Schmidt-Schauss, and Klaus Schulz. 2001. Chapter 8 - Unification Theory. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). North-Holland, Amsterdam. https:\/\/doi.org\/10.1016\/B978-044450813-3\/50010-2 10.1016\/B978-044450813-3\/50010-2"},{"key":"e_1_3_1_11_1","article-title":"Intrinsically-Typed Definitional Interpreters for Imperative Languages","volume":"2","author":"Poulsen Casper Bach","year":"2017","unstructured":"Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser. 2017. Intrinsically-Typed Definitional Interpreters for Imperative Languages. Proc. ACM Program. Lang. 2, POPL, Article 16 (dec 2017), 34 pages. https:\/\/doi.org\/10.1145\/3158104 10.1145\/3158104","journal-title":"Proc. ACM Program. Lang."},{"issue":"4","key":"e_1_3_1_12_1","first-page":"265","article-title":"Universes for generic programs and proofs in dependent type theory","volume":"10","author":"Benke Marcin","year":"2003","unstructured":"Marcin Benke, Peter Dybjer, and Patrik Jansson. 2003. Universes for generic programs and proofs in dependent type theory. Nordic J. of Computing 10, 4 (Dec. 2003), 265\u2013289. http:\/\/dl.acm.org\/citation.cfm?id=985799.985801","journal-title":"Nordic J. of Computing"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_3_1_14_1","volume-title":"14th International Conference on Interactive Theorem Proving, ITP 2023, fuly 31-August 4, 2023, Biatystok, Poland (LIPIcs)","author":"Bosman Roger","year":"2023","unstructured":"Roger Bosman, Georgios Karachalias, and Tom Schrijvers. 2023. No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. In 14th International Conference on Interactive Theorem Proving, ITP 2023, fuly 31-August 4, 2023, Biatystok, Poland (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik. https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2023\/18383\/"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90019-0"},{"key":"e_1_3_1_16_1","unstructured":"Denis Carnier Fran\u00e7ois Pottier and Steven Keuchel. 2024a. Type Inference Logics - Artifact. https:\/\/doi.org\/10.5281\/zenodo.13625874 10.5281\/zenodo.13625874"},{"key":"e_1_3_1_17_1","doi-asserted-by":"crossref","unstructured":"Denis Carnier Fran\u00e7ois Pottier and Steven Keuchel. 2024b. Type Inference Logics - Software Repository. https:\/\/github.com\/decrn\/tilogics","DOI":"10.1145\/3689786"},{"key":"e_1_3_1_18_1","first-page":"93","article-title":"Sikkel: Multimode Simply Type Theory as an Agda Library","author":"Ceulemans Joris","year":"2022","unstructured":"Joris Ceulemans, Andreas Nuys, and Dominique Devriese. 2022. Sikkel: Multimode Simply Type Theory as an Agda Library. In Workshop on Mathematically Structured Functional Programming (MSFP). 93\u2013112. https:\/\/doi.org\/10.4204\/EPTCS.360.5 10.4204\/EPTCS.360.5","journal-title":"Workshop on Mathematically Structured Functional Programming (MSFP)"},{"key":"e_1_3_1_19_1","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"Cock David","year":"2008","unstructured":"David Cock, Gerwin Klein, and Thomas Sewell. 2008. Secure Microkernels, State Monads and Scalable Refinement. In Theorem Proving in Higher Order Logics, Otmane Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 167\u2013182."},{"key":"e_1_3_1_20_1","volume-title":"Combinatory Logic","author":"Curry Haskell B.","year":"1958","unstructured":"Haskell B. Curry and Robert M. Feys. 1958. Combinatory Logic. Vol. 1. North-Holland Publishing Company, Amsterdam."},{"key":"e_1_3_1_21_1","volume-title":"Type Assignment in Programming Languages","author":"Damas Luis","year":"1984","unstructured":"Luis Damas. 1984. Type Assignment in Programming Languages. Ph. D. Dissertation. University of Edinburgh. http:\/\/hdl.handle.net\/1842\/13555"},{"key":"e_1_3_1_22_1","first-page":"207","article-title":"Principal type-schemes for functional programs","author":"Damas Luis","year":"1982","unstructured":"Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In Principles of Programming Languages (POPL). 207\u2013212. http:\/\/doi.acm.org\/10.1145\/582153.582176 10.1145\/582153.582176","journal-title":"Principles of Programming Languages (POPL)."},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_3_1_24_1","first-page":"3","article-title":"Certification of a Type Inference Tool for ML: Damas-Milner within Coq","volume":"23","author":"Dubois Catherine","year":"1999","unstructured":"Catherine Dubois and Val\u00e9rie M\u00e9nissier-Morain. 1999. Certification of a Type Inference Tool for ML: Damas-Milner within Coq. Journal of Automated Reasoning 23, 3\u20134 (Nov. 1999), 319-346. http:\/\/www.ensiie.fr\/~dubois\/jar_final.pdf","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_3_1_25_1","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/1596627.1596631","volume-title":"Proceedings of the 2009 ACM SIGPLAN Workshop on ML (Edinburgh, Scotland) (ML \u201809)","author":"Dunfield Jana","year":"2009","unstructured":"Jana Dunfield. 2009. Greedy Bidirectional Polymorphism. In Proceedings of the 2009 ACM SIGPLAN Workshop on ML (Edinburgh, Scotland) (ML \u201809). Association for Computing Machinery, New York, NY, USA, 15\u201326. https:\/\/doi.org\/10.1145\/1596627.1596631 10.1145\/1596627.1596631"},{"key":"e_1_3_1_26_1","first-page":"429","article-title":"Complete and easy bidirectional typechecking for higher-rank polymorphism","author":"Dunfield Jana","year":"2013","unstructured":"Jana Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and easy bidirectional typechecking for higher-rank polymorphism. In International Conference on Functional Programming (ICFP). 429\u2013442. https:\/\/doi.org\/10.1145\/2500365.2500582 10.1145\/2500365.2500582","journal-title":"International Conference on Functional Programming (ICFP)."},{"key":"e_1_3_1_27_1","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/978-3-540-24849-1_14","volume-title":"Types for Proofs and Programs (LNCS, Vol. 3085)","author":"Gambino Nicola","year":"2004","unstructured":"Nicola Gambino and Martin Hyland. 2004. Wellfounded Trees and Dependent Polynomial Functors. In Types for Proofs and Programs (LNCS, Vol. 3085), Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer, 210\u2013225."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000066"},{"key":"e_1_3_1_29_1","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/1863597.1863608","article-title":"Type inference in context","author":"Gundry Adam","year":"2010","unstructured":"Adam Gundry, Conor McBride, and James McKinna. 2010. Type inference in context. In Workshop on Mathematically Structured Functional Programming (MSFP). 43\u201354. https:\/\/adam.gundry.co.uk\/pub\/type-inference-in-context\/","journal-title":"Workshop on Mathematically Structured Functional Programming (MSFP)"},{"key":"e_1_3_1_30_1","volume-title":"Symposium on Programs as Data Objects (Lecture Notes in Computer Science, Vol. 2053)","author":"Gustavsson J\u00f6rgen","year":"2001","unstructured":"J\u00f6rgen Gustavsson and Josef Svenningsson. 2001. Constraint Abstractions. In Symposium on Programs as Data Objects (Lecture Notes in Computer Science, Vol. 2053). Springer. http:\/\/www.cse.chalmers.se\/~josefs\/publications\/ca.pdf"},{"key":"e_1_3_1_31_1","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/3-540-44622-2_21","volume-title":"Computer Science Logic","author":"Hancock Peter","year":"2000","unstructured":"Peter Hancock and Anton Setzer. 2000. Interactive Programs in Dependent Type Theory. In Computer Science Logic, Peter G. Clote and Helmut Schwichtenberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 317\u2013331."},{"key":"e_1_3_1_32_1","first-page":"3","volume-title":"Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003","author":"Heeren Bastiaan","year":"2003","unstructured":"Bastiaan Heeren, Jurriaan Hage, and S. Doaitse Swierstra. 2003. Scripting the type inference process. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, Colin Runciman and Olin Shivers (Eds.). ACM, 3\u201313. https:\/\/doi.org\/10.1145\/944705.944707 10.1145\/944705.944707"},{"key":"e_1_3_1_33_1","volume-title":"Generic programs and proofs","author":"Hinze Ralf","year":"2000","unstructured":"Ralf Hinze. 2000. Generic programs and proofs. Habilitation thesis. Universit\u00e4t Bonn."},{"key":"e_1_3_1_34_1","first-page":"40","volume-title":"Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming, MSFP\u2019 12 (Electronic Proceedings in Theoretical Computer Science, Vol. 76)","author":"Jaskelioff Mauro","year":"2012","unstructured":"Mauro Jaskelioff and Ondrej Rypacek. 2012. An Investigation of the Laws of Traversals. In Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming, MSFP\u2019 12 (Electronic Proceedings in Theoretical Computer Science, Vol. 76), James Chapman and Paul Blain Levy (Eds.). Open Publishing Association, 40\u201349. https:\/\/doi.org\/10.4204\/EPTCS.76.5 10.4204\/EPTCS.76.5"},{"key":"e_1_3_1_35_1","first-page":"257","volume-title":"Computational Logic. Essays in honor of Alan Robinson","author":"Jouannaud Jean-Pierre","year":"1991","unstructured":"Jean-Pierre Jouannaud and Claude Kirchner. 1991. Solving equations in abstract algebras: a rule-based survey of unification. In Computational Logic. Essays in honor of Alan Robinson, Jean-Louis Lassez and Gordon Plotkin (Eds.). MIT Press, Chapter 8, 257\u2013321."},{"key":"e_1_3_1_36_1","first-page":"256","article-title":"Higher-order ghost state","author":"Jung Ralf","year":"2016","unstructured":"Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In International Conference on Functional Programming (ICFP). 256\u2013269. http:\/\/iris-project.org\/pdfs\/2016-icfp-iris2-final.pdf","journal-title":"International Conference on Functional Programming (ICFP)"},{"key":"e_1_3_1_37_1","volume-title":"Verified compilation of a purely functional language to a realistic machine semantics","author":"Kanabar Hrutvik","year":"2023","unstructured":"Hrutvik Kanabar. 2023. Verified compilation of a purely functional language to a realistic machine semantics. Ph. D. Dissertation. School of Computing, University of Kent. https:\/\/hrutvik.co.uk\/assets\/pdf\/Hrutvik_Kanabar_thesis.pdf"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591259"},{"key":"e_1_3_1_39_1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/1863597.1863601","volume-title":"Proceedings of the Third ACM SIGPLAN Workshop on Mathematically Structured Functional Programming (Baltimore, Maryland, USA) (MSFP \u201810)","author":"Keller Chantal","year":"2010","unstructured":"Chantal Keller and Thorsten Altenkirch. 2010. Hereditary Substitutions for Simple Types, Formalized. In Proceedings of the Third ACM SIGPLAN Workshop on Mathematically Structured Functional Programming (Baltimore, Maryland, USA) (MSFP \u201810). Association for Computing Machinery, New York, NY, USA, 3\u201310. https:\/\/doi.org\/10.1145\/1863597.1863601 10.1145\/1863597.1863601"},{"key":"e_1_3_1_40_1","article-title":"Verified Symbolic Execution with Kripke Specification Monads (and No Meta-Programming)","volume":"6","author":"Keuchel Steven","year":"2022","unstructured":"Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, and Dominique Devriese. 2022. Verified Symbolic Execution with Kripke Specification Monads (and No Meta-Programming). Proc. ACM Program. Lang. 6, ICFP, Article 97 (aug 2022), 31 pages. https:\/\/doi.org\/10.1145\/3547628 10.1145\/3547628","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364394.2364403"},{"key":"e_1_3_1_42_1","first-page":"77:1","article-title":"MoSeL: a general, extensible modal framework for interactive proofs in separation logic","volume":"2","author":"Krebbers Robbert","year":"2018","unstructured":"Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Chargu\u00e9raud, and Derek Dreyer. 2018. MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proceedings of the ACM on Programming Languages 2, ICFP (2018), 77:1\u201377:30. https:\/\/doi.org\/10.1145\/3236772 10.1145\/3236772","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_3_1_43_1","doi-asserted-by":"crossref","unstructured":"Robert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In Principles of Programming Languages (POPL). http:\/\/cs.au.dk\/~birke\/papers\/ipm-conf.pdf","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_44_1","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/978-3-642-14052-5_6","volume-title":"Interactive Theorem Proving","author":"Kumar Ramana","year":"2010","unstructured":"Ramana Kumar and Michael Norrish. 2010. (Nominal) Unification by Recursive Descent with Triangular Substitutions. In Interactive Theorem Proving, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 51\u201366."},{"key":"e_1_3_1_45_1","first-page":"104:1","article-title":"Dijkstra monads for all","volume":"3","author":"Maillard Kenji","year":"2019","unstructured":"Kenji Maillard, Danel Ahman, Robert Atkey, Guido Mart\u00ednez, Catalin Hritcu, Exequiel Rivas, and \u00e9ric Tanter. 2019. Dijkstra monads for all. Proceedings of the ACM on Programming Languages 3, ICFP (2019), 104:1\u2013104:29. https:\/\/doi.org\/10.1145\/3341708 10.1145\/3341708","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_3_1_46_1","unstructured":"Olivier Martinot and Gabriel Scherer. 2020. Quantified Applicatives: API design for type-inference constraints. Presented at the ML Family Workshop."},{"key":"e_1_3_1_47_1","volume-title":"Dependently Typed Functional Programs and their Proofs","author":"McBride Conor","year":"2000","unstructured":"Conor McBride. 2000. Dependently Typed Functional Programs and their Proofs. Ph. D. Dissertation. University of Edinburgh."},{"key":"e_1_3_1_48_1","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-45842-5_13","volume-title":"Types for Proofs and Programs","author":"McBride Conor","year":"2002","unstructured":"Conor McBride. 2002. Elimination with a Motive. In Types for Proofs and Programs, Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack, and Robert Pollack (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 197\u2013216."},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004957"},{"key":"e_1_3_1_50_1","unstructured":"Conor McBride. 2003b. First-Order Unification by Structural Recursion - Correctness Proof. http:\/\/www.strictlypositive.org\/foubsr-website\/ Accessed: 2023-10-26."},{"key":"e_1_3_1_51_1","unstructured":"Conor McBride. 2011. Functional pearl: Kleisli arrows of outrageous fortune. (2011). Available at https:\/\/personal.cis.strath.ac.uk\/conor.mcbride\/Kleisli.pdf."},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_1_54_1","doi-asserted-by":"crossref","unstructured":"E. Moggi G. Bell\u00e8 and C.B. Jay. 1999. Monads Shapely Functors and Traversals. Electronic Notes in Theoretical Computer Science 29 (1999) 187\u2013208. https:\/\/doi.org\/10.1016\/S1571-0661(05)80316-0 10.1016\/S1571-0661(05)80316-0 CTCS \u201899 Conference on Category Theory and Computer Science.","DOI":"10.1016\/S1571-0661(05)80316-0"},{"issue":"3","key":"e_1_3_1_55_1","article-title":"Contextual modal type theory","volume":"9","author":"Nanevski Aleksandar","year":"2008","unstructured":"Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory. ACM Trans. Comput. Logic 9, 3, Article 23 (jun 2008), 49 pages. https:\/\/doi.org\/10.1145\/1352582.1352591 10.1145\/1352582.1352591","journal-title":"ACM Trans. Comput. Logic"},{"key":"e_1_3_1_56_1","doi-asserted-by":"crossref","unstructured":"Wolfgang Naraschewski and Tobias Nipkow. 1999. Type Inference Verified: Algorithm W in Isabelle\/HOL. Journal of Automated Reasoning 23 (1999) 299\u2013318. http:\/\/www4.informatik.tu-muenchen.de\/~nipkow\/pubs\/W.ps.gz","DOI":"10.1023\/A:1006277616879"},{"key":"e_1_3_1_57_1","first-page":"331","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs) (Lecture Notes in Computer Science, Vol. 1125)","author":"Nazareth Dieter","year":"1996","unstructured":"Dieter Nazareth and Tobias Nipkow. 1996. Formal Verification of Algorithm W: The Monomorphic Case. In Theorem Proving in Higher Order Logics (TPHOLs) (Lecture Notes in Computer Science, Vol. 1125). Springer, 331\u2013345. https:\/\/www21.in.tum.de\/~nipkow\/pubs\/tphol96.html"},{"key":"e_1_3_1_58_1","first-page":"29:1","volume-title":"Interactive Theorem Proving (ITP) (Leibniz International Proceedings in Informatics, Vol. 193)","author":"Nigron Pierre","year":"2021","unstructured":"Pierre Nigron and Pierre-\u00e9variste Dagand. 2021. Reaching for the Star: Tale of a Monad in Coq. In Interactive Theorem Proving (ITP) (Leibniz International Proceedings in Informatics, Vol. 193). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 29:1\u201329:19. https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.29 10.4230\/LIPIcs.ITP.2021.29"},{"key":"e_1_3_1_59_1","first-page":"54","article-title":"Putting Type Annotations To Work","author":"Odersky Martin","year":"1996","unstructured":"Martin Odersky and Konstantin L\u00e4ufer. 1996. Putting Type Annotations To Work. In Principles of Programming Languages (POPL). 54\u201367. http:\/\/lamp.epfl.ch\/~odersky\/papers\/popl96.ps.gz","journal-title":"Principles of Programming Languages (POPL)."},{"issue":"1","key":"e_1_3_1_60_1","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1<35::AID-TAPO4>3.0.CO;2-4","article-title":"Type Inference with Constrained Types","volume":"5","author":"Odersky Martin","year":"1999","unstructured":"Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999. Type Inference with Constrained Types. Theory and Practice of Object Systems 5, 1 (1999), 35\u201355. https:\/\/doi.org\/10.1002\/(SICI)1096-9942(199901\/03)5:1<35::AID-TAPO4>3.0.CO;2-4 10.1002\/(SICI)1096-9942(199901\/03)5:1<35::AID-TAPO4>3.0.CO;2-4","journal-title":"Theory and Practice of Object Systems"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_3_1_62_1","first-page":"199","article-title":"Higher-Order Abstract Syntax","author":"Pfenning Frank","year":"1988","unstructured":"Frank Pfenning and Conal Elliott. 1988. Higher-Order Abstract Syntax. In Programming Language Design and Implementation (PLDI). 199\u2013208. http:\/\/doi.acm.org\/10.1145\/53990.54010 10.1145\/53990.54010","journal-title":"Programming Language Design and Implementation (PLDI)."},{"key":"e_1_3_1_63_1","article-title":"Hindley-Milner elaboration in applicative style","author":"Pottier Fran\u00e7ois","year":"2014","unstructured":"Fran\u00e7ois Pottier. 2014. Hindley-Milner elaboration in applicative style. In International Conference on Functional Programming (ICFP). http:\/\/cambium.inria.fr\/~fpottier\/publis\/fpottier-elaboration.pdf","journal-title":"International Conference on Functional Programming (ICFP)"},{"key":"e_1_3_1_64_1","first-page":"389","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pottier Fran\u00e7ois","year":"2005","unstructured":"Fran\u00e7ois Pottier and Didier R\u00e9my. 2005. The Essence of ML Type Inference. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press, Chapter 10, 389\u2013489. http:\/\/cambium.inria.fr\/~fpottier\/publis\/emltifinal.pdf"},{"key":"e_1_3_1_65_1","first-page":"284","volume-title":"Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (New Orleans, LA, USA) (CPP 2020)","author":"Rouvoet Arjen","year":"2020","unstructured":"Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. 2020. Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (New Orleans, LA, USA) (CPP 2020). Association for Computing Machinery, New York, NY, USA, 284\u2013298. https:\/\/doi.org\/10.1145\/3372885.3373818 10.1145\/3372885.3373818"},{"key":"e_1_3_1_66_1","volume-title":"Correct by Construction Language Implementations","author":"Rouvoet A. J.","year":"2021","unstructured":"A. J. Rouvoet. 2021. Correct by Construction Language Implementations. Ph. D. Dissertation. Delft University of Technology. https:\/\/doi.org\/10.4233\/uuid:f0312839-3444-41ee-9313-b07b21b59c11 10.4233\/uuid:f0312839-3444-41ee-9313-b07b21b59c11"},{"key":"e_1_3_1_67_1","doi-asserted-by":"crossref","unstructured":"Rafael Castro G. Silva Cristiano D. Vasconcellos and Karina Girardi Roggia. 2020. Monadic W in Coq. In Brazilian Symposium on Programming Languages (SBLP). 25\u201332. https:\/\/doi.org\/10.1145\/3427081.3427085 10.1145\/3427081.3427085","DOI":"10.1145\/3427081.3427085"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434307"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2491978"},{"key":"e_1_3_1_70_1","first-page":"440","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs) (Lecture Notes in Computer Science, Vol. 5674)","author":"Swierstra Wouter","year":"2009","unstructured":"Wouter Swierstra. 2009. A Hoare Logic for the State Monad. In Theorem Proving in Higher Order Logics (TPHOLs) (Lecture Notes in Computer Science, Vol. 5674). Springer, 440\u2013451. https:\/\/webspace.science.uu.nl\/~swier004\/publications\/2009-tphols.pdf"},{"key":"e_1_3_1_71_1","first-page":"103:1","article-title":"A predicate transformer semantics for effects (functional pearl)","volume":"3","author":"Swierstra Wouter","year":"2019","unstructured":"Wouter Swierstra and Tim Baanen. 2019. A predicate transformer semantics for effects (functional pearl). Proceedings of the ACM on Programming Languages 3, ICFP (2019), 103:1\u2013103:26. https:\/\/doi.org\/10.1145\/3341707 10.1145\/3341707","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_3_1_72_1","doi-asserted-by":"crossref","unstructured":"Yong Kiam Tan Magnus O. Myreen Ramana Kumar Anthony C. J. Fox Scott Owens and Michael Norrish. 2019. The verified CakeML compiler backend. Journal of Functional Programming 29 (2019) e2. https:\/\/cakeml.org\/jfp19.pdf","DOI":"10.1017\/S0956796818000229"},{"key":"e_1_3_1_73_1","first-page":"7:1","article-title":"A verified type system for CakeML","author":"Tan Yong Kiam","year":"2015","unstructured":"Yong Kiam Tan, Scott Owens, and Ramana Kumar. 2015. A verified type system for CakeML. In Implementation of Functional Languages (IFL). 7:1\u20137:12. https:\/\/cakeml.org\/ifl15.pdf","journal-title":"Implementation of Functional Languages (IFL)"},{"key":"e_1_3_1_74_1","first-page":"106","article-title":"Automatic type inference via partial evaluation","author":"Tomb Aaron","year":"2005","unstructured":"Aaron Tomb and Cormac Flanagan. 2005. Automatic type inference via partial evaluation. In Principles and Practice of Declarative Programming (PPDP). 106\u2013116. http:\/\/alumni.soe.ucsc.edu\/~atomb\/tomb05inference.pdf","journal-title":"Principles and Practice of Declarative Programming (PPDP)"},{"key":"e_1_3_1_75_1","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1017\/CBO9780511770524.017","volume-title":"From Semantics to Computer Science: Essays in Honour of Gilles Kahn","author":"Urban Christian","year":"2009","unstructured":"Christian Urban and Tobias Nipkow. 2009. Nominal verification of algorithm W. In From Semantics to Computer Science: Essays in Honour of Gilles Kahn, Yves Bertot, G\u00e9rard Huet, Jean-Jacques L\u00e9vy, and Gordon Plotkin (Eds.). Cambridge University Press, 363\u2013382. https:\/\/www21.in.tum.de\/~nipkow\/pubs\/w.pdf"},{"issue":"2","key":"e_1_3_1_76_1","article-title":"Intrinsically-Typed Definitional Interpreters \u00e0 La Carte","volume":"6","author":"Rest Cas","year":"2022","unstructured":"Cas van der Rest, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser, and Peter Mosses. 2022. Intrinsically-Typed Definitional Interpreters \u00e0 La Carte. Proc. ACM Program. Lang. 6, OOPSLA2, Article 192 (oct 2022), 30 pages. https:\/\/doi.org\/10.1145\/3563355 10.1145\/3563355","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_77_1","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1007\/978-3-540-70594-9_20","volume-title":"Mathematics of Program Construction","author":"Voigtl\u00e4nder Janis","year":"2008","unstructured":"Janis Voigtl\u00e4nder. 2008. Asymptotic Improvement of Computations over Free Monads. In Mathematics of Program Construction, Philippe Audebaud and Christine Paulin-Mohring (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 388\u2013403."},{"key":"e_1_3_1_78_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_3_1_79_1","doi-asserted-by":"crossref","unstructured":"Mitchell Wand. 1987. A Simple Algorithm and Proof for Type Inference. Fundamenta Informatic\u00e6 10 (1987) 115\u2013122. http:\/\/web.cs.ucla.edu\/~palsberg\/course\/cs239\/reading\/wand87.pdf","DOI":"10.3233\/FI-1987-10202"},{"key":"e_1_3_1_80_1","doi-asserted-by":"crossref","first-page":"604","DOI":"10.1007\/978-3-319-94821-8_36","volume-title":"Interactive Theorem Proving","author":"Zhao Jinxu","year":"2018","unstructured":"Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018. Formalization of a Polymorphic Subtyping Algorithm. In Interactive Theorem Proving, Jeremy Avigad and Assia Mahboubi (Eds.). Springer International Publishing, Cham, 604\u2013622."},{"key":"e_1_3_1_81_1","first-page":"112:1","article-title":"A mechanical formalization of higher-ranked polymorphic type inference","volume":"3","author":"Zhao Jinxu","year":"2019","unstructured":"Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. A mechanical formalization of higher-ranked polymorphic type inference. Proceedings of the ACM on Programming Languages 3, ICFP (2019), 112:1\u2013112:29. https:\/\/doi.org\/10.1145\/3341716 10.1145\/3341716","journal-title":"Proceedings of the ACM on Programming Languages"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689786","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689786","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:10:07Z","timestamp":1770196207000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689786"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":80,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689786"],"URL":"https:\/\/doi.org\/10.1145\/3689786","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}