@article{gilbert:hal-01859964,
    Author = {Gilbert, Ga{\"e}tan and Cockx, Jesper and Sozeau, Matthieu and Tabareau, Nicolas},
    File = {Definitional Proof-Irrelevance without K (0) - a - a - d.pdf},
    Journal = {{Proceedings of the ACM on Programming Languages}},
    Month = {January},
    PDF = {https://hal.inria.fr/hal-01859964/file/main\_popl.pdf},
    Pages = {1-28},
    Publisher = {{ACM}},
    Series = {POPL'19},
    Title = {{Definitional Proof-Irrelevance without K}},
    URL = {https://hal.inria.fr/hal-01859964},
    Year = {2019},
    bdsk-url-1 = {https://hal.inria.fr/hal-01859964},
    bdsk-url-2 = {https://doi.org/10.1145/329031610.1145/3290316},
    date-added = {2019-04-16 10:34:24 +0200},
    date-modified = {2019-04-16 10:34:24 +0200},
    hal_id = {hal-01859964},
    hal_local_reference = {BEST},
    hal_version = {v2},
    doi = {10.1145/329031610.1145/3290316}
}

@article{gilbert:hal-01859964, Author = {Gilbert, Ga{\"e}tan and Cockx, Jesper and Sozeau, Matthieu and Tabareau, Nicolas}, File = {Definitional Proof-Irrelevance without K (0) - a - a - d.pdf}, Journal = {{Proceedings of the ACM on Programming Languages}}, Month = {January}, PDF = {https://hal.inria.fr/hal-01859964/file/main_popl.pdf}, Pages = {1-28}, Publisher = {{ACM}}, Series = {POPL'19}, Title = {{Definitional Proof-Irrelevance without K}}, URL = {https://hal.inria.fr/hal-01859964}, Year = {2019}, bdsk-url-1 = {https://hal.inria.fr/hal-01859964}, bdsk-url-2 = {https://doi.org/10.1145/329031610.1145/3290316}, date-added = {2019-04-16 10:34:24 +0200}, date-modified = {2019-04-16 10:34:24 +0200}, hal_id = {hal-01859964}, hal_local_reference = {BEST}, hal_version = {v2}, doi = {10.1145/329031610.1145/3290316} }