Studies concerning the meaning of computer programs: formal specifications and implementations, monolithic and distributed programs, and the semantics of syntactic transformations
Creators: name: Qin, Xueying
Publisher: name: The University of Edinburgh
Year: 2024
Subjects: computer programs
syntactic transformations
specifications and implementations
monolithic frameworks
distributed frameworks
Universal Method Invocation (UMI) library

description: This doctoral thesis presents three studies that concerns the meaning of computer programs in three different aspects, namely, specifications and implementations, monolithic and distributed frameworks, and the formal semantics of syntactic transformations. In general, three conceptual questions have been asked and addressed by these three studies. The first conceptual question is: How to design a better abstraction mechanism that allows programmers to effectively express what they want a computer to do via some declarative yet accurate specifications instead of how a computer should accomplish a task via some concrete implementations? The study, “Primrose: Selecting Container Data Types by Their Properties”, addresses this question by exploring ways to design a specification for a container that truly allows a programmer to separate its interface and usage from the implementation and to select a concrete implementation determined by its interface and usage. By conducting this study, I conclude that such separation of concerns enables automation and optimisation for application developers to use a container data type in their programs. The second conceptual question is: How to intuitively understand distributed programs using the same conceptual model as monolithic programs? The question is addressed by the study of designing a remote procedural call library — the Universal Method Invocation (UMI) library — for Rust. The UMI library supports location transparency by encapsulating the message-passing details and provides programmers an interface that allows them to migrate a monolithic program into a distributed setting, while preserving the semantics and without massive changes to the syntax of the program. This study provides a perspective on designing distributed systems: A monolithic program can be viewed as an abstraction of a distributed program, specifying what functionalities a program attempts to achieve instead of how these functionalities are achieved in a distributed setting by abstracting away the details of distributed memory management and message passing over a network. The third conceptual question is: How do we characterise the relationship between the syntax and semantics of programming languages? The study, “Shoggoth: A Formal Foundation for Strategic Rewriting”, addresses this question by giving three different models of formal semantics: denotational semantics, big-step operational semantics, and axiomatic semantics, to a core calculus of strategic rewriting languages which is used for composing syntactic transformations. The study provides a periii spective on the relationship in the context of rewriting: The syntax and semantics are interdependent, since we have observed that transformations of the syntax of expressions encode the meaning for the evaluation of these expressions. In the meanwhile we can characterise and reason about executions of compositions of these syntactic transformations of expressions by analysing their semantics.