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

Programs using random values can either make all choices in advance (eagerly)or sample as needed (lazily). In formal proofs, we focus onindistinguishability between two lazy programs, a common requirement in therandom oracle model (ROM). While rearranging sampling instructions often solvesthis, it gets complex when sampling is spread across procedures. Thetraditional approach, introduced by Bellare and Rogaway in 2004, convertsprograms to eager sampling, but requires assuming finite memory, a polynomialbound, and artificial resampling functions. We introduce a novel approach inprobabilistic Relational Hoare Logic (pRHL) that directly provesindistinguishability, eliminating the need for conversions and the mentionedassumptions. We also implement this approach in the EasyCrypt theorem prover,showing that it can be a convenient alternative to the traditional method.

A Direct Lazy Sampling Proof Technique in Probabilistic Relational Hoare Logic