Hypernet semantics of programming languages

Muroya, Koko (2020). Hypernet semantics of programming languages. University of Birmingham. Ph.D.

Text - Accepted Version
Available under License All rights reserved.

Download (2MB) | Preview


Comparison is common practice in programming, even regarding a single programming language. One would ask if two programs behave the same, if one program runs faster than another, or if one run-time system produces the outcome of a program faster than another system. To answer these questions, it is essential to have a formal specification of program execution, with measures such as result and resource usage.

This thesis proposes a semantical framework based on abstract machines that enables analysis of program execution cost and direct proof of program equivalence. These abstract machines are inspired by Girard’s Geometry of Interaction, and model program execution as dynamic rewriting of graph representation of a program, guided and controlled by a dedicated object (token) of the graph. The graph representation yields fine control over resource usage, and moreover, the concept of locality in analysing program execution. As a result, this framework enjoys novel flexibility, with which various evaluation strategies and language features, whether they are effects or not, can be modelled and analysed in a uniform way.

Type of Work: Thesis (Doctorates > Ph.D.)
Award Type: Doctorates > Ph.D.
Licence: All rights reserved
College/Faculty: Colleges (2008 onwards) > College of Engineering & Physical Sciences
School or Department: School of Computer Science
Funders: None/not applicable
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Q Science > QA Mathematics > QA76 Computer software
URI: http://etheses.bham.ac.uk/id/eprint/10433


Request a Correction Request a Correction
View Item View Item


Downloads per month over past year