%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Created for Sebastiaan Joosten at 2019-01-16 16:58:30 +0100 


%% Saved with string encoding Unicode (UTF-8) 



@article{Recursion-Theory-I-AFP,
	Author = {Michael Nedzelsky},
	Date-Added = {2019-01-16 16:46:50 +0100},
	Date-Modified = {2019-01-16 16:46:50 +0100},
	Issn = {2150-914x},
	Journal = {Archive of Formal Proofs},
	Month = apr,
	Note = {\url{http://isa-afp.org/entries/Recursion-Theory-I.html}, Formal proof development},
	Title = {Recursion Theory I},
	Year = 2008}

@article{Minsky_Machines-AFP,
	Author = {Bertram Felgenhauer},
	Date-Added = {2019-01-16 16:41:43 +0100},
	Date-Modified = {2019-01-16 16:41:43 +0100},
	Issn = {2150-914x},
	Journal = {Archive of Formal Proofs},
	Month = aug,
	Note = {\url{http://isa-afp.org/entries/Minsky_Machines.html}, Formal proof development},
	Title = {Minsky Machines},
	Year = 2018}

@article{Joosten18,
	Abstract = {We give a procedure that can be used to automatically satisfy invariants of a certain shape. These invariants may be written with the operations intersection, composition and converse over binary relations, and equality over these operations. We call these invariants sentences that we interpret over graphs. For questions stated through sets of these sentences, this paper gives a semi-decision procedure we call graph saturation. It decides entailment over these sentences, inspired on graph rewriting. We prove correctness of the procedure. Moreover, we show the corresponding decision problem to be undecidable. This confirms a conjecture previously stated by the author [7].},
	Author = {Sebastiaan J.C. Joosten},
	Date-Added = {2019-01-16 16:38:28 +0100},
	Date-Modified = {2019-01-16 16:38:28 +0100},
	Doi = {https://doi.org/10.1016/j.jlamp.2018.06.005},
	Issn = {2352-2208},
	Journal = {Journal of Logical and Algebraic Methods in Programming},
	Pages = {98 - 112},
	Title = {Finding models through graph saturation},
	Url = {http://www.sciencedirect.com/science/article/pii/S2352220817301840},
	Volume = {100},
	Year = {2018},
	Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S2352220817301840},
	Bdsk-Url-2 = {https://doi.org/10.1016/j.jlamp.2018.06.005}}

@article{Graph_Saturation-AFP,
	Author = {Sebastiaan J. C. Joosten},
	Date-Added = {2019-01-16 16:37:15 +0100},
	Date-Modified = {2019-01-16 16:37:15 +0100},
	Issn = {2150-914x},
	Journal = {Archive of Formal Proofs},
	Month = nov,
	Note = {\url{http://isa-afp.org/entries/Graph_Saturation.html}, Formal proof development},
	Title = {Graph Saturation},
	Year = 2018}

@inproceedings{Xu13,
	Abstract = {We formalise results from computability theory in the theorem prover Isabelle/HOL. Following the textbook by Boolos et al, we formalise Turing machines and relate them to abacus machines and recursive functions. We ``tie the know'' between these three computational models by formalising a universal function and obtaining from it a universal Turing machine by our verified translation from recursive functions to abacus programs and from abacus programs to Turing machine programs. Hoare-style reasoning techniques allow us to reason about concrete Turing machine and abacus programs.},
	Address = {Berlin, Heidelberg},
	Author = {Xu, Jian and Zhang, Xingyuan and Urban, Christian},
	Booktitle = {Interactive Theorem Proving},
	Date-Added = {2019-01-15 13:15:48 +0100},
	Date-Modified = {2019-01-15 13:15:48 +0100},
	Editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
	Isbn = {978-3-642-39634-2},
	Pages = {147--162},
	Publisher = {Springer Berlin Heidelberg},
	Title = {Mechanising Turing Machines and Computability Theory in Isabelle/HOL},
	Year = {2013}}

@inproceedings{Krauss10,
	Author = {A.~Krauss},
	Booktitle = {Proc.~of the Workshop on Partiality and Recursion in Interactive Theorem Provers},
	Pages = {1-13},
	Series = {EPTCS},
	Title = {{R}ecursive {D}efinitions of {M}onadic {F}unctions},
	Volume = {43},
	Year = {2010}}

@phdthesis{Myreen09,
	Author = {M.~O.~Myreen},
	School = {University of Cambridge},
	Title = {{F}ormal {V}erification of {M}achine-{C}ode {P}rograms},
	Year = 2009}

@article{Nipkow98,
	Author = {T.~Nipkow},
	Journal = {Formal Aspects of Computing},
	Pages = {171--186},
	Title = {{W}inskel is (almost) {R}ight: {T}owards a {M}echanized {S}emantics {T}extbook},
	Volume = 10,
	Year = 1998}

@inproceedings{Jensen13,
	Author = {J.~Braband Jensen and N.~Benton and A.~Kennedy},
	Booktitle = {Proc.~of the 40th Symposium on Principles of Programming Languages (POPL)},
	Pages = {301--314},
	Title = {{H}igh-{L}evel {S}eparation {L}ogic for {L}ow-{L}evel {C}ode},
	Year = {2013}}

@article{UrbanCheneyBerghofer11,
	Author = {C.~Urban and J.~Cheney and S.~Berghofer},
	Issue = {2},
	Journal = {ACM Transactions on Computational Logic},
	Pages = {15:1--15:42},
	Title = {{M}echanizing the {M}etatheory of {LF}},
	Volume = {12},
	Year = {2011}}

@inproceedings{Norrish11,
	Author = {M.~Norrish},
	Booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving (ITP)},
	Pages = {297--311},
	Series = {LNCS},
	Title = {{M}echanised {C}omputability {T}heory},
	Volume = {6898},
	Year = {2011}}

@inproceedings{AspertiRicciotti12,
	Author = {A.~Asperti and W.~Ricciotti},
	Booktitle = {Proc.~of the 19th International Workshop on Logic, Language, Information and Computation (WoLLIC)},
	Pages = {1-25},
	Series = {LNCS},
	Title = {{F}ormalizing {T}uring {M}achines},
	Volume = {7456},
	Year = {2012}}

@unpublished{WuZhangUrban12,
	Author = {C.~Wu and X.~Zhang and C.~Urban},
	Note = {Submitted},
	Title = {{A} {F}ormal {M}odel and {C}orrectness {P}roof for an {A}ccess {C}ontrol {P}olicy {F}ramework},
	Year = {2013}}

@book{Boolos07,
	Author = {G.~Boolos and J.~P.~Burgess and R.~C.~Jeffrey},
	Publisher = {Cambridge University Press},
	Title = {{C}omputability and {L}ogic (5th~ed.)},
	Year = {2007}}

@book{BoolosFourth,
	Author = {G.~Boolos and J.~P.~Burgess and R.~C.~Jeffrey},
	Publisher = {Cambridge University Press},
	Title = {{C}omputability and {L}ogic (4th~ed.)},
	Year = {2002}}

@inproceedings{WuZhangUrban11,
	Author = {C.~Wu and X.~Zhang and C.~Urban},
	Booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving},
	Pages = {341--356},
	Series = {LNCS},
	Title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions ({P}roof {P}earl)},
	Volume = {6898},
	Year = {2011}}

@article{Post36,
	Author = {E.~Post},
	Journal = {Journal of Symbolic Logic},
	Number = {3},
	Pages = {103--105},
	Title = {{F}inite {C}ombinatory {P}rocesses-{F}ormulation 1},
	Volume = {1},
	Year = {1936}}

@article{Dijkstra68,
	Author = {E.~W.~Dijkstra},
	Journal = {Communications of the ACM},
	Number = {3},
	Pages = {147-148},
	Title = {{G}o to {S}tatement {C}onsidered {H}armful},
	Volume = {11},
	Year = {1968}}

@book{Berger66,
	Author = {R.~Berger},
	Journal = {Memoirs of the American Mathematical Society},
	Title = {{T}he {U}ndecidability of the {D}omino {P}roblem},
	Year = {1966}}

@article{Robinson71,
	Author = {R.~M.~Robinson},
	Journal = {Inventiones Mathematicae},
	Pages = {177--209},
	Title = {{U}ndecidability and {N}onperiodicity for {T}ilings of the {P}lane},
	Volume = {12},
	Year = {1971}}

@phdthesis{Zammit99,
	Author = {V.~Zammit},
	School = {University of Kent},
	Title = {{O}n the {R}eadability of {M}achine {C}heckable {F}ormal {P}roofs},
	Year = {1999}}
