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

Networks of communicating processes can be viewed as networks of stream transformers and programmed in a lazy functional language. Thus the correctness of concurrent systems can be reduced to the correctness of functional programs. In this paper such correctness is proved formally in theµ-calculus extended with recursion equations for functional programs. Theµ-calculus is chosen since it allows the definition of properties by least fixed points (induction) as well as by greatest fixed points (coinduction), and since greatest fixed points are useful for formalising properties, such as fairness, of infinitely proceeding programs. Moreover, non-deterministic processes are represented as incompletely specified deterministic processes, that is, as properties of stream transformers. This method is illustrated by proving the correctness of the alternating bit protocol.

A functional programming approach to the specification and verification of concurrent systems