Dr Anton Setzer
Computer Science
Telephone: (01792) 513368
Email: JavaScript is required to view this email address.

Areas of Expertise

  • interactive theorem proving
  • type theory
  • Martin-Loef Type Theory
  • Coinduction
  • Proof theory
  • dependently typed programming
  • ordinals
  • pattern matching
  • railway verification
  • security protocols
  • interactive programs
  • theoretical computer science
  • mathematical logic
  • logic for computer science
  • inductive-inductive definitions
  • inductive-inductive definitions
  • induction recursion
  • inductive recursive definition


  1. & (2014). Unnesting of Copatterns. Presented at Rewriting and Typed Lambda Calculi,, 31-45.Springer. doi:10.1007/978-3-319-08918-8_3
  2. & Interactive programming in Agda – Objects and graphical user interfaces. Journal of Functional Programming 27
  3. & (2016). Programming with monadic CSP-style processes in dependent type theory. Presented at TyDe 2016,, 28-38.ACM. doi:10.1145/2976022.2976032
  4. How to Reason Coinductively Informally. In Reinhard Kahle, Thomas Strahm, Thomas Studer (Ed.), Advances in Proof Theory. -408). Switzerland: Birkhäuser.
  5. & Trace and Stable Failures Semantics in CSP-Agda. In EPTCS post-proceedings of CoALP-Ty workshop.

See more...


  • CS-275 Automata and Formal Language Theory

    This module introduces the notion of grammars for defining the syntax of formal languages, especially programming languages. It introduces the limits of computation using Turing Machines and other models of computation.

  • CS-M25 Research Methodology and Project Specification

    In this modules students are introduced into the topic, the background and the aims of their project. They write a report on a talk related to their topic, a preliminary and a detailed specification which will be the basis of their research project. Guidance as to appropriate research methodologies in provided.

  • CSC313 High Integrity Systems

    This module introduces various techniques for developing high integrity systems.

  • CSCM10 Computer Science Project Research Methods

    This module will introduce students to some fundamental research methodologies and good practice in research. They will undertake background research including a literature review and specify the aims of their MSc project.

  • CSCM13 Critical Systems

    This module introduces techniques for developing critical systems, especially safety critical systems. Students will gain experience in applying modern tools in the development of critical software.


  • Proof-theoretic Methods in Natural Language Processing (current)

    Student name:
    Other supervisor: Dr Ulrich Berger
    Other supervisor: Dr Monika Seisenberger
  • Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification. (current)

    Student name:
    Other supervisor: Dr Ulrich Berger
  • 'Logic and Computation (Testing Software Product Lines)' (awarded 2017)

    Student name:
    Other supervisor: Prof Markus Roggenbach