Dr Monika Seisenberger
Associate Professor
Computer Science
Telephone: (01792) 602131
Email: JavaScript is required to view this email address.

Specialist areas: Formal methods: Program extraction, interactive theorem proving, specification and verification. Logic: proof theory, infinitary combinatorics, in particular well- and better quasiorderings.

Areas of Expertise

  • Formal Methods
  • Program extraction
  • Interactive theorem proving
  • Specification and Verification
  • Logic
  • Proof theory
  • Well- and better quasiorderings


  1. Morgan, J., Paiement, A., Williams, J., Wyner, A., Seisenberger, M. A Chatbot Framework for the Children’s Legal Centre Frontiers in Artificial Intelligence and Applications 205 209
  2. Berger, U., James, P., Lawrence, A., Roggenbach, M., Seisenberger, M. Verification of the European Rail Traffic Management System in Real-Time Maude Science of Computer Programming
  3. Berger, U., Jones, A., Seisenberger, M. Program extraction applied to monadic parsing Journal of Logic and Computation exv078
  4. James, P., Lawrence, A., Roggenbach, M., Seisenberger, M. Towards Safety Analysis of ERTMS/ETCS Level 2 in Real-Time Maude (Ed.), Formal Techniques for Safety-Critical Systems Springer
  5. Schwichtenberg, H., Seisenberger, M., Wiesnet, F. Higman’s Lemma and Its Computational Content (Ed.), Advances in Proof Theory 353 375

See more...


  • CS-081 Computational Problem Solving

    This module is a continuation of the module CSC061: Introduction to Programming. In it, students will continue to enhance their skills in programming, as well as gain a basic understanding of algorithms and data structures.

  • CS-205 Declarative Programming

    This module provides an introduction to the functional and logic programming paradigms and gives students the opportunity to gain practical experience in using both.


  • SAT solver in Haskell: proof of correctness and reduction of problems in NP class to SAT. (current)

    Other supervisor: Dr Arno Pauly
  • Formal Testing of ERTMS Level 2 (current)

    Other supervisor: Prof Markus Roggenbach
  • Enhanced realizability interpretation for extracting correct programs. (current)

    Other supervisor: Dr Ulrich Berger
  • Trustable Machine Learning Systems with Formal Methods (current)

    Other supervisor: Prof Jane Williams
  • Optimal Universal Solvers:«br /» Creating an optimal automated deduction system for First Order Logic (current)

    Other supervisor: Dr Oliver Kullmann
  • 'Centrality Metrics Detection of Terrorist Networks.' (awarded 2018)

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

    Other supervisor: Dr Anton Setzer
    Other supervisor: Dr Ulrich Berger