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 have previously published the Isabelle/HOL formalization of a generaltheory of syntax with bindings. In this companion paper, we instantiate thegeneral theory to the syntax of lambda-calculus and formalize the developmentleading to several fundamental constructions and results: sound semanticinterpretation, the Church-Rosser and standardization theorems, andhigher-order abstract syntax (HOAS) encoding. For Church-Rosser andstandardization, our work covers both the call-by-name and call-by-valueversions of the calculus, following classic papers by Takahashi and Plotkin.During the formalization, we were able to stay focused on the high-level ideasof the development -- thanks to the arsenal provided by our general theory: awealth of basic facts about the substitution, swapping and freshness operators,as well as recursive-definition and reasoning principles, including aspecialization to semantic interpretation of syntax.

Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS