×

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).

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.)

Software:

Coq; Mtac; Agda
PDFBibTeX XMLCite
Full Text: DOI