I would like to read an introductory survey paper explaining the unification algorithm in coq.

It could be a simplified version of it, I'm not interested right now in understanding the whole algorithm in full detail.

I'm looking something that outlines the basic problem that the algorithm is trying to solve and at a high level how it accomplishes this.

the unicoq paper should fit your requirements https://github.com/unicoq/unicoq/

Thanks!

Bas Spitters has marked this topic as resolved.

Last updated: Sep 25 2023 at 12:01 UTC