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