- https://dl.acm.org/doi/10.1145/1637837.1637839; Automatically computing functional instantiations
- http://conal.net/papers/elliott90.pdf; conal elliot's thesis
- https://dl.acm.org/doi/10.5555/778522.778525; Higher-order unification and matching
- https://arxiv.org/abs/2312.07263; A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
- https://arxiv.org/abs/2204.05653; Free Monads, Intrinsic Scoping, and Higher-Order Preunification
- https://arxiv.org/abs/1505.04324; lean's elaboration algo
- https://adam.gundry.co.uk/pub/pattern-unify/pattern-unification-2012-07-10.pdf; adam gundry's presentation of pattern unification
- https://adam.gundry.co.uk/pub/thesis/thesis-2013-12-03.pdf; more gundry
- doi:10.1017/S0956796817000028; A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- https://doi.org/10.1515/comp-2019-0001; A framework for improving error messages in dependently-typed languages
- https://lopezjuan.com/project/togt/tyde2020_2020-06-17_2312da11.pdf; Practical Dependent Type Checking Using Twin Types
- https://arxiv.org/pdf/1609.09709v1.pdf; Type checking through unification