@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}
}

@inproceedings{Norrish11,
  author    = {M.~Norrish},
  title     = {{M}echanised {C}omputability {T}heory},
  booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving (ITP)},
  year      = {2011},
  series    = {LNCS},
  volume    = {6898},
  pages     = {297--311}
}

@inproceedings{AspertiRicciotti12,
  author    = {A.~Asperti and W.~Ricciotti},
  title     = {{F}ormalizing {T}uring {M}achines},
  booktitle = {Proc.~of the 19th International Workshop on Logic, Language, 
               Information and Computation (WoLLIC)},
  year      = {2012},
  pages     = {1-25},
  series    = {LNCS},
  volume    = {7456}
}


@Unpublished{WuZhangUrban12,
  author = 	 {C.~Wu and X.~Zhang and C.~Urban},
  title = 	 {???},
  note = 	 {Submitted},
  year = 	 {2012}
}

@book{Boolos87,
  author    = {G.~Boolos and R.~C.~Jeffrey},
  title     = {{C}omputability and {L}ogic (2.~ed.)},
  publisher = {Cambridge University Press},
  year      = {1987}
}

@inproceedings{WuZhangUrban11,
  author    = {C.~Wu and X.~Zhang and C.~Urban},
  title     = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions
               ({P}roof {P}earl)},
  booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving},
  year      = {2011},
  pages     = {341--356},
  series    = {LNCS},
  volume    = {6898}
}