2026-07-30T04:42:18Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16313 2024-03-06T10:57:13Z ddc:004 open_access

Galois Connecting Call-by-Value and Call-by-Name McDermott, Dylan Mycroft, Alan computational effect evaluation order call-by-push-value categorical semantics We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with side-effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no side-effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name. We propose a technique for stating and proving these properties. The key ingredient is Levy’s call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We construct maps between the call-by-value and call-by-name interpretations of types. We then identify properties of side-effects that imply these maps form a Galois connection. These properties hold for some side-effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates call-by-value and call-by-name. We apply the reasoning principle to example side-effects including divergence and nondeterminism. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dylan McDermott and Alan Mycroft 2022 Is Part Of LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2022.32 urn:nbn:de:0030-drops-163138 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.32 eng https://creativecommons.org/licenses/by/4.0/legalcode