A unification algorithm for Coq featuring universe polymorphism and overloading

DOI10.1145/2784731.2784751zbMath1360.68774OpenAlexW2013202135MaRDI QIDQ2981954

Beta Ziliani, Matthieu Sozeau

Publication date: 10 May 2017

Published in: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2784731.2784751

zbMATH Keywords

unificationinteractive theorem provingCoqoverloadinguniverse polymorphism

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (2)

Functions-as-constructors higher-order unification: extended pattern unification ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading

Uses Software

• Coq
• Agda
• Mtac

This page was built for publication: A unification algorithm for Coq featuring universe polymorphism and overloading