Dr Anton Setzer
Computer Science
Telephone: (01792) 513368
Email: JavaScript is required to view this email address.
Room: Office - 403
Fourth Floor
Computational Foundry
Bay 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:10th International Workshop on Software Engineering for Resilient Systems.
  2. & (2018). Declarative GUIs. 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
  3. & 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.
  4. & Undecidability of Equality for Codata Types. Presented at Proceedings of CMCS'18. To appear in LMCS., Thessaloniki, Greece: CMCS'18.
  5. & Defining Trace Semantics for CSP-Agda. In Proceedings of Types 2016. Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.

See more...


  • 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.

  • CSCM29 Blockchain, Cryptocurrencies and Smart Contracts

    This is a module on modern blockchain technology and its major applications. It will give an overview on the technological setup of major cryptocurrencies, and introduce the blockchain as a concept for determining the order of events in a distributed database. In addition, it will discuss the implementation of smart contracts and summarise the current state of the art of security issues in cryptocurrencies, the blockchain, and smart contracts.


  • Untitled (current)

    Student name:
    Other supervisor: Prof Arnold Beckmann
  • 'Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification.' (awarded 2018)

    Student name:
    Other supervisor: Dr Ulrich Berger
  • '''Application of Proof-theoretic Methods to Natural Language Processing''' (awarded 2018)

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

    Student name:
    Other supervisor: Prof Markus Roggenbach