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

}

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

}