2026-07-24T05:02:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11678 2024-03-06T10:48:46Z ddc:004 open_access

The Call-By-Value Lambda-Calculus with Generalized Applications Espírito Santo, José Generalized applications Natural deduction Strong normalization Standardization Call-by-name Call-by-value Protecting-by-a-lambda The lambda-calculus with generalized applications is the Curry-Howard counterpart to the system of natural deduction with generalized elimination rules for intuitionistic implicational logic. In this paper we identify a call-by-value variant of the system and prove confluence, strong normalization, and standardization. In the end, we show that the cbn and cbv variants of the system simulate each other via mappings based on extensions of the "protecting-by-a-lambda" compilation technique. Schloss Dagstuhl – Leibniz-Zentrum für Informatik José Espírito Santo 2020 Is Part Of LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2020.35 urn:nbn:de:0030-drops-116786 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.35 eng https://creativecommons.org/licenses/by/3.0/legalcode