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

We present Lilac, a separation logic for reasoning about probabilisticprograms where separating conjunction captures probabilistic independence.Inspired by an analogy with mutable state where sampling corresponds to dynamicallocation, we show how probability spaces over a fixed, ambient sample spaceappear to be the natural analogue of heap fragments, and present a newcombining operation on them such that probability spaces behave like heaps andmeasurability of random variables behaves like ownership. This combiningoperation forms the basis for our model of separation, and produces a logicwith many pleasant properties. In particular, Lilac has a frame rule identicalto the ordinary one, and naturally accommodates advanced features likecontinuous random variables and reasoning about quantitative properties ofprograms. Then we propose a new modality based on disintegration theory forreasoning about conditional probability. We show how the resulting modal logicvalidates examples from prior work, and give a formal verification of anintricate weighted sampling algorithm whose correctness depends crucially onconditional independence structure.

Lilac: A Modal Separation Logic for Conditional Probability