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. Berger, U., Matthes, R., Setzer, A. Martin Hofmann’s case for non-strictly positive data types Leibniz International Proceedings in Informatics, LIPIcs 130 1
  2. Setzer, A. An Upper Bound for the Proof Theoretic Strength of Martin-Löf Type Theory with W-type and one Universe (Ed.), Springer
  3. Adelsberger, S., Igried, B., Moser, M., Savenkov, V., Setzer, A. Formal Verification for Feature-Based Composition of Workflows 173 181
  4. Adelsberger, S., Setzer, A., Walkingshaw, E. Developing GUI Applications in a Verified Setting (Ed.), Dependable Software Engineering. Theories, Tools, and Applications 89 107 Beijing, China Dependable Software Engineering. Theories, Tools, and Applications 4th International Symposium, SETTA 2018
  5. Adelsberger, S., Setzer, A., Walkingshaw, E. Declarative GUIs: Simple, Consistent, and Verified PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming 1 15

See more...


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

    Other supervisor: Dr Arno Pauly
  • 'Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification.' (awarded 2018)

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

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

    Other supervisor: Prof Markus Roggenbach