Fundamenta Informaticae - Volume 16, issue 2

Article Type: Other

DOI: 10.3233/FI-1992-16201

Citation: Fundamenta Informaticae, vol. 16, no. 2, pp. i-vii, 1992

Authors: Tarlecki, Andrzej

Article Type: Editorial

DOI: 10.3233/FI-1992-16202

Citation: Fundamenta Informaticae, vol. 16, no. 2, pp. 99-100, 1992

Authors: Astesiano, Egidio | Cerioli, Maura

Article Type: Research Article

Abstract: In this paper the classes of extensional models of higher-order partial conditional specifications are studied, with the emphasis on the closure properties of these classes. Further it is shown that any equationally complete inference system for partial conditional specifications may be extended to an inference system for partial higher-order conditional specifications, which is equationally complete w.r.t. the class of all extensional models. Then, applying some previous results, a deduction system is proposed, equationally complete for the class of extensional models of a partial conditional specification. Finally, turning the attention to the special important case of termextensional models, it is …first shown a sound and equationally complete inference system and then necessary and sufficient conditions are given for the existence of free models, which are also free in the class of term-generated extensional models. Show more

DOI: 10.3233/FI-1992-16203

Citation: Fundamenta Informaticae, vol. 16, no. 2, pp. 101-126, 1992

Authors: Hilken, Barney P. | Rydeheard, David E.

Article Type: Research Article

Abstract: This is an exercise in the description of programming languages as indexed categories. Type classes have been introduced into functional programming languages to provide a uniform framework for ‘overloading’. We establish a correspondence between type classes and comprehension schemata in categories. A coherence result allows us to describe subclasses and implicit conversions between types.

DOI: 10.3233/FI-1992-16204

Citation: Fundamenta Informaticae, vol. 16, no. 2, pp. 127-147, 1992

Authors: Egidi, Lavinia | Honsell, Furio | Ronchi Della Rocca, Simona

Article Type: Research Article

Abstract: The functional fragment of Landin’s ISWIM as implemented by the SECD machine is the paradigm of the procedural kernel of many programming languages. We investigate and compare operational, denotational and logical descriptions of the ISWIM-SECD system. Our goal is to illustrate how to derive from each of these descriptions logical tools for resoning about termination and equivalence of programs. First we show the correctness and incompleteness of the canonical denotational semantics. Then we give a fully abstract quotient semantics using a notion of applicative bisimulation. We discuss next a finitary logical description of the denotational semantics. This takes the form …of a call-by-value intersection type assignment system. Finally we study this type assignment system for its own sake and give a completeness result for it with respect to a natural notion of interpretation. Show more

DOI: 10.3233/FI-1992-16205

Citation: Fundamenta Informaticae, vol. 16, no. 2, pp. 149-169, 1992

Authors: Montanari, Ugo | Sassone, Vladimiro

Article Type: Research Article

Abstract: Weak Observational Congruence (woc) defined on CCS agents is not a bisimulation since it does not require two states reached by bisimilar computations of woc agents to be still woc, e.g. α.τ.β.nil and α.β.nil are woc but τ.β.nil and β.nil are not. This fact prevent us from characterizing CCS semantics (when τ is considered invisible) as a final algebra, since the semantic function would induce an equivalence over the agents that is both a congruence and a bisimulation. In the paper we introduce a new behavioural equivalence for CCS agents, which is the coarsest …among those bisimulations which are also congruences. We call it Dynamic Observational Congruence because it expresses a natural notion of equivalence for concurrent systems required to simulate each other in the presence of dynamic, i.e. run time, (re)configurations. We provide an algebraic characterization of Dynamic Congruence in terms of a universal property of finality. Furthermore we introduce Progressing Bisimulation, which forces processes to simulate each other performing explicit steps. We provide an algebraic characterization of it in terms of finality, two logical characterizations via modal logic in the style of HML and a complete axiomatization for finite agents (consisting of the axioms for Strong Observational Congruence and of two of the three Milner’s τ -laws). Finally, we prove that Dynamic Congruence and Progressing Bisimulation coincide for CCS agents. Show more

DOI: 10.3233/FI-1992-16206

Citation: Fundamenta Informaticae, vol. 16, no. 2, pp. 171-199, 1992