Displaying similar documents to “An abstract monadic semantics for value recursion”

Encoding FIX in Object Calculi

Roy L. Crole (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We show that the type theory introduced by Crole and Pitts [3] can be encoded in variants of Abadi and Cardelli's object calculi. More precisely, we show that the type theory presented with judgements of both equality and operational reduction can be translated into object calculi, and the translation proved sound. The translations we give can be seen as using object calculi as a metalanguge within which can be represented; an analogy can be drawn with Martin Löf's Theory of Arities...

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...

Inf-datalog, Modal Logic and Complexities

Eugénie Foustoucos, Irène Guessarian (2007)

RAIRO - Theoretical Informatics and Applications

Similarity:

Inf-Datalog extends the usual least fixpoint semantics of Datalog with greatest fixpoint semantics: we defined inf-Datalog and characterized the expressive power of various fragments of inf-Datalog in [CITE]. In the present paper, we study the complexity of query evaluation on finite models for (various fragments of) inf-Datalog. We deduce a unified and elementary proof that global model-checking ( computing all nodes satisfying a formula in a given structure) has 1. quadratic...

Denotational aspects of untyped normalization by evaluation

Andrzej Filinski, Henning Korsholm Rohde (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We show that the standard normalization-by-evaluation construction for the simply-typed -calculus has a natural counterpart for the untyped -calculus, with the central type-indexed logical relation replaced by a “recursively defined” , in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal forms,...

On Core XPath with Inflationary Fixed Points

Loredana Afanasiev, Balder Ten Cate (2013)

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

Similarity:

We prove the undecidability of Core XPath 1.0 (CXP) [G. Gottlob and C. Koch, in IEEE CS Press (2002) 189–202.] extended with an operator. More specifically, we prove that the satisfiability problem of this language is undecidable. In fact, the fragment of CXP+IFP containing only the and axes is already undecidable.

A Note on Negative Tagging for Least Fixed-Point Formulae

Dilian Gurov, Bruce Kapron (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

Proof systems with sequents of the form ⊢ Φ for proving validity of a propositional modal -calculus formula Φ over a set of states in a given model usually handle fixed-point formulae through unfolding, thus allowing such formulae to reappear in a proof. Tagging is a technique originated by Winskel for annotating fixed-point formulae with information about the proof states at which these are unfolded. This information is used later in the proof to avoid unnecessary unfolding,...

Topologies, Continuity and Bisimulations

J. M. Davoren (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

The notion of a is of basic importance in many areas of computation theory and logic. Of late, it has come to take a particular significance in work on the formal analysis and verification of , where system properties are expressible by formulas of the modal -calculus or weaker temporal logics. Our purpose here is to give an analysis of the concept of bisimulation, starting with the observation that the zig-zag conditions are suggestive of some form of continuity. We give a topological...

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...

Call-by-value Solvability

Luca Paolini, Simona Ronchi Della Rocca (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

The notion of solvability in the call-by-value -calculus is defined and completely characterized, both from an operational and a logical point of view. The operational characterization is given through a reduction machine, performing the classical -reduction, according to an innermost strategy. In fact, it turns out that the call-by-value reduction rule is too weak for capturing the solvability property of terms. The logical characterization is given through an intersection type assignment...