@article{COCKX_2018,
    doi = {10.1017/s095679681800014x},
    url = {https://doi.org/10.1017%2Fs095679681800014x},
    year = {2018},
    publisher = {Cambridge University Press ({CUP})},
    volume = {28},
    author = {JESPER COCKX and DOMINIQUE DEVRIESE},
    title = {Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory},
    journal = {Journal of Functional Programming}
}

@article{COCKX_2018, doi = {10.1017/s095679681800014x}, url = {https://doi.org/10.1017%2Fs095679681800014x}, year = {2018}, publisher = {Cambridge University Press ({CUP})}, volume = {28}, author = {JESPER COCKX and DOMINIQUE DEVRIESE}, title = {Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory}, journal = {Journal of Functional Programming} }