--- /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}}
+