Research Project funded by the
Engineering and Physical Sciences
Research Council
Grant GR/R16020/01
Duration: 23.4.01 - 22.4.04
Principal Investigator:
Ulrich Berger
Main Collaborator:
Monika Seisenberger
Department of Computer Science,
University of Wales Swansea
[P1] | U. Berger, W. Buchholz and H. Schwichtenberg, Refined Program Extraction from Classical Proofs, Annals of Pure and Applied Logic 114, 3-25, 2002. |
[P2] | M. Seisenberger, On the Constructive Content of Proofs, Ludwig-Maximilians-Universität München, Fakultät für Mathematik, Informatik und Statistik, 2003. |
[P3] | U. Berger, Uniform Heyting Arithmetic, Annals of Pure and Applied Logic, to appear. |
[P4] | U. Berger, A computational interpretation of open induction ,Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science (LICS), F Titsworth, editor, 326-334, IEEE Computer Society Press, 2004. |
[P5] | K. Aehlig, U. Berger, M. Hofmann and H. Schwichtenberg, An arithmetic for non-size-increasing polynomial-time computation Theoretical Computer Science 318, 3-27, 2004. |
[P6] | U. Berger and P. Oliva, Modified Bar Recursion and Classical Dependent Choice, In Logic Collocquium 2001, to appear. |
[P7] | U. Berger and M. Seisenberger, Applications of inductive definitions and choice principles to program synthesis. In L. Crosilla, P. Schuster, editors, Proceedings of the Workshop: From Sets and Types to Topology and Analysis - Towards Practicable Foundations for Constructive Mathematics, Venice International University, 12-16 May 2003, Oxford University Press, to appear. |
[D1] | U. Berger and P. Oliva, Modified bar recursion. |
[D2] | U. Berger, Strong normalization proofs based on continuous semantics. |
[D3] | U. Berger, Logical relations and feasibility in higher types. |