@article{UrbanCheneyBerghofer11,
  author = {C.~Urban and J.~Cheney and S.~Berghofer},
  title = {{M}echanizing the {M}etatheory of {LF}},
  journal = {ACM Transactions on Computational Logic},
  volume = {12},
  issue = {2},
  year = {2011},
  pages = {15:1--15:42}
}