@article{10.1023/A:1019964114625,
    Address = {USA},
    Author = {Coquand, Catarina},
    File = {A Formalised Proof of the Soundness and Completeness of a Simply Typed Lambda-Calculus with Explicit Substitutions - coquand2002 - a - a - a - e.pdf},
    ISSN = {1388-3690},
    Journal = {Higher Order Symbol. Comput.},
    Keywords = {type theory, formal methods, explicit substitutions, normalisation},
    Month = {March},
    Number = {1},
    Pages = {57--90},
    Publisher = {Kluwer Academic Publishers},
    Title = {A Formalised Proof of the Soundness and Completeness of a Simply Typed Lambda-Calculus with Explicit Substitutions},
    URL = {https://doi.org/10.1023/A:1019964114625},
    Volume = {15},
    Year = {2002},
    bdsk-url-1 = {https://doi.org/10.1023/A:1019964114625},
    date-added = {2020-03-30 19:42:08 +0200},
    date-modified = {2020-03-30 19:42:08 +0200},
    issue_date = {March 2002},
    numpages = {34},
    doi = {10.1023/A:1019964114625}
}

@article{10.1023/A:1019964114625, Address = {USA}, Author = {Coquand, Catarina}, File = {A Formalised Proof of the Soundness and Completeness of a Simply Typed Lambda-Calculus with Explicit Substitutions - coquand2002 - a - a - a - e.pdf}, ISSN = {1388-3690}, Journal = {Higher Order Symbol. Comput.}, Keywords = {type theory, formal methods, explicit substitutions, normalisation}, Month = {March}, Number = {1}, Pages = {57--90}, Publisher = {Kluwer Academic Publishers}, Title = {A Formalised Proof of the Soundness and Completeness of a Simply Typed Lambda-Calculus with Explicit Substitutions}, URL = {https://doi.org/10.1023/A:1019964114625}, Volume = {15}, Year = {2002}, bdsk-url-1 = {https://doi.org/10.1023/A:1019964114625}, date-added = {2020-03-30 19:42:08 +0200}, date-modified = {2020-03-30 19:42:08 +0200}, issue_date = {March 2002}, numpages = {34}, doi = {10.1023/A:1019964114625} }