@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}}+ −
+ −