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

Model-checking is one of the most powerful techniques for verifying systemsand programs, which since the pioneering results by Knapik et al., Ong, andKobayashi, is known to be applicable to functional programs with higher-ordertypes against properties expressed by formulas of monadic second-order logic.What happens when the program in question, in addition to higher-orderfunctions, also exhibits algebraic effects such as probabilistic choice orglobal store? The results in the literature range from those, mostly positive,about nondeterministic effects, to those about probabilistic effects, in thepresence of which even mere reachability becomes undecidable. This work takes afresh and general look at the problem, first of all showing that there is anelegant and natural way of viewing higher-order programs producing algebraiceffects as ordinary higher-order recursion schemes. We then move on to considereffect handlers, showing that in their presence the model checking problem isbound to be undecidable in the general case, while it stays decidable whenhandlers have a simple syntactic form, still sufficient to capture so-calledgeneric effects. Along the way we hint at how a general specification languagecould look like, this way justifying some of the results in the literature, andderiving new ones.

On Model-Checking Higher-Order Effectful Programs (Long Version)