Ulrich Berger - Publications

2015

2014

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

Past Millennium

Recent papers and drafts, Some slides of recent talks.

Extracting verified decision procedures: DPLL and Resolution
Ulrich Berger, Andrew Lawrence, Fredrik Nordvall Forsberg, Monika Seisenberger
Logical Methods in Computer Science 11(1) , 2015.

Abstract

This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are correct by construction. To this end, we formalize a completeness proof for the DPLL proof system and extract a SAT solver from it. When applied to a propositional formula in conjunctive normal form the program produces either a satisfying assignment or a DPLL derivation showing its unsatisfiability. We use non-computational quantifiers to remove redundant computational content from the extracted program and translate it into Haskell to improve performance. We also prove the equivalence between the resolution proof system and the DPLL proof system with a bound on the size of the resulting resolution proof. This demonstrates that it is possible to capture quantitative information about the extracted program on the proof level. The formalization is carried out in the interactive proof assistant Minlog.

Bib entry 


@Article{BergerLawrenceNordvallForsbergSeisenberger15,
  author =     "Berger, U. and Lawrence, A. and Noprdvall Forsberg, F. and Seisenberger, M.",
  title =      "Extracting verified decision procedures: DPLL and Resolution",
  journal =    {Logical Methods in Computer Science},
  year =       "2015",
  volume =     "11",
  pages =      "1--18",
  doi =        "doi: 10.2168/LMCS-11(1:6)2015",
  note =       "\url|http://www.lmcs-online.org/ojs/viewarticle.php?id=1479|",
}

Online version at LMCS

Back

Uniform Schemata for Proof Rules
Ulrich Berger, Tie Hou
Lecture Notes in Computer Science 8493 , 2014.

Abstract

Motivated by the desire to facilitate the implementation of interactive proof systems with rich sets of proof rules, we present a uniform system of rule schemata to generate proof rules for different styles of logical calculi. The system requires only one schema for each logical operator to generate introduction and elimination rules in natural deduction and sequent calculus style. In addition, the system supports program extraction from proofs by generating realizers for the proof rules automatically.

Bib entry 


@article{BergerHou14,
  author = 	 "Berger, U. and Hou, T.",
  title = 	 "Uniform Schemata for Proof Rules",
  journal =      "Lecture Notes in Computer Science",
  volume =       "8493",
  pages =        "53--62 ",
  doi =        "doi: 10.1007/978-3-319-08019-2",
  note =       "\url|http://link.springer.com/chapter/10.1007/978-3-319-08019-2_6|",
  year =	 "2014"
}

Back

Extracting Imperative Programs from Proofs: In-place Quicksort
Ulrich Berger, Monika Seisenberger, Gregory Woods
LIPICS 26 , 2014.

Abstract

The process of program extraction is primarily associated with functional programs with less focus on imperative program extraction. In this paper we consider a standard problem for imperative programming: In-place Quicksort. We formalize a proof that every array of natural numbers can be sorted and apply a realizability interpretation to extract a program from the proof. Using monads we are able to exhibit the inherent imperative nature of the extracted program. We see this as a first step towards an automated extraction of imperative programs. The case study is carried out in the interactive proof assistant Minlog.

Bib entry 


@InProceedings{berger_et_al:LIPIcs:2014:4627,
  author =	{Ulrich Berger and Monika Seisenberger and Gregory J. M. Woods},
  title =	{{Extracting Imperative Programs from Proofs: In-place Quicksort}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{84--106},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Ralph Matthes and Aleksy Schubert},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4627},
  URN =		{urn:nbn:de:0030-drops-46274},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.TYPES.2013.84},
  annote =	{Keywords: Program Extraction, Verification, Realizability,
Imperative Programs, In-Place Quicksort, Computational Monads, Minlog}
}

Online version at DROPS

Back

Extracting a DPLL Algorithm
Andrew Lawrence, Ulrich Berger, Monika Seisenberger
Electronic Notes in Theoretical Computer Science , 2012.

Abstract

We formalize a completeness proof for the DPLL proof system and extract a DPLL SAT solver from it. When applied to a propositional formula in conjunctive normal form the program produces either a satisfying assignment or a DPLL derivation which shows that it is unsatisfiable. We use non-computational quantifiers to remove redundant computational content from the extracted program and improve its performance. The formalization is carried out in the Minlog system.

Bib entry 


@Article{LawrenceBergerSeisenberger12,
  author =     "Lawrence, A. and  Berger, U. and Seisenberger, M.",
  title =      "Extracting a DPLL Algorithm",
  journal =    {Electr.~Notes in Theor.~Comp.~Sci.},
  year =       "2012",
  volume =     "286",
  pages =      "243--256",
  doi =        "DOI: http://dx.doi.org/10.1016/j.entcs.2012.08.0160.216",
  note =       "\url|http://www.sciencedirect.com/science/article/pii/S1571066112000461|",
}

Online version at ENTCS

Back

Typed vs. Untyped realizability
Ulrich Berger, Tie Hou
Electronic Notes in Computer Science , 2012.

Abstract

We study the domain-theoretic semantics of a Church-style typed lambda-calculus with constructors, pattern matching and recursion, and show that it is closely related to the semantics of its untyped counterpart. The motivation for this study comes from program extraction from proofs via realizability where one has the choice of extracting typed or untyped terms from proofs. Our result shows that under a certain regularity condition, the choice is irrelevant. The regularity condition is that in every use of a fixed point type fix alpha.rho, alpha occurs only positively in rho.

Bib entry 


@Article{BergerHou12,
  author =     "Berger, U. and Hou, T.",
  title =      "Typed vs. Untyped realizability",
  journal =    {Electr.~Notes in Comp.~Sci.},
  year =       "2012",
  volume =     "286",
  pages =      "57--71",
  doi =        "doi:10.1016/j.entcs.2012.08.005",
  note =       "\url|http://www.sciencedirect.com/science/journal/15710661/286/supp/C|",
}

Online version at ENTCS

Back

Proofs, programs, processes
Ulrich Berger and Monika Seisenberger
Theory of Computing Systems 51(3) , 313-329 , 2012.

Abstract
The objective of this paper is to provide a theoretical foundation for program extraction from proofs. We give a realizability interpretation for first-order proofs involving inductive and coinductive definitions and discuss its application to the synthesis of provably correct programs. We show that realizers, although per-se untyped, can be assigned polymorphic recursive types and hence represent valid programs in a lazy functional programming language such as Haskell. Programs extracted from proofs using coinduction can be understood as perpetual processes producing infinite streams of data. Typical applications of such processes are computations in exact real arithmetic. As an example we show how to extract a program computing the average of two real numbers w.r.t.\ to the binary signed digit representation.

Bib entry 

@article{SeisenBerger12,
  author    = {Berger, U. and
               Seisenberger, M.},
  title     = {Proofs, programs, processes},
  journal   = {Theory of Computing Systems},
  url       = {http://link.springer.com/article/10.1007/s00224-011-9325-8}
  ee        = {DOI:10.1007/s00224-011-9325-8},
  volume    = {51},
  number    = {3},
  year      = {2012},
  pages     = {213-329}
}

Online version at TOCS

Back

From coinductive proofs to exact real arithmetic: theory and applications
Ulrich Berger
Logic Methods in Computer Science , 2011.

Abstract
Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with respect to the binary signed digit representation of real numbers. The data type corresponding to the coinductive definition of continuous functions consists of finitely branching non-wellfounded trees describing when the algorithm writes and reads digits. We discuss several examples including the extraction of programs for polynomials up to degree two and the definite integral of continuous maps.

Bib entry 


@Article{Berger11,
  author =     "U. Berger",
  title =      "From coinductive proofs to exact real arithmetic: theory and applications",
  journal =    {Logical Methods in Comput.~Sci.},
  year =       "2011",
  volume =     "7",
  number =     "1",
  pages =      "1--24",
  doi =        "DOI: 10.2168/LMCS-7(1:8)2011",
  note =       "\url|http://www.lmcs-online.org/ojs/viewarticle.php?id=704&layout=abstract|"
}

Online version at LMCS

Back

Minlog - A Tool for Program Extraction for Supporting Algebra and Coalgebra
Ulrich Berger, Kenji Miyamoto, Helmut Schwichtenberg, and Monika Seisenberger
Lecture Notes in Computer Science , 2011.

Abstract
Minlog is an interactive system which implements prooftheoretic methods and applies them to veri cation and program extraction. We give an overview of Minlog and demonstrate how it can be used to exploit the computational content in (co)algebraic proofs and to develop correct and ecient programs. We illustrate this by means of two examples: one about parsing, the other about exact real numbers in signed digit representation.

Bib entry 

@InProceedings{BergerMiyamotoSchwichtenbergSeisenberger11,
  author = 	 "Berger, U. and Miyamoto, K. and Schwichtenberg, H. and Seisenberger, M."
  title = 	 "Minlog - A Tool for Program Extraction for Supporting Algebra and Coalgebra",
  volume =	 "6859",
  series =	 "LNCS",
  pages =	 "393--399",
  booktitle =	 "CALCO-Tools",
  year =	 "2011",
  doi =          "Doi:10.1007/978-3-642-22944-2_29",
  publisher =	 "Springer-Verlag"
}

SpringerLink

Draft copy: [pdf]

Back

Realisability for Induction and Coinduction with Applications to Constructive Analysis
Ulrich Berger
Journal of Universal Computer Science , 2010.

Abstract
We prove the correctness of a formalised realisability interpretation of extensions of first-order theories by inductive and coinductive definitions in an untyped lambda-calculus with fixed-points. We illustrate the use of this interpretation for program extraction by some simple examples in the area of exact real number computation and hint at further non-trivial applications in computable analysis. This a revised end extended version of the paper "Realisability and adequacy for (co)induction" which appeared in the proceedings of CCA 2009.

Bib entry 


@Article{Berger10,
  author =     "U. Berger",
  title =      "Realisability for Induction and Coinduction with Applications to Constructive Analysis",
  abstract =   "We prove the correctness of a formalised realisability interpretation of extensions of first-order theories by inductive and coinductive definitions in an untyped λ-calculus with fixed-points. We illustrate the use of this interpretation for program extraction by some simple examples in the area of exact real number computation and hint at further non-trivial applications in computable analysis.",
  journal =    "Journal of Universal Computer Science",
  year =       "2010",
  volume =     "16",
  number =     "18",
  pages =      "2535--2555",
  month =      ,
  note =       "\url|http://www.jucs.org/jucs_16_18/realisability_for_induction_and|"
}

Online version at J. Univ. Comp.

Back

Domain Representations of Spaces of Compact Subsets
Ulrich Berger, Jens Blanck and Petter Kober
Mathematical Structures in Computer Science , 2010.

Abstract
We present a method for constructing from a given domain representation of a space X with underlying domain D, a domain representation of a subspace of compact subsets of X where the underlying domain is the Plotkin powerdomain of D. We show that this operation is functorial over a category of domain representations with a natural choice of morphisms. We study the topological properties of the space of representable compact sets and isolate conditions under which all compact subsets of X are representable. Special attention is paid to admissible representations and representations of metric spaces.

Bib entry 

@article{BergerBlanckKober10,
   AUTHOR = {Berger, U. and Blanck, J. and K{\o}ber, P.},
   TITLE = {Domain Representations of Spaces of Compact Subsets},
   JOURNAL = "Mathematical Structures in Computer Science",
   VOLUME = "20",
   PAGES = "107--126",
   YEAR = "2010",
   doi = "DOI:10.1017/S096012950999034X"
}

Online version at MSCS

Back

Proofs, programs, processes
Ulrich Berger and Monika Seisenberger
LNCS 6158 , 2010.

Abstract
We study a realisability interpretation for inductive and coinductive definitions and discuss its application to program extraction from proofs. A speciality of this interpretation is that realisers are given by terms that correspond directly to programs in a lazy functional programming language such as Haskell. Programs extracted from proofs using coinduction can be understood as perpetual processes producing infinite streams of data. Typical applications of such processes are computations in exact real arithmetic. As an example we show how to extract a program computing the average of two real numbers with respect to the binary signed digit representation.

Bib entry 

@inproceedings{SeisenBerger10,
  author    = {Berger, U. and
               Seisenberger, M.},
  title     = {Proofs, programs, processes},
  editor    = {F. Ferreira, B. Lowe, E. Mayordomo, L. M. Gomes},
  booktitle = {Programs, Proofs, Processes, 6th Conference on Computability
               in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, 
               June 30 - July 4, 2010. Proceedings},
  series    = {Lecture Notes in Computer Science},
  url       = {http://www.springerlink.com/content/g81ktw31q3683602/}
  ee        = {DOI: 10.1007/978-3-642-13962-8_5
  volume    = {6158},
  year      = {2010},
  pages     = {39-48},
}

SpringerLink

Draft copy: [pdf]

Back

From coinductive proofs to exact real arithmetic
Ulrich Berger
LNCS 5771 , 132-146, 2009.
DOI: 10.1007/978-3-642-04027-6_12

Abstract
We give a coinductive characterisation of the set of continuous functions defined on a compact real interval, and extract certified programs that construct and combine exact real number algorithms with respect to the binary signed digit representation of real numbers. The data type corresponding to the coinductive definition of continuous functions consists of finitely branching non-wellfounded trees describing when the algorithm writes and reads digits.

Bib entry 

@InProceedings{BergerCSL09,
  author = 	 "Berger, U.",
  title = 	 "From coinductive proofs to exact real arithmetic",
  editor =	 {E. Grädel and R. Kahle},
  volume =	 "5771",
  series =	 "LNCS",
  pages =	 "132--146",
  booktitle =	 "Computer Science Logic",
  year =	 "2009",
  doi = "DOI: 10.1007/978-3-642-04027-6_12"
  publisher =	 sv}

Draft copy: [pdf]

Back

Realisability and adequacy for (co)induction
Ulrich Berger
Proceedings of CCA 2009 , 2009.

Abstract
We prove the correctness of a formalised realisability interpretation of extensions of first-order theories by inductive and coinductive definitions in an untyped lambda-calculus with fixed-points. We illustrate the use of this interpretation for program extraction by some simple examples in the area of exact real number computation, and hint at further non-trivial applications in computable analysis.

Bib entry 

@InProceedings{BergerCCA09,
  author ={Berger, U.},
  title ={Realisability and Adequacy for (Co)induction},
  booktitle ={6th Int'l Conf. on Computability and Complexity in Analysis},
  year ={2009},
  editor ={Andrej Bauer and Peter Hertling and Ker-I Ko},
  publisher ={Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address ={Dagstuhl, Germany},
  URL ={http://drops.dagstuhl.de/opus/volltexte/2009/2258},
  annote ={Keywords: Constructive Analysis, realisability, program extraction, semantics},
}

Draft copy: [pdf]

Back

A domain model characterising strong normalisation
Ulrich Berger
Annals of Pure and Applied Logic 1841 2008.
DOI: 10.1016/j.apal.2008.06.005

Abstract
Building on previous work by Coquand and Spiwack we construct a strict domain-theoretic model for the untyped lambda-calculus with pattern matching and term rewriting which has the property that a term is strongly normalising if its value is not bottom. There are no disjointness or confluence conditions imposed on the rewrite rules, and under a mild but necessary condition completeness of the method is proven. As an application, we prove strong normalisation for barrecursion in higher types combined with polymorphism and non-deterministic choice. 

@article{Berger08,
  author = 	 "Berger, U.",
  title = 	 "A domain model characterising strong normalisation",
  journal =      "Annals of Pure and Applied Logic",
  volume =       "156",
  pages =        "39--50",
  year =	 "2008"
}

Draft copy: [pdf]

Back

Classical truth in higher types
Ulrich Berger
Mathematical Logic Quarterly 54 , 298-321, 2008.

Abstract
We study, from a classical point of view, how the truth of a statement about higher type functionals depends on the underlying model. The models considered are the classical set-theoretic finite type hierarchy and the constructively more meaningful models of continuous functionals, hereditarily effective operations, as well as the closed term model of Gödel's system T. The main results are characterisations of prenex classes for which truth in the full set-theoretic model transfers to truth in the other models. As a corollary we obtain that the axiom of choice is not conservative over Gödel's system T with classical logic for closed Sigma-2-formulas. We hope that this study will contribute to a clearer delineation and perception of constructive mathematics from a classical perspective. 

@Article{Berger08a,
  author = 	 {Berger, U.},
  title = 	 {Classical truth in higher types},
  journal = 	 mlq,
  year = 	 2008,
  volume =	 54,
  number =       3,
  pages =	 {240--246},
  doi =          "DOI: 10.1002/malq.200710046",
  url =          {http://onlinelibrary.wiley.com/doi/10.1002/malq.200710046/abstract}
}

Draft copy: [pdf]

Back

A Provably Correct Translation of the Lambda-Calculus into a Mathematical Model of C++
Rose H. Abdul Rauf, Ulrich Berger and Anton Setzer
Theory of Computing Systems 43 , 298-321, 2008.

Abstract
We introduce a translation of the simply typed lambda-calculus into C++, and give a mathematical proof of the correctness of this translation. For this purpose we develop a suitable fragment of C++ together with a denotational semantics. We introduce a formal translation of the lambda-calculus into this fragment, and show that this translation is correct with respect to the denotational semantics. We show as well a completeness result, namely that by translating lambda-terms we obtain essentially all C++ terms in this fragment. We introduce a mathematical model for the evaluation of programs of this fragment, and show that the evaluation computes the correct result with respect to this semantics. 

@article{AbdulRaufBergerSetzer08,
  author = 	 "Abdul Rauf, R. and Berger, U. and Setzer, A.",
  title = 	 "A Provably Correct Translation of the lambda-Calculus into a Mathematical Model of C++",
  journal =      "Theory of Computing Systems",
  volume =       "43",
  number =       "3-4"
  pages =        "298--321"
  doi =          "DOI: 10.1007/s00224-007-9062-1"
  year =	 "2008"
}

Draft copy: [pdf]

Back

Coinduction for Exact Real Number Computation
Ulrich Berger and Tie Hou
Theory of Computing Systems , 394-409, 2008.

Abstract
This paper studies coinductive representations of real numbers by signed digit streams and fast Cauchy sequences. It is shown how the associated coinductive principle can be used to give straightforward and easily implementable proofs of the equivalence of the two representations as well as the correctness of various corecursive exact real number algorithms. The basic framework is the classical theory of coinductive sets as greatest fixed points of monotone operators and hence is different from (though related to) the type theoretic approach by Ciaffaglione and Gianantonio. 

@article{BergerHou08,
  author = 	 "Berger, U. and Hou, T.",
  title = 	 "Coinduction for Exact Real Number Computation",
  journal =      "Theory of Computing Systems",
  volume =       "43",
  pages =        "394--409",
  doi =          "DOI: 10.1007/s00224-007-9017-6"
  year =	 "2008"
}

Draft copy: [pdf]

Back

Functional Concepts in C++
Rose H. Abdul Rauf, Ulrich Berger and Anton Setzer
Trends in Functional Programming. ,

Abstract
We describe a parser-translator program that translates typed lambda-terms into C++ classes so as to integrate functional concepts. We prove the correctness of the translation of lambda-terms into C++ with respect to a denotational semantics using Kripke-style logical relations. We introduce a general technique for introducing lazy evaluation into C++, and illustrate it by carrying out in C++ the example of computing the Fibonacci numbers efficiently using infinite streams and lazy evaluation. Finally, we show how merge higher-order lambda-terms with imperative C++ code. 

@article{AbdulRaufBergerSetzer07,
  author = 	 "Abdul Rauf, R. and Berger, U. and Setzer, A.",
  title = 	 "Functional Concepts in C++",
  journal =      "Trends in Functional Programming",
  note =         "to appear",
  volume =       "7",
  pages =        "163--179",
  year =	 "2007",
  note =         "ISBN 9781841501888"
}

Draft copy: [pdf]

Back

Program extraction from normalization proofs
Ulrich Berger, Stefan Berghofer, Pierre Letouzey and Helmut Schwichtenberg
Studia Logica 82 , 25-49, 2006.

Abstract
This paper describes formalizations of Tait's normalization proof for the simply typed lambda-calculus in the proof assistants Minlog, Coq and Isabelle/Hol. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting. 

@article{BergerBerghoferLetouzeySchwichtenberg06,
  author = 	 "Berger, U. and Berghofer, S. and Letouzey, P. and Schwichtenberg, H.",
  title = 	 "Program extraction from normalization proofs",
  journal =      "Studia Logica",
  volume =       "82",
  pages =        "25--49",
  year =	 "2006"
}

Draft copy: [pdf]

Back

Modified barrecursion
Ulrich Berger and Paulo Oliva
Mathematical Structures in Computer Science 16 , 163-183, 2006.

Abstract
This paper studies modified bar recursion, a higher type recursion scheme which has been used by Berardi, Bezem, Coquand and the authors for a realizability interpretation of classical analysis. A complete clarification of its relation to Spector's and Kohlenbach's bar recursion, the fan functional, Gandy's functional Gamma and Kleene's notion of S1-S9 computability is given. 

@article{BergerOliva06,
  author = 	 "Berger, U. and Oliva, P.",
  title = 	 "Modified Bar recursion",
  journal =      "Mathematical Structures in Computer Science",
  volume =       "16",
  pages =        "163--183",
  year =	 "2006"
}

Draft copy: [pdf]

Back

Applications of inductive definitions and choice principles to program synthesis
Ulrich Berger and Monika Seisenberger
In: Laura Crosilla and Peter Schuster, editors, From Sets and Types to Topology and Analysis Towards practicable foundations for constructive mathematics, Oxford Logic Guides, Volume 48, Oxford University Press, 137--148, 2005.

Abstract
We describe two methods of extracting constructive content from classical proofs, focusing on theorems involving infinite sequences and nonconstructive choice principles. The first method removes any reference to infinite sequences and transforms the theorem into a system of inductive definitions, the other applies a combination of Gödel's negative- and Friedman's A-translation. Both approaches are explained by means of a case study on Higman's Lemma and its well-known classical proof due to Nash-Williams. We also discuss some proof-theoretic optimizations that were crucial for the formalization and implementation of this work in the interactive proof system Minlog. 

@InCollection{BergerSeisenberger05,
Author = "Berger, U. and Seisenberger, M.",
Title  = "Applications of inductive definitions and choice principles
          to program synthesis", 
editors = "Laura Crosilla and Peter Schuster",
booktitle = "From Sets and Types to Topology and Analysis
             Towards practicable foundations for constructive mathematics",
series = "Oxford Logic Guides",
volume = 48,
publisher = "Oxford University Press",
pages = {137--148},
year =   2005
}

Back

Strong normalization for applied lambda calculi
Ulrich Berger
Logical Methods in Computer Science 1(2), 1--14, 2005.

Abstract
We consider the untyped lambda calculus with constructors and recursively defined constants. We construct a domain-theoretic model such that any term not denoting the bottom element is strongly normalising provided all its `stratified approximations' are. From this we derive a general normalisation theorem for applied typed lambda-calculi: If all constants have a total value, then all typeable terms are strongly normalising. We apply this result to extensions of Gödel's system T and system F extended by various forms of bar recursion for which strong normalisation was hitherto unknown. 

@Article{Berger05b,
  author = 	 {Berger, U.},
  title = 	 {Strong normalization for applied lambda calculi},
  journal = 	 {Logical Methods in Computer Science},
  year = 	 2005,
  volume =	 1(2),
  pages =	 {1--14}
}

Available at LMCS

Back

Continuous Semantics for Strong Normalization
Ulrich Berger
Lecture Notes in Computer Science 3526, 23--34, 2005.

Abstract
We prove a general strong normalization theorem for higher type rewrite systems based on Tait's strong computability predicates and a strictly continuous domain-theoretic semantics. The theorem applies to extensions of Gödel's system T, but also to various forms of bar recursion for which strong normalization was hitherto unknown. 

@InCollection{Berger05a,
   AUTHOR = {Berger, U.},
   TITLE = {Continuous Semantics for Strong Normalization},
   BOOKTITLE = {CiE 2005: New Computational Paradigms},
   SERIES =  {Lecture Notes in Computer Science},
   VOLUME = {3526},
   EDITOR = {Cooper, S.B. and Löwe, B. and Torenvliet, L.},
   PAGES = {23--34},
   YEAR = 2005
}

Draft copy: [pdf] [ps]

Back

Modified Bar Recursion and Classical Dependent Choice
Ulrich Berger and Paulo Oliva
Lecture Notes Logic 20, 89-107, 2005.

Abstract
We introduce a variant of Spector's bar recursion in finite types (which we call ``modified bar recursion'') to give a realizability interpretation of the classical axiom of dependent choice allowing for the extraction of witnesses from proofs of forall-exists-formulas in classical analysis. As another application, we show that the fan functional can be defined by modified bar recursion together with a version of bar recursion due to Kohlenbach. We also show that the type structure M of strongly majorizable functionals is a model for modified bar recursion. 

@InCollection{BO05,
  author = 	 "Berger, U. and Oliva, P.",
  title = 	 "Modified Bar recursion and classical dependent 
                  choice",
  booktitle =	 "Logic Colloquium '01, Proceedings of the Annual European Summer 
                 Meeting of the Association for Symbolic Logic, 
                 held in Vienna, Austria, August 6 - 11, 2001",
  series = {Lecture Notes in Logic},
  volume = {20},
  editor = {Baaz, M. and Friedman, S.D. and Kraijcek, J.}
  pages = {89--107},
  publisher = "Springer",
  year =	 "2005"
}

Draft copy: [pdf] [ps]

Back

Uniform Heyting Arithmetic
Ulrich Berger
Annals of Pure and Applied Logic 133, 125--148, 2005.

Abstract
We present an extension of Heyting Arithmetic in finite types called \emph{Uniform Heyting Arithmetic} that allows for the extraction of optimized programs from constructive and classical proofs. The system has two sorts of first-order quantifiers: ordinary quantifiers governed by the usual rules, and uniform quantifiers subject to stronger variable conditions expressing roughly that the quantified object is not computationally used in the proof. We combine a Kripke-style Friedman/Dragalin translation which is inspired by work of Coquand and Hofmann and a variant of the refined A-translation due to Buchholz, Schwichtenberg and the author to extract programs from a rather large class of classical first-order proofs while keeping explicit control over the levels of recursion and the decision procedures for predicates used in the extracted program. 

@article{Berger05c,
   AUTHOR = {Berger, U.},
   TITLE = "Uniform {H}eyting {A}rithmetic",
   JOURNAL = "{A}nnals of {P}ure and {A}pplied {L}ogic",
   VOLUME = "133",
   YEAR = "2005",
   PAGES = "125-148"
}

Draft copy: [pdf] [ps]

Back

A computational interpretation of open induction
Ulrich Berger
Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS), Turku, Finland, July 2004 , F Titsworth, editor, 326--334, IEEE Computer Society Press, 2004.

Abstract
We study the proof-theoretic and computational properties of open induction, a principle which is classically equivalent to Nash-Williams' minimal-bad-sequence argument and also to (countable) dependent choice (and hence contains full classical analysis). We show that, intuitionistically, open induction and dependent choice are quite different: Unlike dependent choice, open induction is closed under negative- and A-translation, and therefore proves the same Pi02-formulas (over not necessarily decidable, basic predicates) with classical or intuitionistic arithmetic. Via modified realizability we obtain a new direct method for extracting programs from classical proofs of Pi02-formulas using open induction. We also show that the computational interpretation of classical countable choice given by Berardi, Bezem and Coquand can be derived from our results. 

@Inproceedings{Berger04,
Author = "Ulrich Berger",
Title = "A computational interpretation of open induction",
Booktitle = "Proceedings of the Ninetenth Annual IEEE
            Symposium on Logic in Computer Science",
Editor = "F. Titsworth",
Pages = "326--334,
Publisher = "IEEE Computer Society",
Year = 2004}

Draft copy

Back

An arithmetic for non-size-increasing polynomial-time computation
Klaus Aehlig, Ulrich Berger, Martin Hofmann and Helmut Schwichtenberg
Theoretical Computer Science 318, 3-27, 2004

Abstract
An arithmetical system is presented with the property that from every proof a realizing term can be extracted that is definable in a certain affine linear typed variant of Gödel's system T and therefore defines a non-size-increasing polynomial time computable function. 

@article{AehligBergerHofmannSchwichtenberg04,
   AUTHOR = {Aehlig, K. and Berger, U. and Hofmann, M. and Schwichtenberg, H.},
   TITLE = {An arithmetic for non-size-increasing polynomial-time computation},
   JOURNAL = {Theoretical Computer Science},
   VOLUME = 318,
   PAGES = {3--27},
   YEAR = 2004
}

Draft copy: [pdf] [ps]

Back

Term rewriting for normalization by evaluation
Ulrich Berger, Matthias Eberl and Helmut Schwichtenberg
Information and Computation 183, 19--42, 2003.

Abstract
We extend normalization by evaluation from the pure types lambda-calculus to general higher-order rewrite systems. We distinguish between computational and proper rewrite rules, and define a domain theoretic model intended to explain why normalization by evaluation for the former is more efficient. Normalization by evaluation is proved to be correct w.r.t. this model. 

@Article{BergerEberlSchwichtenberg03a,
  author = 	 {Berger, U. and Eberl, M. and Schwichtenberg, H.},
  title = 	 {Term rewriting for normalization by evaluation},
  journal = 	 {Information and Computation},
  year = 	 2003,
  volume =	 183,
  pages =	 {19--42}
}

Draft copy

Back

Minimisation vs. recursion on the partial continuous functionals
Ulrich Berger
In the Scope of Logic, Methodology and Philosophy of Science 1 57--64,
Proceedings of the 11th International Congress of Logic, Methodology and Philosophy of Science (August 20-26, 1999), Synthese Library 316, Kluwer, 2002.

Abstract
We study the relationship between minimsation and recursion on the partial continuous functionals. We prove that already at type level two minimisation is weaker than recursion. 

@incollection{Berger02b,
   AUTHOR = {Berger, U.},
   TITLE = {Minimisation vs. recursion on the partial continuous functionals},
   BOOKTITLE = {In the Scope of Logic, Methodology and Philosophy of Science},
   EDITOR = {G\"ardenfors, P. and Wolenski, J. and Kijania-Placek, K.},
   VOLUME = 1,
   SERIES = {Synthese {L}ibrary 316},
   PAGES = {57--64},
   PUBLISHER = {Kluwer},
   YEAR = 2002
}

Draft copy

Back

Refined Program Extraction from Classical Proofs
Annals of Pure and Applied Logic 114 , 3-25, 2002
Ulrich Berger, Wilfried Buchholz and Helmut Schwichtenberg

Abstract
The paper develops a refinement of Gödel's negative- and Friedman's A-translation for classical arithmetic in finite types. The advantages of this refinment are twofold: (1) the negative-translation needs to be applied only partially, (2) the translation applies to an enrichment of arithmetic by free predicate symbols (without decidability assumptions) and axioms of a certain syntactical form (including Horn-formulas). (1) leads to simplified programs, (2) increases the applicability of the system since many notions and facts can be introduced axiomatically which means that proofs need only be partially formalized. 

@article{Berger02,
   AUTHOR = {Berger, U. and Buchholz, W. and Schwichtenberg, H.},
   TITLE = {Refined Program Extraction from Classical Proofs},
   JOURNAL = {Annals of Pure and Applied Logic},
   VOLUME = 114,
   PAGES = {3--25},
   year = 2002
}

Draft copy: [pdf] [ps]

Back

Computability and Totality in Domains
Ulrich Berger
Mathematical Structures in Computer Science 12 , 455--467, 2002.

Abstract
We survey the main results on computability and totality in Scott-Ershov-domains as well their applications to the theory of functionals of higher types and the semantics of functional programming languages. A new density theorem is proved and applied to to show the equivalence of the hereditarily computable total continuous functionals with the hereditarily effective operations over a large class of base types. 

@article{Berger02a,
   AUTHOR = {Berger, U.},
   TITLE = {Computability and Totality in Domains},
   JOURNAL = {Mathematical Structures in Computer Science},
   VOLUME = 12,
   PAGES = {455--467},
   YEAR = 2002
}

Draft copy

Back

Program extraction from Gentzen's proof of transfinite induction up to epsilon_0
Ulrich Berger
in: R. Kahle, P. Schroeder-Heister, R. Stärk, editors: Proof Theory in Computer Science, Lecture Notes in Computer Science 2183, 137--192, 2001.

Abstract
We discuss higher type constructions inherent to intuitionistic proofs. As an example we consider Gentzen's proof of transfinite induction up to the ordinal epsilon_0. From the constructive content of this proof we derive higher type algorithms for some ordinal recursive hierarchies of number theoretic functions as well as simple higher type primitive recursive definitions of tree ordinals of all heights epsilon_0.

Bibtex entry 

@InProceedings{Berger01a,
  author = 	 "Ulrich Berger",
  title = 	 "Program extraction from Gentzen's 
                  proof of transfinite induction up to epsilon_0",
  editor =	 "R. Kahle, P. Schroeder-Heister, R. St{\"a}rk",
  volume =	 "2138",
  series =	 "LNCS",
  pages =	 "68--77",
  booktitle =	 "Proof Theory in Computer Science",
  year =	 "2001",
  publisher =	 "Springer-Verlag"}

Draft copy

Implementation

Back

The Warshall Algorithm and Dickson's Lemma: Two Examples of Realistic Program Extraction +
Ulrich Berger, Helmut Schwichtenberg and Monika Seisenberger
Journal of Automated Reasoning 26 , 205--221, 2001

Abstract
By means of two well-known examples it is demonstrated that the method of extracting programs from proofs is manageable in practise and may yield efficient and sometimes unexpected programs. The Warshall algorithm computing the transitive closure of a relation is extracted from a constructive proof that repetitions in a path can always be avoided. Secondly, we extract a program from a classical (i.e. non constructive) proof of a special case of Dickson's Lemma, by transforming the classical proof into a constructive one. These techniques (as well as the examples) are implemented in the interactive theorem prover \Minlog\ developed at the University of Munich.

Bibtex entry 

@article{Berger01,
   AUTHOR = {Berger, U. and Schwichtenberg, H. and Seisenberger, M.},
   TITLE = {The {W}arshall Algorithm and {D}ickson's Lemma: Two examples 
            of realistic program extraction},
   JOURNAL = {Journal of Automated Reasoning},
   VOLUME = 26,
   YEAR = 2001
}

Draft copy

Back