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. & Higman’s Lemma and Its Computational Content. In Advances in Proof Theory. (pp. 353-375).
  2. & Towards Safety Analysis of ERTMS/ETCS Level 2 in Real-Time Maude. In Formal Techniques for Safety-Critical Systems. Springer.
  3. & Program extraction applied to monadic parsing. Journal of Logic and Computation, exv078
  4. & Extracting verified decision procedures: DPLL and Resolution. Logical Methods in Computer Science 11(1)
  5. & Verification of Solid State Interlocking Programs. In Counsell, Steve and Nunez, Manuel (Ed.), Software Engineering and Formal Methods. (pp. 253-268). Springer.

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.

  • CS-261 Coding for Lawyers

    This module provides an introduction to Computer programming and coding principles, tailored to students from Law. Students be able to apply those principles in practice to program development in Python and gain further insight in the typical design, structure and application of technical solutions. The module enables students majoring in Law to reach a level of skill in programming such that they will be able to apply their computing knowledge to their own subject.


  • 'Centrality Metrics Detection of Terrorist Networks.' (current)

    Student name:
    Other supervisor: Dr Daniel Archambault
  • Proof-theoretic Methods in Natural Language Processing (current)

    Student name:
    Other supervisor: Dr Ulrich Berger
    Other supervisor: Dr Anton Setzer
  • From Natural Language Proofs to Correct Programs. (current)

    Student name:
    Other supervisor: Dr Ulrich Berger