Dr Ulrich Berger
Reader
Computer Science
Telephone: (01792) 513380
Email: JavaScript is required to view this email address.
Room: Office - 337
Third Floor
Computational Foundry
Bay Campus

Publications

  1. Berger, U. On the constructive and computational content of abstract mathematics. Mathesis Universalis, Computability and Proof
  2. Berger, U., Matthes, R., & Setzer, A. Martin Hofmann’s case for non-strictly positive 1 data types. In 24th International Conference on Types for Proofs and Programs (pp. 1:1-1:22).
    http://drops.dagstuhl.de/opus/volltexte/2019/11405/
  3. Berger, U. & Petrovska, O. (n.d.) Optimized Program Extraction for Induction and Coinduction. In Sailing Routes in the World of Computation-80). Springer.
  4. Berger, U. Extracting nondeterministic concurrent programs. In Computer Science Logic 2016 (pp. 26:1-26:21).
    http://www.cs.swan.ac.uk/~csulrich/ftp/berger-csl16-revised.pdf
  5. Berger, U. & HOU, T. A realizability interpretation of Church's simple theory of types. Mathematical Structures in Computer Science, 1-22.
    http://www.cs.swan.ac.uk/~csulrich/ftp/berger_hou_march2016.pdf

See more...

Teaching

  • 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-M15 Directed studies in Logic and Computation

    Students will be assigned specific study topics associated with their intended research topic. They will be expected to undertake specialised individual study under the direction of their tutor. Both students and lecturers will give talks on project related topics. The student talks are assessed.

  • CSC375 Logic for Computer Science

    This module provides an introduction to logic and its applications to computer science, in particular to the formal specification and verification of computer programs.

  • CSC385 Modelling and Verification Techniques

    This module will give an overview of the landscape and the state of the art of current modelling and verification techniques. Students will gain hands-on experience in using a tool for modelling and verification.

  • CSCM75 Logic in Computer Science

    This module provides an in-depth introduction to logic and its applications to computer science, as a sound basis for the formal specification and verification of computer programs. Student will also learn how to use an interactive proof tool and carry out interactive proofs themselves.

  • CSCM85 Modelling and Verification Techniques

    This module will give an overview of the landscape and the state of the art of current modelling and verification techniques. One particular tool for software verification will be studied in depth. Students will gain hands-on experience in using that tool.

  • CSGM05 Directed Studies in Logic and Computation

    Students will be assigned specific study topics associated with their project topic. They will be expected to undertake specialised individual study under the direction of their tutor. Both students and lecturers will give talks on project related topics. The student talks are assessed.

Supervision

  • Enhanced realizability interpretation for extracting correct programs. (current)

    PhD
    Other supervisor: Dr Monika Seisenberger
  • Deep Encoding: Where Genetic Algorithms and Numeral Systems Meet (current)

    MRes
    Other supervisor: Dr Arno Pauly
  • Implementing Prawf with Program Extraction and Case Studies for Sequent Calculus Rules (current)

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

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

    PhD
    Other supervisor: Dr Anton Setzer
    Other supervisor: Dr Monika Seisenberger