Muroya, Koko (2020). Hypernet semantics of programming languages. University of Birmingham. Ph.D.
|
Muroya2020PhD.pdf
Text - Accepted Version Available under License All rights reserved. Download (2MB) | Preview |
Abstract
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. | ||||||
Supervisor(s): |
|
||||||
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 |
Actions
Request a Correction | |
View Item |
Downloads
Downloads per month over past year