Publications

Journal Articles

  1. Berger, U. Martin Hofmann’s case for non-strictly positive 1 data types LIPICS
  2. Berger, U., Seisenberger, M., Roggenbach, M., James, P. Verification of the European Rail Traffic Management System in Real-Time Maude Science of Computer Programming
  3. Berger, U. A coinductive approach to computing with compact sets Journal of Logic and Analysis
  4. Berger, U. A realizability interpretation of Church's simple theory of types Mathematical Structures in Computer Science 1 22
  5. Berger, U., Seisenberger, M. Program extraction applied to monadic parsing Journal of Logic and Computation exv078
  6. Berger, U., Seisenberger, M. Extracting verified decision procedures: DPLL and Resolution Logical Methods in Computer Science 11 1
  7. Berger, U. Extracting Imperative Programs from Proofs: In-place Quicksort Leibniz International Proceedings in Informatics (LIPIcs) 26 84 106
  8. Berger, U., Seisenberger, M. Proofs, Programs, Processes Theory of Computing Systems 51 3 313 329
  9. Berger, U. Typed vs. Untyped realizability Electronic Notes in Theoretical Computer Science 286 57 71
  10. Berger, U. From coinductive proofs to exact real arithmetic: theory and applications Logical Methods in Computer Science 7 1 8
  11. Berger, U., Kahle, R. From coinductive proofs to exact real arithmetic: theory and applications Logical Methods in Computer Science 7 1
  12. Berger, U., Kahle, R. From coinductive proofs to exact real arithmetic: theory and applications Logical Methods in Computer Science 7 1
  13. Berger, U. Realisability for Induction and Coinduction with Applications to Constructive Analysis Journal of Universal Computer Science 16 18 2535 2555
  14. BERGER, U., BLANCK, J., KØBER, P. Domain representations of spaces of compact subsets Mathematical Structures in Computer Science 20 02 107 126
  15. KØBER, P., BLANCK, J., BERGER, U. Domain representations of spaces of compact subsets Mathematical Structures in Computer Science 20 02 107
  16. Berger, U., , ., , . A coinductive approach to verified exact real number computation Electronic Communications of the EASST 23 15 pp.
  17. 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., Hou, T. Coinduction for Exact Real Number Computation Theory of Computing Systems 43 3-4 394 408
  21. Berger, U., Escardó, M. Strong normalization for applied lambda calculi Logical Methods in Computer Science 1 2
  22. Berger, U. Uniform Heyting arithmetic Annals of Pure and Applied Logic 133 1-3 125
  23. 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. 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., , ., , . Program extraction via typed realisability for induction and coinduction. (Ed.), Series in Mathematical Logic. 157 181 Frankfurt Ontos Verlag

Conference Contributions

  1. Berger, U. Optimized Program Extraction for Induction and Coinduction Sailing Routes in the World of Computation 10936 80
  2. Berger, U., Setzer, A. Undecidability of Equality for Codata Types Coalgebraic Methods in Computer Science 11202 55
  3. Berger, U. Extracting nondeterministic concurrent programs Computer Science Logic 2016
  4. Berger, U. Uniform Schemata for Proof Rules Computability in Europe 2015 (CiE 2015) 8493 53 62
  5. Berger, U. Proofs-as-programs in computable analysis Electronic Communications of the EASST 23 5 pp.
  6. Berger, U. From Coinductive Proofs to Exact Real Arithmetic Computer Science Logic, Lecture Notes in Computer Science 5771 132
  7. Berger, U. A computational interpretation of open induction 326 334