Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory

Jesper Cockx, Dominique Devriese. Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory. Journal of Functional Programming, 28, 2018. [doi]

Possibly Related Publications

The following publications are possibly variants of this publication: