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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Starting with Hoare Logic over 50 years ago, numerous sound and relativelycomplete program logics have been devised to reason about the diverse programsencountered in the real world. This includes reasoning about computationaleffects, particularly those effects that cause the program execution to branchinto multiple paths due to, e.g., nondeterministic or probabilistic choice.  The recently introduced Outcome Logic reimagines Hoare Logic with effects atits core, using an algebraic representation of choice to capture a variety ofeffects. In this paper, we give the first relatively complete proof system forOutcome Logic, handling general purpose looping for the first time. We alsoshow that this proof system applies to programs with various effects and thatit facilitates the reuse of proof fragments across different kinds ofspecifications.

A Relatively Complete Program Logic for Effectful Branching