Ziliani, Beta; Sozeau, Matthieu A unification algorithm for Coq featuring universe polymorphism and overloading. (English) Zbl 1360.68774 Proceedings of the 20th ACM SIGPLAN international conference on functional programming, ICFP ’15, Vancouver, Canada, September 1–3, 2015. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3669-7). 179-191 (2015). Cited in 2 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68N18 Functional programming and lambda calculus 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) Keywords:Coq; interactive theorem proving; overloading; unification; universe polymorphism Software:Coq; Mtac; Agda PDFBibTeX XMLCite \textit{B. Ziliani} and \textit{M. Sozeau}, in: Proceedings of the 20th ACM SIGPLAN international conference on functional programming, ICFP '15, Vancouver, Canada, September 1--3, 2015. New York, NY: Association for Computing Machinery (ACM). 179--191 (2015; Zbl 1360.68774) Full Text: DOI