Dr Anton Setzer
Computer Science
Telephone: (01792) 513368
Email: JavaScript is required to view this email address.
Room: Office - 952
First Floor
Talbot Building
Singleton Campus

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. & Formal Verification for Feature-based Composition of Workflows. Presented at Proceedings of SERENE 2018, Iasi (Romania): SERENE 2018.
  2. & Declarative GUIs: Simple, Consistent, and Verified. Presented at Declarative GUIs: Simple, Consistent, and Verified, Frankfurt/Main, Germany: Proceedings of PPDP 2018.
  3. & Undecidability of Equality for Codata Types. Presented at Proceedings of CMCS'18. To appear in LMCS., Thessaloniki, Greece: CMCS'18.
  4. & Defining Trace Semantics for CSP-Agda. In Proceedings of Types 2016. Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  5. & (2014). Unnesting of Copatterns. Presented at Rewriting and Typed Lambda Calculi,, 31-45.Springer. doi:10.1007/978-3-319-08918-8_3

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.


  • '''Application of Proof-theoretic Methods to Natural Language Processing''' (current)

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

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

    Student name:
    Other supervisor: Prof Markus Roggenbach