Author of the publication

Mechanising Turing Machines and Computability Theory in Isabelle/HOL.

, , and . ITP, volume 7998 of Lecture Notes in Computer Science, page 147-162. Springer, (2013)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof., and . RTA, volume 5117 of Lecture Notes in Computer Science, page 409-424. Springer, (2008)A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)., , and . ITP, volume 6898 of Lecture Notes in Computer Science, page 341-356. Springer, (2011)Nominal logic programming., and . ACM Trans. Program. Lang. Syst., 30 (5): 26:1-26:47 (2008)A New Foundation for Nominal Isabelle., and . ITP, volume 6172 of Lecture Notes in Computer Science, page 35-50. Springer, (2010)A Formal Model and Correctness Proof for an Access Control Policy Framework., , and . CPP, volume 8307 of Lecture Notes in Computer Science, page 292-307. Springer, (2013)Priority Inheritance Protocol Proved Correct., , and . J. Autom. Reason., 64 (1): 73-95 (2020)Strong Normalisation of Cut-Elimination in Classical Logic., and . Fundam. Informaticae, 45 (1-2): 123-155 (2001)Formal SOS-Proofs for the Lambda-Calculus., and . LSFA, volume 247 of Electronic Notes in Theoretical Computer Science, page 139-155. Elsevier, (2008)Quotients revisited for Isabelle/HOL., and . SAC, page 1639-1644. ACM, (2011)POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)., , and . ITP, volume 9807 of Lecture Notes in Computer Science, page 69-86. Springer, (2016)