The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
This paper is a themed account of the action semantics project, which Peter Mosses has led since the 1980s. It explains his motivations for developing action semantics, the inspirations behind its design, and the foundations of action semantics based on unified algebras. It goes on to outline some applications of action semantics to describe real programming languages, and some efforts to implement...
Security policies are one of the most fundamental elements of computer security. This paper uses colored Petri net process (CPNP) to specify and verify security policies in a modular way. It defines fundamental policy properties, i.e., completeness, termination, consistency and confluence, in Petri net terminology and gets some theoretical results. According to XACML combiners and property-preserving...
Parameterization is one of the most powerful features to make specifications and declarative programs modular and reusable, and our best hope for scaling up formal verification efforts. This paper studies order-sorted parameterization at three different levels: (i) its mathematical semantics; (ii) its operational semantics by term rewriting; and (iii) the inductive reasoning principles that can soundly...
We present Maude Object-Oriented Action Tool, an executable environment that incorporates elements from for Object-Oriented and Constructive Action Semantics. Our tool is implemented as a conservative extension of Full Maude and Maude MSOS Tool. The syntax used by our tool is fairly similar to the one used by the original Action Semantics formalism. Furthermore, we present an Object-Oriented Action...
Peter Mosses has contributed to computer science in many different ways. In particular, to programming language semantics. I had the pleasure, and the honor, to work with Peter Mosses as a PhD student and to collaborate with him afterwards. His work has greatly influenced my research interests. In this paper, I focus on his constructive approach to the semantics of programming languages. Constructive...
Weighted transition systems are defined, parametrized by a commutative monoid of weights. These systems are further understood as coalgebras for functors of a specific form. A general rule format for the SOS specification of weighted systems is obtained via the coalgebraic approach of Turi and Plotkin. Previously known formats for labelled transition systems (GSOS) and stochastic systems (SGSOS) appear...
Model transformation is one of the key notions in the model-driven engineering approach to software development. Most work in this area concentrates on designing methods and tools for defining or implementing transformations, on defining interesting specific classes of transformations, or on proving properties about given transformations, like confluence or termination. However little attention has...
We derive two big-step abstract machines, a natural semantics, and the valuation function of a denotational semantics based on the small-step abstract machine for Core Scheme presented by Clinger at PLDI’98. Starting from a functional implementation of this small-step abstract machine, (1) we fuse its transition function with its driver loop, obtaining the functional implementation of a big-step abstract...
We present a context-sensitive reduction semantics for a lambda-calculus with explicit substitutions and we show that the functional implementation of this small-step semantics mechanically corresponds to that of the abstract machine for Core Scheme presented by Clinger at PLDI’98, including first-class continuations. Starting from this reduction semantics, (1) we refocus it into a small-step abstract...
Evolution of programming languages requires co-evolution of static analysis tools designed for these languages. Traditional approaches to static analysis, e.g., those based on Structural Operational Semantics (SOS), assume, however, that the syntax and the semantics of the programming language under consideration are fixed. Language modification is, therefore, likely to cause redevelopment of the...
Introduction This article describes some results concerning the conceptual separation of model dependent and language inherent aspects in a denotational semantics of a programming language. Before going into the technical explanation, the authors wish to relate a story that illustrates how correctly and precisely posed questions can influence the direction of research. By means of his questions, Professor...
This paper surveys some recent works on the study of termination in a concurrent setting. Processes are π-calculus processes, on which type systems are imposed that ensure termination of the process computations. Two approaches are exposed. The first one draws on the method of logical relations, which has been extensively used in the analysis of sequential languages. The second approach exploits notions...
We propose a naive version of action semantics that begins with a selection of “transient” and “persistent” facets, each characterized as a partial monoid. Yielders are defined as operations on the monoids’ values, and actions extract values from the facets, give them to yielders, and place the results into facet output. Actions are composed with a primary combinator, andthen, which can be specialized...
We make a connection between higher-order rewriting in the form of combinatory reduction systems (CRS) and logic-based operational semantics in the form of big step semantic (BSS) specifications. We show how sets of CRS rewrite rules can be encoded as BSS, and how BSS (including natural semantics) can be encoded as CRS. The connections permit the use of proper variables and substitution in both formalisms.
The UML Testing Profile (U2TP) provides a means of using UML for test case specification. In this work we show how the concepts of model-based testing can be mapped to U2TP at the conceptual level. We discuss structural as well as behavioural issues that allow certain aspects of model-based testing to be considered an instance of U2TP. This is achieved without insisting that model-based testing should...
We present a co-inductive syntactic theory, eager normal form bisimilarity, for the untyped call-by-value lambda calculus extended with continuations and mutable references. We demonstrate that the associated bisimulation proof principle is easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs. The theory is modular in...
Research into embedded sensor networks has placed increased focus on the problem of developing reliable and flexible software for microcontroller-class devices. Languages such as nesC [10] and Virgil [20] have brought higher-level programming idioms to this lowest layer of software, thereby adding expressiveness. Both languages are marked by the absence of dynamic memory allocation, which removes...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.