@inproceedings{altenkirch_et_al:LIPIcs:2016:5972,
    Address = {Dagstuhl, Germany},
    Annote = {Keywords: normalisation by evaluation, dependent types, internal type theory, logical relations, Agda},
    Author = {Altenkirch, Thorsten and Kaposi, Ambrus},
    BookTitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
    Editor = {Kesner, Delia and Pientka, Brigitte},
    File = {LIPIcs-FSCD-2016-6 (0) - a - a - m.pdf},
    ISBN = {978-3-95977-010-1},
    ISSN = {1868-8969},
    Keywords = {normalization by evaluation},
    Pages = {6:1--6:16},
    Publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
    Series = {Leibniz International Proceedings in Informatics (LIPIcs)},
    Title = {{Normalisation by Evaluation for Dependent Types}},
    URL = {http://drops.dagstuhl.de/opus/volltexte/2016/5972},
    Volume = {52},
    Year = {2016},
    bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2016/5972},
    bdsk-url-2 = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.6},
    date-added = {2017-05-03 13:05:56 +0000},
    date-modified = {2017-05-03 13:06:54 +0000},
    urn = {urn:nbn:de:0030-drops-59727},
    doi = {10.4230/LIPIcs.FSCD.2016.6}
}

@inproceedings{altenkirch_et_al:LIPIcs:2016:5972, Address = {Dagstuhl, Germany}, Annote = {Keywords: normalisation by evaluation, dependent types, internal type theory, logical relations, Agda}, Author = {Altenkirch, Thorsten and Kaposi, Ambrus}, BookTitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, Editor = {Kesner, Delia and Pientka, Brigitte}, File = {LIPIcs-FSCD-2016-6 (0) - a - a - m.pdf}, ISBN = {978-3-95977-010-1}, ISSN = {1868-8969}, Keywords = {normalization by evaluation}, Pages = {6:1--6:16}, Publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, Series = {Leibniz International Proceedings in Informatics (LIPIcs)}, Title = {{Normalisation by Evaluation for Dependent Types}}, URL = {http://drops.dagstuhl.de/opus/volltexte/2016/5972}, Volume = {52}, Year = {2016}, bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2016/5972}, bdsk-url-2 = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.6}, date-added = {2017-05-03 13:05:56 +0000}, date-modified = {2017-05-03 13:06:54 +0000}, urn = {urn:nbn:de:0030-drops-59727}, doi = {10.4230/LIPIcs.FSCD.2016.6} }