4 results
Ulrich Berger ; Andrew Lawrence ; Fredrik Nordvall Forsberg ; Monika Seisenberger.
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 […]
Published on March 10, 2015
Ulrich Berger.
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 […]
Published on March 24, 2011
Ulrich Berger.
We consider the untyped lambda calculus with constructors and recursively defined constants. We construct a domain-theoretic model such that any term not denoting bottom is strongly normalising provided all its `stratified approximations' are. From this we derive a general normalisation theorem for […]
Published on October 5, 2005
Dieter Spreen ; Ulrich Berger.
Infinite Gray code has been introduced by Tsuiki as a redundancy-free representation of the reals. In applications the signed digit representation is mostly used which has maximal redundancy. Tsuiki presented a functional program converting signed digit code into infinite Gray code. Moreover, he […]
Published on July 6, 2023