Beta Ziliani, Matthieu Sozeau
A unification algorithm for Coq featuring universe polymorphism and overloading
ICFP, 2015.
@inproceedings{ICFP-2015-ZilianiS, author = "Beta Ziliani and Matthieu Sozeau", booktitle = "{Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming}", doi = "10.1145/2784731.2784751", isbn = "978-1-4503-3669-7", pages = "179--191", publisher = "{ACM}", title = "{A unification algorithm for Coq featuring universe polymorphism and overloading}", year = 2015, }