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

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The lambda-bar-mu-mu-tilde-calculus, defined by Curien and Herbelin, is a variant of the lambda-mu-calculus that exhibits symmetries such as terms/contexts and call-by-name/call-by-value. Since it is a symmetric, and hence a non-deterministic calculus, usual proof techniques of normalization needs some adjustments to work in this setting. Here we prove the strong normalization (SN) of simply typed lambda-bar-mu-mu-tilde-calculus with explicit substitutions. For that purpose, we first prove SN of simply typed lambda-bar-mu-mu-tilde-calculus (by a variant of the reducibility technique from Barbanera and Berardi), then we formalize a proof technique of SN via PSN (preservation of strong normalization), and we prove PSN by the perpetuality technique, as formalized by Bonelli.

Strong Normalization of $\overline{\lambda}\mu\widetilde{\mu}$ -Calculus with Explicit Substitutions