Page 1 Next

Displaying 1 – 20 of 98

Showing per page

A Coalgebraic Semantics of Subtyping

Erik Poll (2010)

RAIRO - Theoretical Informatics and Applications

Coalgebras have been proposed as formal basis for the semantics of objects in the sense of object-oriented programming. This paper shows that this semantics provides a smooth interpretation for subtyping, a central notion in object-oriented programming. We show that different characterisations of behavioural subtyping found in the literature can conveniently be expressed in coalgebraic terms. We also investigate the subtle difference between behavioural subtyping and refinement.

A coalgebraic semantics of subtyping

Erik Poll (2001)

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

Coalgebras have been proposed as formal basis for the semantics of objects in the sense of object-oriented programming. This paper shows that this semantics provides a smooth interpretation for subtyping, a central notion in object-oriented programming. We show that different characterisations of behavioural subtyping found in the literature can conveniently be expressed in coalgebraic terms. We also investigate the subtle difference between behavioural subtyping and refinement.

A complete characterization of primitive recursive intensional behaviours

P. Valarcher (2008)

RAIRO - Theoretical Informatics and Applications

We give a complete characterization of the class of functions that are the intensional behaviours of primitive recursive (PR) algorithms. This class is the set of primitive recursive functions that have a null basic case of recursion. This result is obtained using the property of ultimate unarity and a geometrical approach of sequential functions on N the set of positive integers.

A Finite Axiomatization of Nondeterministic Regular Expressions

Flavio Corradini, Rocco De Nicola, Anna Labella (2010)

RAIRO - Theoretical Informatics and Applications

An alternative (tree-based) semantics for a class of regular expressions is proposed that assigns a central rôle to the + operator and thus to nondeterminism and nondeterministic choice. For the new semantics a consistent and complete axiomatization is obtained from the original axiomatization of regular expressions by Salomaa and by Kozen by dropping the idempotence law for + and the distribution law of • over +.

A non-uniform finitary relational semantics of system T

Lionel Vaux (2013)

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

We study iteration and recursion operators in the denotational semantics of typed λ-calculi derived from the multiset relational model of linear logic. Although these operators are defined as fixpoints of typed functionals, we prove them finitary in the sense of Ehrhard’s finiteness spaces.

A note on Coinduction and Weak Bisimilarity for While Programs

J. J.M.M. Rutten (2010)

RAIRO - Theoretical Informatics and Applications

An illustration of coinduction in terms of a notion of weak bisimilarity is presented. First, an operational semantics 𝒪 for while programs is defined in terms of a final automaton. It identifies any two programs that are weakly bisimilar, and induces in a canonical manner a compositional model 𝒟 . Next 𝒪 = 𝒟 is proved by coinduction.

A semantic construction of two-ary integers

Gabriele Ricci (2005)

Discussiones Mathematicae - General Algebra and Applications

To binary trees, two-ary integers are what usual integers are to natural numbers, seen as unary trees. We can represent two-ary integers as binary trees too, yet with leaves labelled by binary words and with a structural restriction. In a sense, they are simpler than the binary trees, they relativize. Hence, contrary to the extensions known from Arithmetic and Algebra, this integer extension does not make the starting objects more complex. We use a semantic construction to get this extension. This...

An abstract monadic semantics for value recursion

Eugenio Moggi, Amr Sabry (2010)

RAIRO - Theoretical Informatics and Applications

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

An abstract monadic semantics for value recursion

Eugenio Moggi, Amr Sabry (2004)

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

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

Coalgebras for binary methods : properties of bisimulations and invariants

Hendrik Tews (2001)

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

Coalgebras for endofunctors 𝒞 𝒞 can be used to model classes of object-oriented languages. However, binary methods do not fit directly into this approach. This paper proposes an extension of the coalgebraic framework, namely the use of extended polynomial functors 𝒞 o p × 𝒞 𝒞 . This extension allows the incorporation of binary methods into coalgebraic class specifications. The paper also discusses how to define bisimulation and invariants for coalgebras of extended polynomial functors and proves many standard...

Currently displaying 1 – 20 of 98

Page 1 Next