--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/root.bib Fri Jan 18 11:40:01 2013 +0000
@@ -0,0 +1,68 @@
+@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 = {???},
+ note = {Submitted},
+ year = {2012}
+}
+
+@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}
+}
+