Displaying similar documents to “Semantics of value recursion for Monadic Input/Output”

Idealized coinductive type systems for imperative object-oriented programs

Davide Ancona, Giovanni Lagorio (2011)

RAIRO - Theoretical Informatics and Applications

Similarity:

In recent work we have proposed a novel approach to define idealized type systems for object-oriented languages, based on of programs into Horn formulas which are interpreted w.r.t. the coinductive (that is, the greatest) Herbrand model. In this paper we investigate how this approach can be applied also in the presence of imperative features. This is made possible by considering a natural translation of intermediate form programs into Horn formulas, where functions correspond to...

On Existentially First-Order Definable Languages and Their Relation to NP

Bernd Borchert, Dietrich Kuske, Frank Stephan (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

Under the assumption that the Polynomial-Time Hierarchy does not collapse we show for a regular language : the unbalanced polynomial-time leaf language class determined by equals  iff is existentially but not quantifierfree definable in FO[<, min, max, +1, −1]. Furthermore, no such class lies properly between NP and co-1-NP or NP⊕co-NP. The proofs rely on a result of Pin and Weil characterizing the automata of existentially first-order definable languages.

Wadge Degrees of -Languages of Deterministic Turing Machines

Victor Selivanov (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We describe Wadge degrees of -languages recognizable by deterministic Turing machines. In particular, it is shown that the ordinal corresponding to these degrees is where is the first non-recursive ordinal known as the Church–Kleene ordinal. This answers a question raised in [2].

Idealized coinductive type systems for imperative object-oriented programs

Davide Ancona, Giovanni Lagorio (2011)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

In recent work we have proposed a novel approach to define idealized type systems for object-oriented languages, based on of programs into Horn formulas which are interpreted w.r.t. the coinductive (that is, the greatest) Herbrand model. In this paper we investigate how this approach can be applied also in the presence of imperative features. This is made possible by considering a natural translation of intermediate form programs into Horn formulas, where functions correspond to union...

On biautomata

Ondřej Klíma, Libor Polák (2012)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

We initiate the theory and applications of biautomata. A biautomaton can read a word alternately from the left and from the right. We assign to each regular language its canonical biautomaton. This structure plays, among all biautomata recognizing the language , the same role as the minimal deterministic automaton has among all deterministic automata recognizing the language . We expect that from the graph structure of this automaton one could decide the membership of a given language...

An abstract monadic semantics for value recursion

Eugenio Moggi, Amr Sabry (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our technique for combining value recursion with computational effects works for all monads. The operational nature of our approach is related to the implementation of recursion in Scheme and its monadic version proposed by Friedman and Sabry, but it defines a different semantics and does not rely on assignments. When contrasted to the axiomatic approach proposed by Erkök and Launchbury,...

On differentiation functions, structure functions, and related languages of context-free grammars

Jürgen Dassow, Victor Mitrana, Gheorghe Păun, Ralf Stiebe (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We introduce the notion of a differentiation function of a context-free grammar which gives the number of terminal words that can be derived in a certain number of steps. A grammar is called narrow (or -narrow) iff its differentiation function is bounded by a constant (by ). We present the basic properties of differentiation functions, especially we relate them to structure function of context-free languages and narrow grammars to slender languages. We discuss the decidability...

k-counting automata

Joël Allred, Ulrich Ultes-Nitsche (2012)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

In this paper, we define -counting automata as recognizers for -languages, languages of infinite words. We prove that the class of -languages they recognize is a proper extension of the -regular languages. In addition we prove that languages recognized by -counting automata are closed under Boolean operations. It remains an open problem whether or not emptiness is decidable for -counting automata. However, we conjecture strongly that it is decidable and give formal reasons why we believe...

On global induction mechanisms in a -calculus with explicit approximations

Christoph Sprenger, Mads Dam (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We investigate a Gentzen-style proof system for the first-order -calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with...

Distributed Objects for Parallel Numerical Applications

Francoise Baude, Denis Caromel, David Sagnol (2010)

ESAIM: Mathematical Modelling and Numerical Analysis

Similarity:

The language (pronounced ) was designed and implemented with the aim of importing into parallel and concurrent programming, in the framework of a model. From a reduced set of rather simple primitives, comprehensive and versatile libraries are defined. In the absence of any syntactical extension, the user writes standard code. The libraries are themselves extensible by the final users, making an open system. Two specific techniques to improve performances of a...