scholarly journals From CML to process Algebras

1993 ◽  
Vol 22 (433) ◽  
Author(s):  
Flemming Nielson ◽  
Hanne Riis Nielson
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Process Algebra ◽  
Operational Semantics ◽  
Concurrent Programming ◽  
Process Algebras ◽  
Standard Ml ◽  
Concurrent Programming Languages ◽  
Structural Operational Semantics ◽  
Communication Behaviours

<p>Reppy's language CML extends Standard ML of Milner et al. with primitives for communication. It thus inherits a notion of strong polymorphic typing and may be equipped with a structural operational semantics. We formulate an effect system for statically expressing the communication behaviours of CML programs as these are not otherwise reflected in the types.</p><p>We then show how types and behaviours evolve in the course of computation: types may decrease and behaviours may loose alternatives as well as decrease. It will turn out that the syntax of behaviours is rather similar to that of a process algebra; our main results may therefore be viewed as regarding the semantics of a process algebra as an <em>abstraction</em> of the semantics of an underlying programming language. This establishes a new kind of connection between ''realistic'' concurrent programming languages and ''theoretical'' process algebras.</p>

scholarly journals A Linear Logic Programming Language for Concurrent Programming over Graph Structures

2014 ◽  
Vol 14 (4-5) ◽  
pp. 493-507 ◽  
Author(s):  
FLAVIO CRUZ ◽  
RICARDO ROCHA ◽  
SETH COPEN GOLDSTEIN ◽  
FRANK PFENNING
Keyword(s):  
Data Structure ◽  
Logic Programming ◽  
Programming Languages ◽  
Programming Language ◽  
Linear Logic ◽  
Operational Semantics ◽  
Concurrent Programming ◽  
Logical System ◽  
Logic Programming Language ◽  
Graph Data

AbstractWe have designed a new logic programming language called LM (Linear Meld) for programming graph-based algorithms in a declarative fashion. Our language is based on linear logic, an expressive logical system where logical facts can be consumed. Because LM integrates both classical and linear logic, LM tends to be more expressive than other logic programming languages. LM programs are naturally concurrent because facts are partitioned by nodes of a graph data structure. Computation is performed at the node level while communication happens between connected nodes. In this paper, we present the syntax and operational semantics of our language and illustrate its use through a number of examples.

scholarly journals On the Action Semantics of Concurrent Programming Languages

1992 ◽  
Vol 21 (424) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Semantic Description ◽  
Paper Briefly ◽  
Action Semantics ◽  
Concurrent Programming Languages ◽  
Structural Operational Semantics ◽  
Bisimulation Equivalence ◽  
Basic Concepts

<p>Action semantics is a framework for semantic description of prograrnming languages. In this framework, actions are semantic entities, used to represent the potential behaviour of programs --- also the contributions that parts of programs make to such behaviour. The notation for expressing actions, called action notation, is combinator-based. It is used in much the same way that lambda-notation is used in denotational semantics. However, the essence of action notation is operational, rather than mathematical, and its meaning is formally defined by a structural operational semantics together with a bisimulation equivalence.</p><p>This paper briefly motivates action semantics, and explains the basic concepts. It then illustrates the use of the framework by giving an action semantic description of a small example language. This language includes a simple form of concurrency: tasks that may synchronize by means of rendezvous. The paper also discusses the operational semantics of action notation, focusing on the primitive actions that represent asynchronous message transmission and process initiation.</p>

scholarly journals Persistent Stochastic Non-Interference

2021 ◽  
Vol 181 (1) ◽  
pp. 1-35
Author(s):  
Jane Hillston ◽  
Andrea Marin ◽  
Carla Piazza ◽  
Sabina Rossi
Keyword(s):  
Process Algebra ◽  
Operational Semantics ◽  
Evaluation Process ◽  
Decision Algorithm ◽  
Secure Systems ◽  
Information Flow Security ◽  
Structural Operational Semantics ◽  
Timing Properties ◽  
Functional Point ◽  
Security Property

In this paper, we study an information flow security property for systems specified as terms of a quantitative Markovian process algebra, namely the Performance Evaluation Process Algebra (PEPA). We propose a quantitative extension of the Non-Interference property used to secure systems from the functional point view by assuming that the observers are able to measure also the timing properties of the system, e.g., the response time of certain actions or its throughput. We introduce the notion of Persistent Stochastic Non-Interference (PSNI) based on the idea that every state reachable by a process satisfies a basic Stochastic Non-Interference (SNI) property. The structural operational semantics of PEPA allows us to give two characterizations of PSNI: one based on a bisimulation-like equivalence relation inducing a lumping on the underlying Markov chain, and another one based on unwinding conditions which demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. A decision algorithm for PSNI is presented and an application of PSNI to a queueing system is discussed.

M-nets: An algebra of high-level Petri nets, with an application to the semantics of concurrent programming languages

1998 ◽  
Vol 35 (10) ◽  
pp. 813-857 ◽  
Author(s):  
Eike Best ◽  
Wojciech Frączak ◽  
Richard P. Hopkins ◽  
Hanna Klaudel ◽  
Elisabeth Pelz
Keyword(s):  
Petri Nets ◽  
Programming Languages ◽  
Concurrent Programming ◽  
Concurrent Programming Languages ◽  
High Level
Sign in / Sign up

Export Citation Format

Share Document