Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus

DOI10.1016/J.JLAMP.2022.100775OpenAlexW4226055581WikidataQ114013905 ScholiaQ114013905MaRDI QIDQ2141293

Tarmo Uustalu, José Espírito Santo, Luís Pinto

Publication date: 25 May 2022

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2022.100775

zbMATH Keywords

\(\lambda\)-calculuscall-by-valuecall-by-nameGirard's embeddingGödel's embeddingS4 modal logic

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (2)

A tribute to José Manuel Valença ⋮ Galois connecting call-by-value and call-by-name

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Lectures on the Curry-Howard isomorphism
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• The bang calculus revisited
• Factorization in call-by-name and call-by-value calculi via linear logic
• Call-By-Push-Value from a Linear Logic Point of View

This page was built for publication: Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus