文章基本信息

标题：The Call-By-Value Lambda-Calculus with Generalized Applications
本地全文：下载
作者：Jos Esp{\'\i}rito Santo
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：152
页码：1-12
DOI：10.4230/LIPIcs.CSL.2020.35
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Generalized applications; Natural deduction; Strong normalization; Standardization; Call-by-name; Call-by-value; Protecting-by-a-lambda