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