Title: The call-by-value Lambda-Calculus with generalized applications
Abstract: 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.
Publication Year: 2020
Publication Date: 2020-01-01
Language: en
Type: article
Access and Citation
Cited By Count: 4
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot