1 @inproceedings{Krauss10,

     2   author    = {A.~Krauss},

     3   title     = {{R}ecursive {D}efinitions of {M}onadic {F}unctions},

     4   booktitle = {Proc.~of the Workshop on Partiality and Recursion in Interactive

     5                Theorem Provers},

     6   year      = {2010},

     7   pages     = {1-13},

     8   series    = {EPTCS},

     9   volume    = {43}

    10 }

    11 

    12 @PhdThesis{Myreen09,

    13   author =	 {M.~O.~Myreen},

    14   title = 	 {{F}ormal {V}erification of {M}achine-{C}ode {P}rograms},

    15   year = 	 2009,

    16   school =  {University of Cambridge}

    17 }

    18 

    19 @article{Nipkow98,

    20   author={T.~Nipkow},

    21   title={{W}inskel is (almost) {R}ight: {T}owards a {M}echanized {S}emantics {T}extbook},

    22   journal={Formal Aspects of Computing},

    23   volume=10,

    24   pages={171--186},

    25   year=1998

    26 }

    27 

    28 @inproceedings{Jensen13,

    29   author    = {J.~Braband Jensen and

    30                N.~Benton and

    31                A.~Kennedy},

    32   title     = {{H}igh-{L}evel {S}eparation {L}ogic for {L}ow-{L}evel {C}ode},

    33   booktitle = {Proc.~of the 40th Symposium on Principles

    34                of Programming Languages (POPL)},

    35   year      = {2013},

    36   pages     = {301--314}

    37 }

    38 

    39 @article{UrbanCheneyBerghofer11,

    40   author = {C.~Urban and J.~Cheney and S.~Berghofer},

    41   title = {{M}echanizing the {M}etatheory of {LF}},

    42   journal = {ACM Transactions on Computational Logic},

    43   volume = {12},

    44   issue = {2},

    45   year = {2011},

    46   pages = {15:1--15:42}

    47 }

    48 

    49 @inproceedings{Norrish11,

    50   author    = {M.~Norrish},

    51   title     = {{M}echanised {C}omputability {T}heory},

    52   booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving (ITP)},

    53   year      = {2011},

    54   series    = {LNCS},

    55   volume    = {6898},

    56   pages     = {297--311}

    57 }

    58 

    59 @inproceedings{AspertiRicciotti12,

    60   author    = {A.~Asperti and W.~Ricciotti},

    61   title     = {{F}ormalizing {T}uring {M}achines},

    62   booktitle = {Proc.~of the 19th International Workshop on Logic, Language, 

    63                Information and Computation (WoLLIC)},

    64   year      = {2012},

    65   pages     = {1-25},

    66   series    = {LNCS},

    67   volume    = {7456}

    68 }

    69 

    70 

    71 @Unpublished{WuZhangUrban12,

    72   author = 	 {C.~Wu and X.~Zhang and C.~Urban},

    73   title = 	 {{A} {F}ormal {M}odel and {C}orrectness {P}roof for an 

    74                   {A}ccess {C}ontrol {P}olicy {F}ramework},

    75   note = 	 {Submitted},

    76   year = 	 {2013}

    77 }

    78 

    79 @book{Boolos87,

    80   author    = {G.~Boolos and J.~P.~Burgess and R.~C.~Jeffrey},

    81   title     = {{C}omputability and {L}ogic (5th~ed.)},

    82   publisher = {Cambridge University Press},

    83   year      = {2007}

    84 }

    85 

    86 @book{BoolosFourth,

    87   author    = {G.~Boolos and J.~P.~Burgess and R.~C.~Jeffrey},

    88   title     = {{C}omputability and {L}ogic (4th~ed.)},

    89   publisher = {Cambridge University Press},

    90   year      = {2002}

    91 }

    92 

    93 

    94 @inproceedings{WuZhangUrban11,

    95   author    = {C.~Wu and X.~Zhang and C.~Urban},

    96   title     = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions

    97                ({P}roof {P}earl)},

    98   booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving},

    99   year      = {2011},

   100   pages     = {341--356},

   101   series    = {LNCS},

   102   volume    = {6898}

   103 }

   104 

   105 

   106 @Article{Post36,

   107   author =       {E.~Post},

   108   title =        {{F}inite {C}ombinatory {P}rocesses-{F}ormulation 1},

   109   journal =      {Journal of Symbolic Logic},

   110   year =         {1936},

   111   volume =       {1},

   112   number =       {3},

   113   pages =        {103--105}

   114 }

   115 

   116 @article{Dijkstra68,

   117   author    = {E.~W.~Dijkstra},

   118   title     = {{G}o to {S}tatement {C}onsidered {H}armful},

   119   journal   = {Communications of the ACM},

   120   volume    = {11},

   121   number    = {3},

   122   year      = {1968},

   123   pages     = {147-148}

   124 }

   125 

   126 

   127 

   128 @Book{Berger66,

   129   author = 	 {R.~Berger},

   130   title = 	 {{T}he {U}ndecidability of the {D}omino {P}roblem},

   131   journal = 	 {Memoirs of the American Mathematical Society},

   132   year = 	 {1966}

   133 }

   134 

   135 

   136 @Article{Robinson71,

   137   author = 	 {R.~M.~Robinson},

   138   title = 	 {{U}ndecidability and {N}onperiodicity for {T}ilings of the {P}lane},

   139   journal = 	 {Inventiones Mathematicae},

   140   year = 	 {1971},

   141   volume = 	 {12},

   142   pages = 	 {177--209}

   143 }

   144 

   145 

   146 @phdthesis{Zammit99,

   147 author = {V.~Zammit},

   148 title = {{O}n the {R}eadability of {M}achine {C}heckable {F}ormal {P}roofs},

   149 year = {1999},

   150 school = {University of Kent}}

   151