Defined algebraic operations

Geron, Bram ORCID: 0000-0001-9237-3282 (2020). Defined algebraic operations. University of Birmingham. Ph.D.

Text - Accepted Version
Available under License Creative Commons Attribution.

Download (1MB) | Preview


Defined algebraic operations ("DAO") is a novel model of programming, which sits broadly between imperative and purely functional programming. DAO expresses many control-flow idioms in a fashion similar to algebraic effect handling. But operation definition is lexical, and commutes with sequencing (when that type-checks).

DAO has three particular strengths. Firstly, DAO automatically avoids name clashes when writing higher-order programs with nonlocal control. This is demonstrated with a simple example. Secondly, certain buggy programs do not type check due to the lexical nature of DAO.

Thirdly, it validates a strong "theory-dependent" logic, which uses properties of operation definitions to add equivalences inside their scope. For instance, under an operation definition for state, most state equations hold, even under lambdas --- the analogous statement for handling is false. This lends extra credibility to the claim that DAO is a form of user-defined effects.

To substantiate these claims, we give a concrete DAO language and logic based on the fine-grain call-by-value lambda calculus, and a number of examples. As an additional contribution, we give a simpler presentation of a method for proving coherence of denotational semantics, first presented in a more sophisticated setting by Biernacki and Polesiuk.

Type of Work: Thesis (Doctorates > Ph.D.)
Award Type: Doctorates > Ph.D.
Licence: Creative Commons: Attribution 4.0
College/Faculty: Colleges (2008 onwards) > College of Engineering & Physical Sciences
School or Department: School of Computer Science
Funders: Engineering and Physical Sciences Research Council
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Q Science > QA Mathematics > QA76 Computer software


Request a Correction Request a Correction
View Item View Item


Downloads per month over past year