3 citations · 8 across the 7 of their papers we have counts for
8 papers
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…
Projected images of the Sierpinski tetrahedron and other layered fractal imaginary cubes
Hideki Tsuiki
The Sierpinski tetrahedron has a remarkable property: It is projected to squares in three orthogonal directions, and moreover, to sets with positive Lebesgue measures in numerous d…
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…
Computable dyadic subbases and -representations of compact sets
Arno Pauly, Hideki Tsuiki
We explore representing the compact subsets of a given represented space by infinite sequences over Plotkin's . We show that computably compact computable metric spaces…
Domain Representations Induced by Dyadic Subbases
Hideki Tsuiki, Yasuyuki Tsukamoyo
We study domain representations induced by dyadic subbases and show that a proper dyadic subbase S of a second-countable regular space X induces an embedding of X in the set of min…
Every Separable Metrizable Space has a Proper Dyadic Subbase
Haruto Ohta, Hideki Tsuiki, Kohzo Yamada
The notions of a proper dyadic subbase and an independent subbase was introduced by H. Tsuiki to investigate in {0, 1, bot}-sequence codings of topological spaces. We show that eve…