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. & Martin Hofmann’s case for non-strictly positive data types. Presented at Proceedings of Types 2018,
  2. An Upper Bound for the Proof Theoretic Strength of Martin-Löf Type Theory with W-type and one Universe. In Springer.
  3. & (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
  4. & 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.
  5. & (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

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, blockchain technology, and smart contracts.


  • First Steps Towards Computable Frame Theory (current)

    Student name:
    Other supervisor: Dr Arno Pauly
  • 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