Defined algebraic operations

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

Preview

Geron2020PhD.pdf
Text - Accepted Version
Available under License Creative Commons Attribution.
Download (1MB) | Preview

Abstract

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.

Supervisor(s):