Subexponentials in non-commutative linear logic

Linear logical frameworks with subexponentials have been used for the specification of, among other systems, proof systems, concurrent programming languages and linear authorisation logics. In these frameworks, subexponentials can be configured to allow or not for the application of the contraction and weakening rules while the exchange rule can always be applied. This means that formulae in such frameworks can only be organised as sets and multisets of formulae not being possible to organise formulae as lists of formulae. This paper investigates the proof theory of linear logic proof systems in the non-commutative variant. These systems can disallow the application of exchange rule on some subexponentials. We investigate conditions for when cut elimination is admissible in the presence of non-commutative subexponentials, investigating the interaction of the exchange rule with the local and non-local contraction rules. We also obtain some new undecidability and decidability results on non-commutative linear logic with subexponentials.

Specifying Concurrent Program Based on TLA

.The Temporal logic of actions TLA is a logic for specifying and reasoning about concurrent systems, which make systems and their properties are expressed in the same logic. In this paper, we introduce the concurrent programming languages and behavior semantics, mainly describe safety properties and liveness properties in TLA and take NeedhamSchroeder symmetric key protocol as an example to illustrate how to specify these properties in concurrent program by TLA.

Coordination Languages and Models for Open Distributed Systems

Programming open distributed systems will be of rapidly growing importance in the coming decades to the scientists and engineers that will be using these techniques to solve society’s most pressing problems. Even today, the authors see a growing number of critical applications such as MRI spin relaxometry, gene sequence analysis, climate modeling, and molecular modeling of potential bioactive compounds that require massive amounts of computation. The demands for intensive computational power will only grow in the future, as society tackles more complex problems. Existing concurrent programming languages are not well-suited to the development of open distributed systems. Middleware technologies provide the support for the development of open distributed systems. However, the technologies suffer the same problems of existing concurrent programming approaches which the software evolution of the systems are not supported well. The resulting systems are difficult to maintain due to the changes. This has led to the design and implementation of a variety of coordination models and languages for open distributed systems. The main purpose is to separate the concerns of the complexities including communication, coordination, computation, and heterogeneity in the development of open distributed systems. The models manage the concerns to improve the maintenance of the systems.