English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

We present the first session typing system guaranteeing request-responseliveness properties for possibly non-terminating communicating processes. Thetypes augment the branch and select types of the standard binary session typeswith a set of required responses, indicating that whenever a particular labelis selected, a set of other labels, its responses, must eventually also beselected. We prove that these extended types are strictly more expressive thanstandard session types. We provide a type system for a process calculus similarto a subset of collaborative BPMN processes with internal (data-based) andexternal (event-based) branching, message passing, bounded and unboundedlooping. We prove that this type system is sound, i.e., it guaranteesrequest-response liveness for dead-lock free processes. We exemplify the use ofthe calculus and type system on a concrete example of an infinite state system.

Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion