Observed communication semantics provide an intuitive notion of equivalence for communicating programs. We give the first observed communication semantics for a session-typed programming language with general recursion. This language, Polarized SILL, also supports channel and code transmission, synchronous and asynchronous communication, and functional programming. We present a framework inspired by testing preorders for defining simulations based on observed communications. We show that the "external" simulations coincide with barbed precongruence. Polarized SILL is defined using a multiset-rewriting-style substructural operational semantics. To ensure that our observed communication semantics is well-defined, we introduce fairness for multiset rewriting systems. We construct a fair scheduler and we give sufficient conditions for traces to be fair.
翻译：观测到的通信语义为通信程序提供了一个直观的等同概念。 我们给一个会话类型编程语言提供第一个观测到的通信语义, 并进行一般性循环。 这个语言, 极化的 SILL, 也支持频道和代码传输, 同步和不同步的通信, 以及功能性编程 。 我们提出了一个受测试预选程序启发的框架, 用于根据观察到的通信来定义模拟 。 我们显示“ 外部” 模拟与条形预感相吻合 。 极化 SIL 的定义是使用多套式重写风格的亚结构操作语义 。 为确保我们观察到的通信语义定义明确, 我们为多谱重写系统引入了公平性。 我们构建了一个公平的排程器, 我们为追踪公平提供了充分的条件 。
相关内容
微信扫码咨询专知VIP会员