2026-09-20T00:25:48Zhttps://api.repository.cam.ac.uk/server/oai/request

oai:www.repository.cam.ac.uk:1810/3056422023-12-22T13:57:17Zcom_1810_219481com_1810_256065col_1810_219482

Reasoning about effectful programs and evaluation order 10.17863/CAM.52720 McDermott, Dylan 0000000267051449 Mycroft, Alan Program transformations have various applications, such as in compiler optimizations. These transformations are often effect-dependent: replacing one program with another relies on some restriction on the side-effects of subprograms. For example, we cannot eliminate a dead computation that raises an exception, or a duplicated computation that prints to the screen. Effect-dependent program transformations can be described formally using effect systems, which annotate types with information about the side-effects of expressions. In this thesis, we extend previous work on effect systems and correctness of effect-dependent transformations in two related directions. First, we consider evaluation order. Effect systems for call-by-value languages are well-known, but are not sound for other evaluation orders. We describe sound and precise effect systems for various evaluation orders, including call-by-name. We also describe an effect system for Levy's call-by-push-value, and show that this subsumes those for call-by-value and call-by-name. This naturally leads us to consider effect-dependent transformations that replace one evaluation order with another. We show how to use the call-by-push-value effect system to prove the correctness of transformations that replace call-by-value with call-by-name, using an argument based on logical relations. Finally, we extend call-by-push-value to additionally capture call-by-need. We use our extension to show a classic example of a relationship between evaluation orders: if the side-effects are restricted to (at most) nontermination, then call-by-name is equivalent to call-by-need. The second direction we consider is non-invertible transformations. A program transformation is non-invertible if only one direction is correct. Such transformations arise, for example, when considering undefined behaviour, nondeterminism, or concurrency. We present a general framework for verifying noninvertible effect-dependent transformations, based on our effect system for call-by-push-value. The framework includes a non-symmetric notion of correctness for effect-dependent transformations, and a denotational semantics based on order-enriched category theory that can be used to prove correctness. University of Cambridge 2019-10-01 Thesis Doctoral Doctor of Philosophy (PhD) eng https://www.repository.cam.ac.uk/handle/1810/305642 https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/739cbf54-0489-4339-beb3-2e86b9be5991/download 2e1b18d8d7c1167c92e34ae9428f1a2a https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/026a2314-c273-415c-8820-ce682024215f/download 353adac0d1ebdfd65ab16480263c3c87 https://creativecommons.org/licenses/by-sa/4.0/ computational effects evaluation order call-by-push-value call-by-need categorical semantics