Publications

Journal Articles

  1. & Verification of the European Rail Traffic Management System in Real-Time Maude. Science of Computer Programming
  2. & Program extraction applied to monadic parsing. Journal of Logic and Computation, exv078
  3. & Extracting verified decision procedures: DPLL and Resolution. Logical Methods in Computer Science 11(1)
  4. & Extracting a DPLL Algorithm. Electronic Notes in Theoretical Computer Science 286, 243-256.
  5. & Proofs, Programs, Processes. Theory of Computing Systems 51(3), 313-329.
  6. Programs from proofs using classical dependent choice. Annals of Pure and Applied Logic 153(1-3), 97-110.
  7. & Applications of inductive definitions and choice principles to program synthesis. Oxford Logic Guides 48, 137-148.
  8. Kruskal's tree theorem in a constructive theory of inductive definitions. Synthese Library 306, 241-255.
  9. & The Warshall Algorithm and Dickson's Lemma: Two examples of realistic program extraction. Journal of Automated Reasoning 26(2), 205-221.

Book Chapters

  1. & Higman’s Lemma and Its Computational Content. In Advances in Proof Theory. (pp. 353-375).
  2. & Towards Safety Analysis of ERTMS/ETCS Level 2 in Real-Time Maude. In Formal Techniques for Safety-Critical Systems. Springer.
  3. & Verification of Solid State Interlocking Programs. In Counsell, Steve and Nunez, Manuel (Ed.), Software Engineering and Formal Methods. (pp. 253-268). Springer.
  4. & Proof theory at work: Program development in the Minlog system. In W. Bibel and P.H. Schmitt (Ed.), Automated Deduction - A Basis for Applications. (pp. 41-71). Dordrecht: Kluwer.
  5. & Program extraction via typed realisability for induction and coinduction. In Ways of Proof Theory. (pp. 157-181). Frankfurt: Ontos Verlag.

Conference Contributions

  1. & (2018). A Chatbot Framework for the Children’s Legal Centre. Presented at Frontiers in Artificial Intelligence and Applications,, 205-209. doi:10.3233/978-1-61499-935-5-205
  2. & (2011). Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras. Presented at Lecture Notes In Computer Science,, 393-399. doi:10.1007/978-3-642-22944-2_29
  3. & (2010). Proofs, Programs, Processes. Presented at Lecture Notes In Computer Science,, 39-48. doi:10.1007/978-3-642-13962-8_5
  4. (2001). An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument for Higman’s Lemma. Presented at Lecture Notes In Computer Science,, 233-242.Springer. doi:10.1007/3-540-45842-5_15