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
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|", }Back
Uniform Schemata for Proof Rules
Ulrich Berger, Tie Hou
Lecture Notes in Computer Science 8493
,
2014.
Abstract
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
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} }Back
Extracting a DPLL Algorithm
Andrew Lawrence, Ulrich Berger, Monika Seisenberger
Electronic Notes in Theoretical Computer Science
,
2012.
Abstract
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|", }Back
Typed vs. Untyped realizability
Ulrich Berger, Tie Hou
Electronic Notes in Computer Science
,
2012.
Abstract
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|", }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} }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|" }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 verication 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" }
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" }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}, }
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 }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" }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" }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}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 }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} }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 }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 }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 }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"}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 }Back