@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 J.~P.~Burgess and R.~C.~Jeffrey}, title = {{C}omputability and {L}ogic (5th~ed.)}, publisher = {Cambridge University Press}, year = {2007}}@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}}@Article{Post36, author = {E.~Post}, title = {{F}inite {C}ombinatory {P}rocesses-{F}ormulation 1}, journal = {Journal of Symbolic Logic}, year = {1936}, volume = {1}, number = {3}, pages = {103--105}}