Search

• < Previous
• 1
• Next >

---

Extracting verified decision procedures: DPLL and Resolution

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&nbsp;[&hellip;]

---

From coinductive proofs to exact real arithmetic: theory and applications

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&nbsp;[&hellip;]

---

Strong normalisation for applied lambda calculi

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&nbsp;[&hellip;]

---

Computing with Infinite Objects: the Gray Code Case

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&nbsp;[&hellip;]

---