1 @article{UrbanCheneyBerghofer11,

     2   author = {C.~Urban and J.~Cheney and S.~Berghofer},

     3   title = {{M}echanizing the {M}etatheory of {LF}},

     4   journal = {ACM Transactions on Computational Logic},

     5   volume = {12},

     6   issue = {2},

     7   year = {2011},

     8   pages = {15:1--15:42}

     9 }