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 Tools annual

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 monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

We propose Pushdown Normal Form (PDNF) Bisimulation to verify contextualequivalence in higher-order functional programming languages with local state.Similar to previous work on Normal Form (NF) bisimulation, PDNF Bisimulation issound and complete with respect to contextual equivalence. However, unliketraditional NF Bisimulation, PDNF Bisimulation is also decidable for a class ofprogram terms that reach bounded configurations but can potentially haveunbounded call stacks and input an unbounded number of unknown functions fromtheir context. Our approach relies on the principle that, in model-checking forreachability, pushdown systems can be simulated by finite-state automatadesigned to accept their initial/final stack content. We embody this in astackless Labelled Transition System (LTS), together with an on-the-flysaturation procedure for call stacks, upon which bisimulation is defined. Toenhance the effectiveness of our bisimulation, we develop up-to techniques andconfirm their soundness for PDNF Bisimulation. We develop a prototypeimplementation of our technique which is able to verify equivalence in examplesfrom practice and the literature that were out of reach for previous work.

Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence