Trosolwg
Mae Dr Ulrich Berger yn Ddarllenydd yn yr Adran Gyfrifiadureg, Prifysgol Abertawe.
Dr Ulrich Berger
Darllenydd,
Computer Science
337
Trydydd Llawr
Y Ffowndri Gyfrifiadol
Campws y Bae
Trydydd Llawr
Y Ffowndri Gyfrifiadol
Campws y Bae
Ar gael ar gyfer Goruchwyliaeth Ôl-raddedig
Dolenni Ymchwil
Cyhoeddiadau
Uchafbwyntiau Ymchwil
-
Spreen, D. & Berger, U. (2023). Computing with Infinite Objects: the Gray Code Case. Logical Methods in Computer Science, 19(3)SU Repository: https://cronfa.swan.ac.uk/Record/cronfa65589
-
Berger, U., Seisenberger, M., Rathjen, M., & Schuster, P. (2023). Concurrent Gaussian Elimination. In Marco Benini, Olaf Beyersdorff, Michael Rathjen, Peter Schuster (Ed.), Mathematics for Computation (M4C) (pp. 223-250). WORLD SCIENTIFIC
-
Berger, U. & Tsuiki, H. (2022). Extracting total Amb programs from proofs. In Ilya Sergey (Ed.), Programming Languages and Systems (pp. 85-113). Springer International Publishing.
-
Petrovska, O., Berger, U., Petrovska, O., & Tsuiki, H. (2020). Prawf: An Interactive Proof System for Program Extraction. In Lecture Notes in Computer Science (pp. 137-148). Springer International Publishing.
-
Berger, U. & Seisenberger, M. (2023). On the Computational Content of Choice Principles. In Douglas Bridges Hajime Ishihara Michael Rathjen Helmut Schwichtenberg (Ed.), Handbook of Constructive Mathematics (pp. 806-825). Cambridge University Press
-
Berger, U. & Tsuiki, H. (2021). Intuitionistic fixed point logic. Annals of Pure and Applied Logic, 172(3), 102903
-
Berger, U., Blanck, J., & KØBER, P. (2010). Domain representations of spaces of compact subsets. Mathematical Structures in Computer Science, 20(02), 107
-
Abdul Rauf, R., Berger, U., & Setzer, A. (2008). A Provably Correct Translation of the λ-Calculus into a Mathematical Model of C++. Theory of Computing Systems, 43(3-4), 298-321.
-
Berger, U., Lawrence, A., Forsberg, F., & Seisenberger, M. (2015). Extracting verified decision procedures: DPLL and Resolution. Logical Methods in Computer Science, 11(1)
-
Berger, U., Jones, A., & Seisenberger, M. (2015). Program extraction applied to monadic parsing. Journal of Logic and Computation, exv078
Holl Ymchwil
Erthyglau Cylchgronau
-
Spreen, D. & Berger, U. (2023). Computing with Infinite Objects: the Gray Code Case. Logical Methods in Computer Science, 19(3)SU Repository: https://cronfa.swan.ac.uk/Record/cronfa65589
-
Berger, U. & Tsuiki, H. (2021). Intuitionistic fixed point logic. Annals of Pure and Applied Logic, 172(3), 102903
-
Berger, U., James, P., Lawrence, A., Roggenbach, M., & Seisenberger, M. (2018). Verification of the European Rail Traffic Management System in Real-Time Maude. Science of Computer Programming, 154, 61-88.
-
Berger, U. & HOU, T. (2017). A realizability interpretation of Church's simple theory of types. Mathematical Structures in Computer Science, 27(8), 1364-1385.
-
Berger, U. & Spreen, D. (2016). A coinductive approach to computing with compact sets. Journal of Logic and Analysis, 8(3), 1-35.
-
Berger, U., Jones, A., & Seisenberger, M. (2015). Program extraction applied to monadic parsing. Journal of Logic and Computation, exv078
-
Berger, U., Lawrence, A., Forsberg, F., & Seisenberger, M. (2015). Extracting verified decision procedures: DPLL and Resolution. Logical Methods in Computer Science, 11(1)
-
Berger, U., Seisenberger, M., & Woods, G. (2014). Extracting Imperative Programs from Proofs: In-place Quicksort. Leibniz International Proceedings in Informatics (LIPIcs), 26, 84-106.
-
Berger, U. & Seisenberger, M. (2012). Proofs, Programs, Processes. Theory of Computing Systems, 51(3), 313-329.
-
Berger, U. & Hou, T. (2012). Typed vs. Untyped realizability. Electronic Notes in Theoretical Computer Science, 286, 57-71.
-
Berger, U. & Kahle, R. (2011). From coinductive proofs to exact real arithmetic: theory and applications. Logical Methods in Computer Science, 7(1)
-
Berger, U. & Kahle, R. (2011). From coinductive proofs to exact real arithmetic: theory and applications. Logical Methods in Computer Science, 7(1)
-
Berger, U. (2011). From coinductive proofs to exact real arithmetic: theory and applications. Logical Methods in Computer Science, 7(1), 8
-
Berger, U., Blanck, J., & KØBER, P. (2010). Domain representations of spaces of compact subsets. Mathematical Structures in Computer Science, 20(02), 107
-
Berger, U., BLANCK, J., & KØBER, P. (2010). Domain representations of spaces of compact subsets. Mathematical Structures in Computer Science, 20(02), 107-126.
-
Berger, U. (2010). Realisability for Induction and Coinduction with Applications to Constructive Analysis. Journal of Universal Computer Science, 16(18), 2535-2555.
-
Berger, U. & Sion, L. (2009). A coinductive approach to verified exact real number computation. Electronic Communications of the EASST, 23, 15 pp.SU Repository: https://cronfa.swan.ac.uk/Record/cronfa42
-
Abdul Rauf, R., Berger, U., & Setzer, A. (2008). A Provably Correct Translation of the λ-Calculus into a Mathematical Model of C++. Theory of Computing Systems, 43(3-4), 298-321.
-
Berger, U. & Hou, T. (2008). Coinduction for Exact Real Number Computation. Theory of Computing Systems, 43(3-4), 394-408.
-
Berger, U. (2008). A domain model characterising strong normalisation. Annals of Pure and Applied Logic, 156(1), 39-50.
-
Berger, U. (2008). Classical truth in higher types. MLQ, 54(3), 240-246.
-
Berger, U. & Escardó, M. (2005). Strong normalization for applied lambda calculi. Logical Methods in Computer Science, 1(2)
-
Berger, U. (2005). Uniform Heyting arithmetic. Annals of Pure and Applied Logic, 133(1-3), 125
-
Berger, U., Eberl, M., & Schwichtenberg, H. (2003). Term rewriting for normalization by evaluation. Information and Computation, 183(1), 19
Llyfrau Awdurol
-
Berger, U., Benton, D., Benton, D., Benton, D., Hall, K., & Rhys, R. (2009). Realisability and adequacy for (co)induction Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
Penodau Llyfrau
-
Berger, U. & Seisenberger, M. (2023). On the Computational Content of Choice Principles. In Douglas Bridges Hajime Ishihara Michael Rathjen Helmut Schwichtenberg (Ed.), Handbook of Constructive Mathematics (pp. 806-825). Cambridge University Press
-
Berger, U., Seisenberger, M., Rathjen, M., & Schuster, P. (2023). Concurrent Gaussian Elimination. In Marco Benini, Olaf Beyersdorff, Michael Rathjen, Peter Schuster (Ed.), Mathematics for Computation (M4C) (pp. 223-250). WORLD SCIENTIFIC
-
Berger, U. (2019). On the constructive and computational content of abstract mathematics. Mathesis Universalis, Computability and ProofSU Repository: https://cronfa.swan.ac.uk/Record/cronfa50301
-
Berger, U. & Petrovska, O. (2018). Optimized Program Extraction for Induction and Coinduction. Sailing Routes in the World of Computation (pp. 70-80). Springer International Publishing
-
Berger, U., Miyamoto, K., Schwichtenberg, H., & Tsuiki, H. (2016). Logic for Gray-code computation. (pp. 69de Gruyter
-
Berger, U., Miyamoto, K., Schwichtenberg, H., & Seisenberger, M. (2011). Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras. Algebra and Coalgebra in Computer Science (pp. 393-399). Springer
-
Berger, U. & Seisenberger, M. (2010). Proofs, Programs, Processes. Programs, Proofs, Processes (pp. 39-48). Springer
-
Berger, U. & Monika, S. (2010). Program extraction via typed realisability for induction and coinduction.. Series in Mathematical Logic. (pp. 157-181). Ontos VerlagSU Repository: https://cronfa.swan.ac.uk/Record/cronfa8008
Cyfraniadau Cynadleddau
-
Berger, U. & Tsuiki, H. (2022). Extracting total Amb programs from proofs. In Ilya Sergey (Ed.), Programming Languages and Systems (pp. 85-113). Springer International Publishing.
-
Petrovska, O., Berger, U., Petrovska, O., & Tsuiki, H. (2020). Prawf: An Interactive Proof System for Program Extraction. In Lecture Notes in Computer Science (pp. 137-148). Springer International Publishing.
-
Berger, U., Matthes, R., & Setzer, A. (2019). Martin Hofmann’s case for non-strictly positive data types. In Leibniz International Proceedings in Informatics, LIPIcs
-
Berger, U., Matthes, R., & Setzer, A. (2019). 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).
-
Berger, U. & Setzer, A. (2018). Undecidability of Equality for Codata Types. In Coalgebraic Methods in Computer Science (pp. 34-55). Springer International Publishing.
-
Berger, U. (2016). Extracting nondeterministic concurrent programs. In Editors: Jean-Marc Talbot and Laurent Regnier (Ed.), 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). (pp. 26:1-26:21). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
-
Berger, U. & Hou, T. (2014). Uniform Schemata for Proof Rules. In Computability in Europe 2015 (CiE 2015) (pp. 53-62). Springer.
-
Berger, U. (2009). Proofs-as-programs in computable analysis. In Electronic Communications of the EASST (pp. 5 pp.SU Repository: https://cronfa.swan.ac.uk/Record/cronfa50
-
Berger, U. (2009). From Coinductive Proofs to Exact Real Arithmetic. In Computer Science Logic, Lecture Notes in Computer Science (pp. 132Springer.
-
Berger, U. & Berger, U. (2004). A computational interpretation of open induction. (pp. 326-334).
Goruchwyliaeth
-
Mind the Gap: Representation and Reasoning for Autonomous Vehicles (cyfredol)
PhDGoruchwyliwr arall: Dr Adam Wyner -
Automated Verification of Dynamical Systems over Continuous Data (cyfredol)
PhDGoruchwyliwr arall: Dr Eike Neumann -
Deep Encoding: Where Genetic Algorithms and Numeral Systems Meet (dyfarnwyd 2022)
MResGoruchwyliwr arall: Dr Arno Pauly
Modiwlau a Addysgir
-
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.
-
CS-M20 MSc Project
This module will provide students with the opportunity of exploring a particular topic in computer science in some considerable depth. It is only open to students studying MSc Computer Science, MSc Advanced Computer Science, MSc Advanced Software Technology, MSc in High Performance and Scientific Computing, and MSc Data Science.
-
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.