@inproceedings{Krauss10, author = {A.~Krauss}, title = {{R}ecursive {D}efinitions of {M}onadic {F}unctions}, booktitle = {Proc.~of the Workshop on Partiality and Recursion in Interactive Theorem Provers}, year = {2010}, pages = {1-13}, series = {EPTCS}, volume = {43}}@PhdThesis{Myreen09, author = {M.~O.~Myreen}, title = {{F}ormal {V}erification of {M}achine-{C}ode {P}rograms}, year = 2009, school = {University of Cambridge}}@article{Nipkow98, author={T.~Nipkow}, title={{W}inskel is (almost) {R}ight: {T}owards a {M}echanized {S}emantics {T}extbook}, journal={Formal Aspects of Computing}, volume=10, pages={171--186}, year=1998}@inproceedings{Jensen13, author = {J.~Braband Jensen and N.~Benton and A.~Kennedy}, title = {{H}igh-{L}evel {S}eparation {L}ogic for {L}ow-{L}evel {C}ode}, booktitle = {Proc.~of the 40th Symposium on Principles of Programming Languages (POPL)}, year = {2013}, pages = {301--314}}@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 = {{A} {F}ormal {M}odel and {C}orrectness {P}roof for an {A}ccess {C}ontrol {P}olicy {F}ramework}, note = {Submitted}, year = {2013}}@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}}@book{BoolosFourth, author = {G.~Boolos and J.~P.~Burgess and R.~C.~Jeffrey}, title = {{C}omputability and {L}ogic (4th~ed.)}, publisher = {Cambridge University Press}, year = {2002}}@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}}@article{Dijkstra68, author = {E.~W.~Dijkstra}, title = {{G}o to {S}tatement {C}onsidered {H}armful}, journal = {Communications of the ACM}, volume = {11}, number = {3}, year = {1968}, pages = {147-148}}@Book{Berger66, author = {R.~Berger}, title = {{T}he {U}ndecidability of the {D}omino {P}roblem}, journal = {Memoirs of the American Mathematical Society}, year = {1966}}@Article{Robinson71, author = {R.~M.~Robinson}, title = {{U}ndecidability and {N}onperiodicity for {T}ilings of the {P}lane}, journal = {Inventiones Mathematicae}, year = {1971}, volume = {12}, pages = {177--209}}@phdthesis{Zammit99,author = {V.~Zammit},title = {{O}n the {R}eadability of {M}achine {C}heckable {F}ormal {P}roofs},year = {1999},school = {University of Kent}}