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]

Abstract

Abstract is missing.