Journal Articles

  1. & A light-weight integration of automated and interactive theorem proving. Mathematical Structures in Computer Science 26(01), 129-153.
  2. & Defining Trace Semantics for CSP-Agda. Leibniz International Proceedings in Informatics, LIPIcs 97, 12:1-12:23.
  3. & Trace and Stable Failures Semantics for CSP-Agda. Electronic Proceedings in Theoretical Computer Science 258, 36-51.
  4. & Interactive programming in Agda – Objects and graphical user interfaces. Journal of Functional Programming 27
  5. & Automated Verification of Signalling Principles in Railway Interlocking Systems. Electronic Notes in Theoretical Computer Science 250(2), 19-31.
  6. & Automated Verification of Signalling Principles in Railway Interlocking Systems. Electronic Notes in Theoretical Computer Science 250(2), 19-31.
  7. & A Provably Correct Translation of the λ-Calculus into a Mathematical Model of C++. Theory of Computing Systems 43(3-4), 298-321.
  8. & Indexed induction–recursion. The Journal of Logic and Algebraic Programming 66(1), 1
  9. & Induction–recursion and initial algebras. Annals of Pure and Applied Logic 124(1-3), 1-47.

Book Chapters

  1. An Upper Bound for the Proof Theoretic Strength of Martin-Löf Type Theory with W-type and one Universe. In Springer.
  2. & Developing GUI Applications in a Verified Setting. In Dependable Software Engineering. Theories, Tools, and Applications. (pp. 89-107). Beijing, China: Dependable Software Engineering. Theories, Tools, and Applications 4th International Symposium, SETTA 2018.
  3. How to Reason Coinductively Informally. In Reinhard Kahle, Thomas Strahm, Thomas Studer (Ed.), Advances in Proof Theory. -408). Switzerland: Birkhäuser.
  4. The Use of Trustworthy Principles in a Revised Hilbert’s Program. In Reinhard Kahle, Michael Rathjen (Ed.), Gentzen's Centenary. (pp. 45-60). Springer.
  5. Coalgebras as Types Determined by Their Elimination Rules. In Peter Dybjerl; Sten Lindström; Erik Palmgren; Göran Sundholm (Ed.), Epistemology versus Ontology. (pp. 351-369).
  6. Proof theory and Martin-Löf Type Theory. In One Hundred Years of Intuitionism (1907–2007). (pp. 257-279). Birkhäuser.
  7. & Inductive-Inductive Definitions. In Computer Science Logic. (pp. 454-468). Springer.
  8. Universes in type theory part I—Inaccessibles and Mahlo. In Logic Colloquium 2004. (pp. 123-156). Cambridge University Press.
  9. & An extended predicative definition of the Mahlo universe. In Ralf Schindler (Ed.), Ways of Proof Theory. (pp. 309-334). Berlin, Boston: De Gruyter.

Conference Contributions

  1. & Martin Hofmann’s case for non-strictly positive data types. Presented at Proceedings of Types 2018,
  2. & (2018). Formal Verification for Feature-Based Composition of Workflows. , 173-181. Iasi (Romania): SERENE 2018:10th International Workshop on Software Engineering for Resilient Systems. doi:10.1109/EDCC.2018.00039
  3. & (2018). Undecidability of Equality for Codata Types. Presented at Coalgebraic Methods in Computer Science,-55. Thessaloniki, Greece: CMCS'18. doi:10.1007/978-3-030-00389-0_4
  4. & (2018). Declarative GUIs: Simple, Consistent, and Verified. Presented at PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming,, 1-15. Frankfurt/Main, Germany: Proceedings of PPDP 2018. doi:10.1145/3236950.3236962
  5. & (2016). Programming with monadic CSP-style processes in dependent type theory. Presented at TyDe 2016,, 28-38.ACM. doi:10.1145/2976022.2976032
  6. & (2014). Unnesting of Copatterns. Presented at Rewriting and Typed Lambda Calculi,, 31-45.Springer. doi:10.1007/978-3-319-08918-8_3
  7. & (2014). Verification of Solid State Interlocking Programs. Presented at Software Engineering and Formal Methods,-268. doi:10.1007/978-3-319-05032-4_19
  8. & (2013). Fibred Data Types. Presented at Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on,, 243-252. New Orleans: IEEE. doi:10.1109/LICS.2013.30
  9. & (2013). Copatterns: programming infinite structures by observations. Presented at Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages,(1), 27-38.ACM, New York, NY, USA. doi:10.1145/2429069.2429075
  10. & (2011). A Categorical Semantics for Inductive-Inductive Definitions. Presented at Algebra and Coalgebra in Computer Science. 4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings,, 70-84. Heidelberg: Springer. doi:10.1007/978-3-642-22944-2_6
  11. & (2009). Specifying railway interlocking systems. , 233-236.Swansea University.
  12. & (2006). Weak Bisimulation Approximants. Presented at Computer Science Logic,, 365 doi:10.1007/11874683_24