Abstract We present a logical system CFP (Concurrent Fixed Point Logic) that supports the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by two propositional operators, $$B|_{A}$$ B | A (restriction, a strengthening of implication) and $${\mathbf {\downdownarrows }}(B)$$ ⇊ ( B ) (total concurrency). The source of the extraction are formal CFP proofs, the target is a lambda calculus with constructors and recursion extended by a constructor Amb (for McCarthy’s amb) which is interpreted operationally as globally angelic choice and is used to implement nondeterminism and concurrency. The correctness of extracted programs is proven via an intermediate domain-theoretic denotational semantics. We demonstrate the usefulness of our system by extracting a nondeterministic program that translates infinite Gray code into the signed digit representation. A noteworthy feature of our system is that the proof rules for restriction and concurrency involve variants of the classical law of excluded middle that would not be interpretable computationally without Amb.

Abstract This article outlines a proof-theoretic approach to developing correct and terminating monadic parsers. Using modified realizability, we extract formally verified and terminating programs from formal proofs. By extracting both primitive parsers and parser combinators, it is ensured that all complex parsers built from these are also correct, complete and terminating for any input. We demonstrate the viability of our approach by means of two case studies: we extract (i) a small arithmetic calculator and (ii) a non-deterministic natural language parser. The work is being carried out in the interactive proof system Minlog.

We give a realizability interpretation of an intuitionistic version of Church's Simple Theory of Types (CST) which can be viewed as a formalization of intuitionistic higher-order logic. Although definable in CST we include operators for monotone induction and coinduction and provide simple realizers for them. Realizers are formally represented in an untyped lambda–calculus with pairing and case-construct. The purpose of this interpretation is to provide a foundation for the extraction of verified programs from formal proofs as an alternative to type-theoretic systems. The advantages of our approach are that (a) induction and coinduction are not restricted to the strictly positive case, (b) abstract mathematical structures and results may be imported, (c) the formalization is technically simpler than in other systems, for example, regarding the definition of realizability, which is a simple syntactical substitution, and the treatment of nested and simultaneous (co)inductive definitions.

We introduce an extension of intuitionistic fixed point logic by a modal operator facilitating the extraction of non-deterministic concurrent programs from proofs. We apply this extension to program extraction in computable analysis, more precisely, to computing with Tsuiki's infinite Gray code for real numbers.

This special issue of Mathematical Structures in Computer Science is composed mainly of papers submitted by participants of the Dagstuhl Seminar on Computing with Infinite Data: Topological and Logical Foundations. The workshop took place in the Schloss Dagstuhl - Leibniz Center for Informatics in the first half of October 2011.

We present a method for constructing from a given domain representation of a spaceXwith underlying domainD, a domain representation of a subspace of compact subsets ofXwhere the underlying domain is the Plotkin powerdomain ofD. 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 ofXare representable. Special attention is paid to admissible representations and representations of metric spaces.

We prove a general strong normalisation 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 barrecursion for which strong normalisation was hitherto unknown.

This paper studies modified bar recursion, a higher type recursion scheme, which has been used in Berardi et al. (1998) and Berger and Oliva (2005) for a realisability interpretation of classical analysis. A complete clarification of its relation to Spector's and Kohlenbach's bar recursion, the fan functional, Gandy's functional and Kleene's notion of S1–S9 computability is given.

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 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\"odel's system T and system F extended by various forms of bar recursion for which strong normalisation was hitherto unknown.

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 /spl pi//sub 2//sup 0/-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 /spl pi//sub 2//sup 0/-formulas using open induction. We also show that the computational interpretation of classical countable choice given by S. Berardi et al. (1998) can be derived from our results.

We survey the main results on computability and totality in Scott–Eršov-domains as well as 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 show the equivalence of the hereditarily computable total continuous functionals with the hereditarily effective operations over a large class of base types.

A functional p to e (procedure to expression) that inverts the evaluation functional for typed lambda -terms in any model of typed lambda -calculus containing some basic arithmetic is defined. Combined with the evaluation functional, p to e yields an efficient normalization algorithm. The method is extended to lambda -calculi with constants and is used to normalize (the lambda -representations of) natural deduction proofs of (higher order) arithmetic. A consequence of theoretical interest is a strong completeness theorem for beta eta -reduction. If two lambda -terms have the same value in some model containing representations of the primitive recursive functions (of level 1) then they are probably equal in the beta eta -calculus.>