{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:16Z","timestamp":1776891436050,"version":"3.51.2"},"reference-count":42,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2017,2,7]],"date-time":"2017-02-07T00:00:00Z","timestamp":1486425600000},"content-version":"unspecified","delay-in-days":37,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Unification is a core component of every proof assistant or programming language featuring dependent types. In many cases, it must deal with higher order problems up to conversion. Since unification in such conditions is undecidable, unification algorithms may include several heuristics to solve common problems. However, when the stack of heuristics grows large, the result and complexity of the algorithm can become unpredictable. Our contributions are twofold: (1) We present a full description of a new unification algorithm for the Calculus of Inductive Constructions (the base logic of C\n                    <jats:sc>OQ<\/jats:sc>\n                    ), building it up from a basic calculus to the full Calculus of Inductive Constructions as it is implemented in C\n                    <jats:sc>OQ<\/jats:sc>\n                    , including universe polymorphism, canonical structures (the overloading mechanism baked into C\n                    <jats:sc>OQ<\/jats:sc>\n                    's unification), and a small set of useful heuristics. (2) We implemented our algorithm, and tested it on several libraries, providing evidence that the selected set of heuristics suffices for large developments.\n                  <\/jats:p>","DOI":"10.1017\/s0956796817000028","type":"journal-article","created":{"date-parts":[[2017,2,7]],"date-time":"2017-02-07T05:56:38Z","timestamp":1486446998000},"source":"Crossref","is-referenced-by-count":5,"title":["A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading"],"prefix":"10.46298","volume":"27","author":[{"given":"BETA","family":"ZILIANI","sequence":"first","affiliation":[]},{"given":"MATTHIEU","family":"SOZEAU","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2017,2,7]]},"reference":[{"key":"S0956796817000028_ref39","volume-title":"Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Wadler","year":"1989"},{"key":"S0956796817000028_ref24","unstructured":"Mahboubi A. & Tassi E. (2013) Canonical Structures for the working Coq user. In ITP. ed. Blazy, Sandrine, Paulin-Mohring, Christine, Pichardie, David. Springer, pp. 19\u201334."},{"key":"S0956796817000028_ref37","unstructured":"Sozeau M. & Tabareau N. (2014) Universe polymorphism in Coq. In Proceedings of International Conference on Interactive Theorem Proving (ITP). Berlin, Heidelberg, Springer, pp. 499\u2013514."},{"key":"S0956796817000028_ref19","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000051"},{"key":"S0956796817000028_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(85)90009-7"},{"key":"S0956796817000028_ref30","doi-asserted-by":"crossref","unstructured":"Peyton Jones S. , Vytiniotis D. , Weirich S. & Washburn G. (2006) Simple unification-based type inference for GADTs. In Proceedings of Inernational Conference of Functional Programming (ICFP). New York, NY, USA: ACM. pp. 50\u201361.","DOI":"10.1145\/1159803.1159811"},{"key":"S0956796817000028_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/1577824.1577832"},{"key":"S0956796817000028_ref3","doi-asserted-by":"crossref","unstructured":"Asperti A. , Ricciotti W. , Coen C. S. & Tassi E. (2009) Hints in unification. In TPHOLs, ed. Berghofer, Stefan, Nipkow, Tobias, Urban, Christian, Wenzel, Makarius, LNCS, vol. 5674. Berlin, Heidelberg: Springer, pp. 84\u201398.","DOI":"10.1007\/978-3-642-03359-9_8"},{"key":"S0956796817000028_ref31","doi-asserted-by":"crossref","unstructured":"Pfenning F. (1991) Unification and anti-unification in the calculus of constructions. In Proceedings of 6th Annual IEEE Symposium on Logic in Computer Science, Ieee Computer Society, Washington, D.C., United States, pp. 74\u201385.","DOI":"10.1109\/LICS.1991.151632"},{"key":"S0956796817000028_ref27","unstructured":"Norell U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory. PhD Thesis, Chalmers University of Technology."},{"key":"S0956796817000028_ref22","doi-asserted-by":"crossref","unstructured":"Huet G. P. (2002) Higher order unification 30 years later. In Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics. In TPHOLs '02. London, UK: Springer-Verlag, pp. 3\u201312.","DOI":"10.1007\/3-540-45685-6_2"},{"key":"S0956796817000028_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"S0956796817000028_ref6","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"Baader","year":"1994"},{"key":"S0956796817000028_ref38","unstructured":"The Coq Development Team. (2012) The Coq Proof Assistant Reference Manual \u2013 Version V8.4. Available at: http:\/\/coq.inria.fr\/V8.4\/CREDITS."},{"key":"S0956796817000028_ref40","unstructured":"Ziliani B. & Sozeau M. (2015) A unification algorithm for Coq featuring universe polymorphism and overloading. In Proceedings of the International Conference of Functional Programming (ICFP). New York, NY, USA: ACM, pp. 179\u2013191."},{"key":"S0956796817000028_ref16","doi-asserted-by":"crossref","unstructured":"Garillot F. , Gonthier G. , Mahboubi A. & Rideau L. (2009) Packaging mathematical structures. In TPHOL. ed. Berghofer, Stefan, Nipkow, Tobias, Urban, Christian, Wenzel, Makarius: Springer, pp. 327\u2013342.","DOI":"10.1007\/978-3-642-03359-9_23"},{"key":"S0956796817000028_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"S0956796817000028_ref25","unstructured":"Miller D. (1991) Unification of simply typed lamda-terms as logic programming. In ICLP. ed. Beaumont, Anthony and Gupta, Gopal, MIT Press, pp. 255-269."},{"key":"S0956796817000028_ref28","first-page":"230","volume-title":"Types in Language Design and Implementation (TLDI)","author":"Norell","year":"2009"},{"key":"S0956796817000028_ref9","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.5.639"},{"key":"S0956796817000028_ref1","doi-asserted-by":"crossref","unstructured":"Abel A. & Pientka B. (2011) Higher-order dynamic pattern unification for dependent types and records. In Proceedings of International Conference on Typed Lambda Calculi and Applications (TLCA). Berlin, Heidelberg: Springer, pp. 10\u201326.","DOI":"10.1007\/978-3-642-21691-6_5"},{"key":"S0956796817000028_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"S0956796817000028_ref4","first-page":"1","article-title":"A bi-directional refinement algorithm for the calculus of (co)inductive constructions","volume":"8","author":"Asperti","year":"2012","journal-title":"Log. Methods Comput. Sci. (LMCS)"},{"key":"S0956796817000028_ref18","first-page":"163","volume-title":"Proceedings of Inernational Conference of Functional Programming (ICFP)","author":"Gonthier","year":"2011"},{"key":"S0956796817000028_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500579"},{"key":"S0956796817000028_ref32","first-page":"1657","volume-title":"Types for Proofs and Programs","author":"Pfenning","year":"1998"},{"key":"S0956796817000028_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"S0956796817000028_ref17","unstructured":"Gonthier G. , Mahboubi A. & Tassi E. (2008) A Small Scale Reflection Extension for the Coq System. Technical Report, INRIA."},{"key":"S0956796817000028_ref35","unstructured":"Sacerdoti Coen C. (2004) Mathematical Knowledge Management and Interactive Theorem Proving. PhD Thesis, University of Bologna."},{"key":"S0956796817000028_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/62029.62030"},{"key":"S0956796817000028_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"S0956796817000028_ref14","doi-asserted-by":"crossref","unstructured":"Elliott C. M. (1989) Higher-order unification with dependent function types. In Proceedings of 3rd International Conference Rewriting Techniques and Applications, LNCS, vol. 355. Berlin, Heidelberg: Springer-Verlag, pp. 121\u2013136.","DOI":"10.1007\/3-540-51081-8_104"},{"key":"S0956796817000028_ref20","doi-asserted-by":"crossref","unstructured":"Gonthier G. , Asperti A. , Avigad J. , Bertot Y. , Cohen C. , Garillot F. , Le Roux S. , Mahboubi A. , O'Connor R. , Ould Biha S. , Pasca I. , Rideau L. , Solovyev A. , Tassi E. & Th\u00e9ry L. (2013b) A machine-checked proof of the odd order theorem. In ITP. ed. Blazy, Sandrine, Paulin-Mohring, Christine, Pichardie, David. Springer, pp. 163\u2013179.","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"S0956796817000028_ref36","unstructured":"Sa\u00edbi A. (1999) Outils Generiques de Modelisation et de Demonstration Pour la Formalisation des Mathematiques en Theorie des Types. Application a la Theorie des Categories. PhD Thesis, University Paris 6."},{"key":"S0956796817000028_ref2","unstructured":"Asperti A. , Coen C. S. , Tassi E. & Zacchiroli S. (2006) Crafting a proof assistant. In Berlin, Heidelberg: Springer-Verlag, ed. Altenkirch, Thorsten and McBride, Conor, pp. 18\u201332."},{"key":"S0956796817000028_ref10","volume-title":"Certified Programming with Dependent Types","author":"Chlipala","year":"2011"},{"key":"S0956796817000028_ref12","unstructured":"Dowek G. , Hardin T. , Kirchner C. & Pfenning F. (1996) Unification via explicit substitutions: The case of higher-order patterns. In Proceedings of lics'95. IEEE Computer Society Press, Washington, DC, USA, pp. 36637\u20134, 366\u2013381."},{"key":"S0956796817000028_ref15","unstructured":"Garillot F. (2011 December) Generic Proof Tools and Finite Group Theory. PhD Thesis, Ecole Polytechnique X."},{"key":"S0956796817000028_ref42","volume-title":"J. Funct. Program. (JFP)","volume":"25","author":"Ziliani","year":"2015"},{"key":"S0956796817000028_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90108-T"},{"key":"S0956796817000028_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2756553"},{"key":"S0956796817000028_ref11","unstructured":"de Moura L. , Avigad J. , Kong S. & Roux C. (2015) Elaboration in dependent type theory. Arxiv e-prints, May."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796817000028","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:50Z","timestamp":1776889190000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796817000028\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":42,"alternative-id":["S0956796817000028"],"URL":"https:\/\/doi.org\/10.1017\/s0956796817000028","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"article-number":"e10"}}