33 citations · 67 across the 9 of their papers we have counts for
10 papers
Uniform Realizability Interpretations
Ulrich Berger, Paulo Oliva
This work introduces a novel framework of uniform realizability that unifies and generalizes various realizability interpretations of logic, particularly focussing on the treatment…
Extracting total Amb programs from proofs
Ulrich Berger, Hideki Tsuiki
We present a logical system CFP (Concurrent Fixed Point Logic) supporting the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an…
Concurrent Gaussian elimination
Ulrich Berger, Monika Seisenberger, Dieter Spreen +1
Working in a semi-constructive logical system that supports the extraction of concurrent programs, we extract a program inverting non-singular real valued matrices from a construct…
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…
Extracting total Amb programs from proofs
Ulrich Berger, Hideki Tsuiki
We present a logical system CFP (Concurrent Fixed Point Logic) from whose proofs one can extract nondeterministic and concurrent programs that are provably total and correct with r…
Intuitionistic Fixed Point Logic
Ulrich Berger, Hideki Tsuiki
We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define…