The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
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.
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.
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.
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 +.
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.
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.
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...
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,...
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,...
Currently displaying 1 –
15 of
15