Galois connecting call-by-value and call-by-name

DOI10.46298/lmcs-20(1:13)2024arXiv2202.08246v6OpenAlexW4391754855MaRDI QIDQ6151562

Dylan McDermott, Alan Mycroft

Publication date: 11 March 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2202.08246v6

zbMATH Keywords

categorical semanticscomputational effectevaluation ordercall-by-push-value

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Notions of computation and monads
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Retraction approach to CPS transform
• A syntactic view of computational adequacy
• Monads for which structures are adjoint to units
• Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• A reflection on call-by-value
• Adjunction Models For Call-By-Push-Value With Stacks
• The duality of computation
• A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators
• Gradual type theory
• Call-by-value is dual to call-by-name
• Reasoning about multi-stage programs
• Extended call-by-push-value: reasoning about effectful programs and evaluation order
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item