Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Abstract Continuation Semantics for Multiparty Interactions in Process Calculi based on CCS

Eneia Nicolae Todoran, Gabriel Ciobanu

TL;DR

It is shown that the continuation-based denotational models designed with continuations for process calculi based on CCS extended with mechanisms offering support for multiparty interactions are weakly abstract with respect to the corresponding operational models.

Abstract

We develop denotational and operational semantics designed with continuations for process calculi based on CCS extended with mechanisms offering support for multiparty interactions. We investigate the abstractness of this continuation semantics. We show that our continuation-based denotational models are weakly abstract with respect to the corresponding operational models.

Abstract Continuation Semantics for Multiparty Interactions in Process Calculi based on CCS

TL;DR

It is shown that the continuation-based denotational models designed with continuations for process calculi based on CCS extended with mechanisms offering support for multiparty interactions are weakly abstract with respect to the corresponding operational models.

Abstract

We develop denotational and operational semantics designed with continuations for process calculi based on CCS extended with mechanisms offering support for multiparty interactions. We investigate the abstractness of this continuation semantics. We show that our continuation-based denotational models are weakly abstract with respect to the corresponding operational models.

Paper Structure

This paper contains 12 sections, 14 theorems, 1 equation.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Denotable continuations
  4. Weak abstractness criterion
  5. Finite bags and the structure of continuations
  6. Continuation semantics for $CCS^n$
  7. Final Semantic Domains
  8. Operational semantics
  9. Denotational semantics
  10. Continuation semantics for $CCS^{n+}$
  11. Weak abstractness of continuation semantics
  12. Conclusion

Key Result

Theorem 1

Let $(M,d)$ be a non-empty complete metric space. Each contraction $f:M\to{M}$ has a unique fixed point.

Theorems & Definitions (49)

  • Theorem 1: Banach
  • Theorem 2
  • Theorem 3
  • Remark 1
  • Definition 1
  • Remark 2
  • Remark 3
  • Lemma 1
  • Definition 2
  • Remark 4
  • ...and 39 more