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 give arithmetical proofs of the strong normalization of two symmetric$\lambda$-calculi corresponding to classical logic. The first one is the$\bar{\lambda}\mu\tilde{\mu}$-calculus introduced by Curien & Herbelin. It isderived via the Curry-Howard correspondence from Gentzen's classical sequentcalculus LK in order to have a symmetry on one side between "program" and"context" and on other side between "call-by-name" and "call-by-value". Thesecond one is the symmetric $\lambda \mu$-calculus. It is the $\lambda\mu$-calculus introduced by Parigot in which the reduction rule $\mu'$, whichis the symmetric of $\mu$, is added. These results were already known but theprevious proofs use candidates of reducibility where the interpretation of atype is defined as the fix point of some increasing operator and thus, arehighly non arithmetical.

Arithmetical proofs of strong normalization results for symmetric lambda calculi