diff -r 00ac265b251b -r 02b6fab379ba Journal/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/root.bib	Sat Jul 27 08:17:54 2013 +0200
@@ -0,0 +1,151 @@
+@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}}
+