@inproceedings{Aehlig:2008:CIN:1459784.1459795,
    Address = {Berlin, Heidelberg},
    Author = {Aehlig, Klaus and Haftmann, Florian and Nipkow, Tobias},
    BookTitle = {Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics},
    File = {A Compiled Implementation of Normalization by Evaluation - Aehlig, Haftmann, Nipkow (1) (0) - a - a - x.pdf},
    ISBN = {978-3-540-71065-3},
    Location = {Montreal, P.Q., Canada},
    Pages = {39--54},
    Publisher = {Springer-Verlag},
    Series = {TPHOLs '08},
    Title = {A Compiled Implementation of Normalization by Evaluation},
    URL = {http://dx.doi.org/10.1007/978-3-540-71067-7\_8},
    Year = {2008},
    acmid = {1459795},
    bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-71067-7\_8},
    date-added = {2013-06-11 12:09:42 +0000},
    date-modified = {2013-06-11 12:09:42 +0000},
    file-2 = {A Compiled Implementation of Normalization by Evaluation - Aehlig, Haftmann, Nipkow (0) (1) - a - a - x.pdf},
    numpages = {16},
    doi = {10.1007/978-3-540-71067-7_8}
}

@inproceedings{Aehlig:2008:CIN:1459784.1459795, Address = {Berlin, Heidelberg}, Author = {Aehlig, Klaus and Haftmann, Florian and Nipkow, Tobias}, BookTitle = {Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics}, File = {A Compiled Implementation of Normalization by Evaluation - Aehlig, Haftmann, Nipkow (1) (0) - a - a - x.pdf}, ISBN = {978-3-540-71065-3}, Location = {Montreal, P.Q., Canada}, Pages = {39--54}, Publisher = {Springer-Verlag}, Series = {TPHOLs '08}, Title = {A Compiled Implementation of Normalization by Evaluation}, URL = {http://dx.doi.org/10.1007/978-3-540-71067-7_8}, Year = {2008}, acmid = {1459795}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-71067-7_8}, date-added = {2013-06-11 12:09:42 +0000}, date-modified = {2013-06-11 12:09:42 +0000}, file-2 = {A Compiled Implementation of Normalization by Evaluation - Aehlig, Haftmann, Nipkow (0) (1) - a - a - x.pdf}, numpages = {16}, doi = {10.1007/978-3-540-71067-7_8} }