Domain-theoretic methods for program synthesis

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

Project Outline

Review

Publications

[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.

Drafts

[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.

Conferences/ Workshops

Dagstuhl, 7-12 October 2001
Conference: Proof Theory in Computer Science (01411)
Organizers: R Kahle, P Schröder-Heister, R Stärk (Zürich)
Talk: Programs from Proofs

Vienna, 6-11 August 2001
Conference: Logic Colloquium 2001
Organizer: M Baaz
Talk: Modified realizability for classical countable choice

Munich, 6 April 2002
Conference: Ein Bogen von der Beweistheorie zur Informatik
Organizers: U Berger, R Kahle, R Matthes

Oberwolfach, 7-14 April 2002
Conference: Mathematical Logic and Implicit Complexity
Organizers: Y Moschovakis, H Schwichtenberg, A S Troelstra, S S Wainer
Talk: Minimization vs General Recursion

Dagstuhl, 26-31 May 2002
Conference: Mathematical Structures for Computable Topology and Geometry (02221)
Organizers: R Kopperman, M B Smyth, D Spreen
Title: Bar Recursion on Continuous Functionals

Birmingham 2002, 12-14 September 2002
Conference: BLC Annual Meeting
Organizer: E Ritter
Talk: A Kripke-interpretation for a fragment of classical second-order logic

Birmingham 2002, 15-19 September 2002
Conference: Domains VI
Organizers: M Escardo, A Jung
Talk: Verification of a domain-theoretic algorithm using a non-constructive induction principle

Gothenberg, 14-15 November 2002
Conference: Workshop in Termination and Type Theory
Organizers: A Bove, T Coquand, P Dybjer, P Jansson, B Nordström, D Wahlstedt
Talk: Proving termination by update-induction

Edinburgh, 23 - 29 March 2003
Conference: Workshop on Proof Theory and Algorithms
Organizer: M Hyland, U Kohlenbach
Talk: A Kripke translation for classical proofs

Venice, 12-16 May 2003,
Conference: From Sets and Types to Topology and Analysis - Towards Practicable Foundations for Constructive Mathematics
Organizers: L Crosilla and P Schuster
Talk (M. Seisenberger): On the Constructive Content of Proofs

Dresden, 3-4 July 2003
Conference: PCC - Proof, Computation, Complexity
Organizers: B Elbl, R Kahle
Talk (M. Seisenberger): A-Translation of Higman's Lemma

Rome, 10-12 September 2003
Conference: Calculemus 2003
Organizers: T Hardin, R Rioboo
Talk: Inductive Definitions vs classical Choice in The Minlog System (with M Seisenberger)

Munich 1-2 November 2003
Conference: Domains Topology and Constructive Logic
Organizers: M Latte and D Scott
Talk: A domain-theoretic interpretation of open induction and countable choice

Marseille Luminy, 12-16 January 2004
Conference: Computer Algebra, Certified algorithms, Constructive proofs
Organizers: T Coquand, H Lombardi
Talk: A computational Interpretation of Open Induction

Venice San-Servolo, 5-8 April 2004
Conference: Spring School - Logic in Computer Science
Organizers: M Latte, H Schwichtenberg
Talk (M. Seisenberger): Hilbert's Basis Theorem and Gröbner Bases - A case for A-Translation?
Talk: Logical Relations and Complexity in Higher Types

Dresden, 17-19 June 2004
Conference: PCC - Proof, Computation, Complexity
Organizers: B Elbl, R Kahle
Talk: A Computational Interpretation of Classical Analysis

Turku, 13-17 July 2004
Conference: LICS 2004
Organizers: H Ganzinger, A Voronkov
Talk: A Computational Interpretation of Open Induction

Dagstuhl, 22-27 August 2004
Conference: Spatial Representation: Discrete vs. Continuous Computational Models (04351)
Organizers: R Kopperman, M B Smyth, D Spreen, J Webster
Talk: Continuous Semantics for Termination Proofs

Research Visits and Seminar Talks


Aarhus/Gothenberg June 2001
Organizer: U Kohlenbach
Talk: On the computational content of the axiom of choice

Swansea, 26 March 2002
Organizer: A Setzer
Talk: While-programs are Turing-incomplete for non-strict oracles

Nottingham, June 2002
Organizer: T Altenkirch
Talk: Modified Bar Recursion and Classical Dependent Choice

Munich, April - October 2002
Organizer: H Schwichtenberg
Research visit (M. Seisenberger)

Swansea, 11 July 2002
Organizer: A Setzer
Talk: A domain-theoretic realization of the classical axiom of countable choice

Munich, 1-23 August 2003
Organizer: H Schwichtenberg
Talk: A Kripke Interpretation for Classical Logic
Talk: A non-constructive induction principle for program verification

Munich, 10 July 2003
Organizer: H Schwichtenberg
Talk (M. Seisenberger): On the constructive content of proofs

Munich, 18-22 August 2003
Organizer: H Schwichtenberg
Research visit.


Ulrich Berger, Monika Seisenberger, August 2004