Fundamenta Informaticae - Volume 130, issue 1

Authors: Müller, Berndt | Fitting, Melvin

Article Type: Other

DOI: 10.3233/FI-2014-979

Citation: Fundamenta Informaticae, vol. 130, no. 1, pp. v-v, 2014

Authors: Baier, Christel | Klein, Joachim | Klüppelholz, Sascha

Article Type: Research Article

Abstract: In controller synthesis, i.e., the question whether there is a controller or strategy to achieve some objective in a given system, the controller is often realized as some kind of automaton. In the context of the exogenous coordination language Reo, where the coordination glue code between the components is realized as a network of channels, it is desirable for such synthesized controllers to also take the form of a Reo connector built from a repertoire of basic channels. In this paper, we address the automatic construction of such Reo connectors directly from a constraint automaton representation.

DOI: 10.3233/FI-2014-980

Citation: Fundamenta Informaticae, vol. 130, no. 1, pp. 1-20, 2014

Authors: Bellin, Gianluigi | Menti, Alessandro

Article Type: Research Article

Abstract: We reconsider work by Bellin and Scott in the 1990s on R. Milner and S. Abramsky's encoding of linear logic in the π-calculus and give an account of efforts to establish a tight connection between the structure of proofs and of the cut elimination process in multiplicative linear logic, on one hand, and the input-output behaviour of the processes that represent them, on the other, resulting in a proof-theoretic account of (a variant of) Chu's construction. But Milner's encoding of the linear lambda calculus suggests consideration of multiplicative co-intuitionistic linear logic: we provide a term assignment for it, a calculus …of coroutines which presents features of concurrent and distributed computing. Finally, as a test case of its adequacy as a logic for distributed computation, we represent our term assignment as a λP system. We argue that translations of typed functional languages in concurrent and distributed systems (such as π-calculi or λP systems) are best typed with co-intuitionistic logic, where some features of computations match the logical properties in a natural way. Show more

DOI: 10.3233/FI-2014-981

Citation: Fundamenta Informaticae, vol. 130, no. 1, pp. 21-65, 2014

Authors: Cervesato, Iliano | Sans, Thierry

Article Type: Research Article

Abstract: This paper introduces an abstract web programming language, QWeSST, and a methodology for proving properties of formalisms, such are QWeSST, that are parallel, distributed and concurrent. At its core, QWeSST is a small functional programming language extended with primitives for mobile code and remote procedure calls, two distinguishing features of web programming. It supports a localized view of typechecking and of evaluation, which reflects the way we program web applications and web services. We have developed a prototype implementation for QWeSST and used it to elegantly write simple web applications that are however not easily expressed using current web technology. …We give two semantics for QWeSST, one is standard and models a naive form of single-threaded evaluation, the other is maximally parallel and exploits a presentation of its typing and execution behaviors based on an extended form of substructural operational semantics. It augments standard inference rules with a construction that realizes parametric multiset comprehension, which makes it convenient to capture ensemble-level behaviors. We prove that both semantics are type safe, the former using traditional methods, the latter by developing a proof methodology that parallels the multiset-oriented presentation of the semantics. Show more

Keywords: Web Programming, Type Safety, Parallelism, Mobile Code, Substructural Operational Semantics

DOI: 10.3233/FI-2014-982

Citation: Fundamenta Informaticae, vol. 130, no. 1, pp. 67-97, 2014

Authors: Köhler-Bußmeier, Michael

Article Type: Research Article

Abstract: This contribution presents recent results on Elementary Object Systems (EOS). Object nets are Petri nets which have Petri nets as tokens – an approach known as the nets-within-nets paradigm. In this work we study the relationship of EOS to existing Petri net formalisms. It turns out that EOS are equivalent to counter programs. But even for the restricted subclass of conservative EOS reachability and liveness are undecidable problems. On the other hand for other properties like boundedness are still decidable for conservative EOS. We also study the sub-class of generalised state machines, which is worth mentioning since it combines decidability …of many theoretically interesting properties with a quite rich practical modelling expressiveness. Show more

Keywords: Petri nets, nets-within-nets, reachability, liveness, boundedness

DOI: 10.3233/FI-2014-983

Citation: Fundamenta Informaticae, vol. 130, no. 1, pp. 99-123, 2014

Authors: Mendler, Michael | Scheele, Stephan

Article Type: Research Article

Abstract: We aim to establish the multi-modal logic CKn as a baseline for a constructive correspondence theory of constructive modal logics. Just like many classical multi-modal logics may be studied as theories of the basic system K obtained by model-theoretic specialisation, we envisage constructive modal logics to be derived as proof-theoretic enrichments of CKn . The system CKn would then act as a core system for constructive contextual reasoning with controlled information flow. In this paper, as a first step towards this goal, we study CKn as a type theory and introduce its computational λ-calculus, λCKn . Extending …previous work on CKn , we present a cut-free contextual sequent system in the spirit of Masini's two-dimensional generalisation of natural deduction and Brünnler's nested sequents and give a computational interpretation for CKn following the Curry-Howard Correspondence. The associated modal type theory λCKn permits an interpretation for both the modalities □ and ◊ of CKn as type operators with simple and independent constructors and destructors, which has been missing in the literature. It is shown that the calculus satisfies subject reduction, strong normalisation and confluence. Since normal forms can be characterised by way of a Gentzen-style typing system with sub-formula property, λCKn is suitable for proof search in CKn . At the same time, λCKn enjoys natural deduction style typing which is important for programming applications. In contrast to most existing modal type theories, which are obtained as theories of the constructive modal logic S4, CKn is not bound to a particular contextual interpretation. Thus, λCKn constitutes the core of a functional language which provides static type checking of information processing to support safe contextual navigation in relational structures like those treated by description logics. We review some existing work on modal type theories and discuss their relation to λCKn . Show more

DOI: 10.3233/FI-2014-984

Citation: Fundamenta Informaticae, vol. 130, no. 1, pp. 125-162, 2014