Publications

Journal Articles

  1. 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 154 61 88
  2. Berger, U., HOU, T. A realizability interpretation of Church's simple theory of types Mathematical Structures in Computer Science 1 22
  3. Berger, U., Spreen, D. A coinductive approach to computing with compact sets Journal of Logic and Analysis 8 3 1 35
  4. Berger, U., Jones, A., Seisenberger, M. Program extraction applied to monadic parsing Journal of Logic and Computation exv078
  5. Berger, U., Lawrence, A., Forsberg, F., Seisenberger, M. Extracting verified decision procedures: DPLL and Resolution Logical Methods in Computer Science 11 1
  6. Berger, U., Seisenberger, M., Woods, G. Extracting Imperative Programs from Proofs: In-place Quicksort Leibniz International Proceedings in Informatics (LIPIcs) 26 84 106
  7. Berger, U., Seisenberger, M. Proofs, Programs, Processes Theory of Computing Systems 51 3 313 329
  8. Berger, U., Hou, T. Typed vs. Untyped realizability Electronic Notes in Theoretical Computer Science 286 57 71
  9. Berger, U., Kahle, R. From coinductive proofs to exact real arithmetic: theory and applications Logical Methods in Computer Science 7 1
  10. Berger, U., Kahle, R. From coinductive proofs to exact real arithmetic: theory and applications Logical Methods in Computer Science 7 1
  11. Berger, U. From coinductive proofs to exact real arithmetic: theory and applications Logical Methods in Computer Science 7 1 8
  12. Berger, U., BLANCK, J., KØBER, P. Domain representations of spaces of compact subsets Mathematical Structures in Computer Science 20 02 107 126
  13. Berger, U., Blanck, J., KØBER, P. Domain representations of spaces of compact subsets Mathematical Structures in Computer Science 20 02 107
  14. Berger, U. Realisability for Induction and Coinduction with Applications to Constructive Analysis Journal of Universal Computer Science 16 18 2535 2555
  15. Berger, U., Sion, L. A coinductive approach to verified exact real number computation Electronic Communications of the EASST 23 15 pp.
  16. Berger, U., Hou, T. Coinduction for Exact Real Number Computation Theory of Computing Systems 43 3-4 394 408
  17. Abdul Rauf, R., Berger, U., Setzer, A. A Provably Correct Translation of the λ-Calculus into a Mathematical Model of C++ Theory of Computing Systems 43 3-4 298 321
  18. Berger, U. A domain model characterising strong normalisation Annals of Pure and Applied Logic 156 1 39 50
  19. Berger, U. Classical truth in higher types MLQ 54 3 240 246
  20. Berger, U., Escardó, M. Strong normalization for applied lambda calculi Logical Methods in Computer Science 1 2
  21. Berger, U. Uniform Heyting arithmetic Annals of Pure and Applied Logic 133 1-3 125
  22. Berger, U., Eberl, M., Schwichtenberg, H. Term rewriting for normalization by evaluation Information and Computation 183 1 19

Books

  1. Berger, U., Benton, D., Benton, D., Benton, D., Hall, K., Rhys, R. Realisability and adequacy for (co)induction Schloss Dagstuhl - Leibniz-Zentrum für Informatik

Book Chapters

  1. Berger, U. On the constructive and computational content of abstract mathematics (Ed.), Mathesis Universalis, Computability and Proof
  2. Berger, U., Miyamoto, K., Schwichtenberg, H., Tsuiki, H. Logic for Gray-code computation (Ed.), 69 Mouton, Oldenburg, China de Gruyter
  3. Berger, U., Seisenberger, M. Proofs, Programs, Processes (Ed.), Programs, Proofs, Processes 39 48 Berlin Springer
  4. Berger, U., Miyamoto, K., Schwichtenberg, H., Seisenberger, M. Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras (Ed.), Algebra and Coalgebra in Computer Science 393 399 Berlin-Heidelberg Springer
  5. Berger, U., Monika, S. Program extraction via typed realisability for induction and coinduction. (Ed.), Series in Mathematical Logic. 157 181 Frankfurt Ontos Verlag

Conference Contributions

  1. Berger, U., Petrovska, O. Optimized Program Extraction for Induction and Coinduction Sailing Routes in the World of Computation 10936 80
  2. Berger, U., Matthes, R., Setzer, A. Martin Hofmann’s case for non-strictly positive 1 data types 24th International Conference on Types for Proofs and Programs 130 1:1 1:22
  3. Berger, U., Matthes, R., Setzer, A. Martin Hofmann’s case for non-strictly positive data types Leibniz International Proceedings in Informatics, LIPIcs 130 1
  4. Berger, U., Setzer, A. Undecidability of Equality for Codata Types Coalgebraic Methods in Computer Science 11202 34 55
  5. Berger, U. Extracting nondeterministic concurrent programs Computer Science Logic 2016 62 26:1 26:21
  6. Berger, U., Hou, T. Uniform Schemata for Proof Rules Computability in Europe 2015 (CiE 2015) 8493 53 62
  7. Berger, U. Proofs-as-programs in computable analysis Electronic Communications of the EASST 23 5 pp.
  8. Berger, U. From Coinductive Proofs to Exact Real Arithmetic Computer Science Logic, Lecture Notes in Computer Science 5771 132
  9. Berger, U., Berger, U. A computational interpretation of open induction 326 334