-пространства.
A coalgebraic semantics of subtyping
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
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
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
A Finite Axiomatization of Nondeterministic Regular Expressions
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
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
A note on Coinduction and Weak Bisimilarity for While Programs
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
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...
A simplification functor for coalgebras.
Algorithmically definable functions (A contribution towards the semantics of programming languages) [Book]
An abstract monadic semantics for value recursion
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
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 intensional approach to questions
An operational semantics for process algebra
Catégories lax-localement-cartésiennes et catégories localement cartésiennes : un exemple de suffisante complétude connexe de sémantiques initiales
Category-theoretic models of linear Abadi & Plotkin logic.
Closure operators on O-categories.
Coalgebras for binary methods : properties of bisimulations and invariants
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 . 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...