Simon Spies, Yannick Forster 0002. Undecidability of higher-order unification formalised in Coq. In Jasmin Blanchette, Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. pages 143-157, ACM, 2020. [doi]
@inproceedings{Spies020,
title = {Undecidability of higher-order unification formalised in Coq},
author = {Simon Spies and Yannick Forster 0002},
year = {2020},
doi = {10.1145/3372885.3373832},
url = {https://doi.org/10.1145/3372885.3373832},
researchr = {https://researchr.org/publication/Spies020},
cites = {0},
citedby = {0},
pages = {143-157},
booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020},
editor = {Jasmin Blanchette and Catalin Hritcu},
publisher = {ACM},
isbn = {978-1-4503-7097-4},
}