et en

Thesis topics from Danel Ahman

Here are some thesis topics. If these are not exactly what you are looking for, but you are interested in programming languages, logics, semantics, or verification, then please get in touch and we'll find a topic that suits you best.

Contact: Danel Ahman (danel.ahman(at)ut.ee)

Formal verification of effectful (e.g., embedded) programs in F*

F* [1] is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving. It has an excellent support for reasoning about programs containing computational effects (state, exceptions, IO, nondeterminism, etc) based on Dijkstra monads [2] and layered indexed effects [3], and then extracting such verified code to runnable OCaml, C, and Rust.

A thesis in this area would involve learning F* and using its effect system to specify and verify the correctness of some effectful programs or algorithms. One of the goals of the thesis would be to demonstrate that F* is a good tool for a hybrid style of program verification: you can focus on formally verifying certain critical aspects of a piece of software, while postulating in an abstract interface that the rest of the software behaves as intended by the programmer.

For example, one example project idea in this area is to use the Steel and Pulse frameworks [4] of F* to verify the correctness of some embedded IoT software, written in C or Rust, and running on small microcontrollers, such as on ESP32. For a better idea of the work involved, [5] demonstrates the use of the older Low* framework in F* for specifying and verifying the memory-safety of simple ESP32 programs installing interrupt handlers and reacting to interrupts.

Any potential students are of course very welcome to propose their own ideas about which effectful programs or algorithms to specify and verify in F*. Students interested in the verification of algorithms in other dependently typed programming languages (e.g., Agda) are also welcome to get in contact.

Going beyond broadcast semantics for asynchronous algebraic effects

Asynchronous algebraic effects [1,2] is an approach to accommodate asynchronous computations in a mathematically natural way in programming languages based on algebraic effects and effect handlers [4] via the means of sending signals, receiving interrupts, and triggering interrupt handlers. This approach is formalised in a core effectful lambda-calculus, equipped with a type-and-effect system, small-step operational semantics, and a prototype implementation [3].

The goal of this thesis project would be to generalise the current broadcast everywhere propagation of signals and interrupts to something more fine-grain, in which it would be possible to control which other processes or agents receive certain signals, so as to improve the efficiency of such communication.

This thesis project could both be approached (i) more theoretically by working more with the lambda calculus underpinning asynchronous effects, or (ii) more practically by working more on extending the prototype implementation.

Combining asynchronous algebraic effects with general effect handlers

Asynchronous algebraic effects [1,2] is an approach to accommodate asynchronous computations in a mathematically natural way in programming languages based on algebraic effects and effect handlers [4] via the means of sending signals, receiving interrupts, and triggering interrupt handlers. This approach is formalised in a core effectful lambda-calculus, equipped with a type-and-effect system, small-step operational semantics, and a prototype implementation [3].

The goal of this thesis project would be to give asynchronous algebraic effects more control over continuations, so as to for example remove memory leaks in examples that currently can only simulate cancellations of remote process calls. This could involve combining asynchronous effects with general effect handlers or investigating how to give signals, interrupts, or interrupt handlers a more bespoke access to the continuations of current and other programs.

A Haskell DSL for temporal resources

Temporal resources [1,2] is an approach for using a static type system to specify and verify temporal properties of the resources that programs use, e.g., that before an assembly robot can assemble pieces of furniture, they have dry for a certain amount of time after being painted, or that before a chemical solution can be used certain time needs to pass for necessary reactions to take place.

The core lambda calculus underpinning temporal resources currently has only a deeply embedded toy prototype written in OCaml [3,4]. The goal of this project would be to design and implement a shallowly embedded domain-specific language (DSL) in a functional language such as Haskell (but it could also be in Idris, OCaml, etc). As the correct usage of temporal resources relies on modal types, which are not a common feature in existing languages, part of this project would involve developing a suitable compiler or typechecker plugin to be able to use types to check for temporal properties of resources. If working in Haskell, inspiration can be drawn from work on modal functional reactive programming [5].

Compared to the existing deeply embedded prototype implemented in OCaml, a shallowly embedded DSL in Haskell (or other language) would allow the programmer to immediately use all the other features such language allows (e.g., type classes).

Extending a prototype language for temporal resources with new features

Temporal resources [1,2] is an approach for using a static type system to specify and verify temporal properties of the resources that programs use, e.g., that before an assembly robot can assemble pieces of furniture, they have dry for a certain amount of time after being painted, or that before a chemical solution can be used certain time needs to pass for necessary reactions to take place.

As part of a recent CS UT MSc thesis [3,4] a prototype implementation of the lambda calculus underpinning temporal resources was developed in OCaml. The goal of this thesis would be to extend the underlying lambda calculus and the prototype implementation with new and more realistic language features (e.g., supporting different notions of temporal specifications, adding first-class polymorphism, recursion/iteration that account for temporal properties, and/or extending the language with an appropriate notion of concurrency/parallelism).

Another direction this thesis project could go would be to improve the user experience of this prototype implementation, such as supporting syntax highlighting, interactive web-based code development, or for example even developing a VS Code plugin to interface with the prototype implementation.

Linear temporal resources

Temporal resources [1,2] is an approach for using a static type system to specify and verify temporal properties of the resources that programs use, e.g., that before an assembly robot can assemble pieces of furniture, they have dry for a certain amount of time after being painted, or that before a chemical solution can be used certain time needs to pass for necessary reactions to take place.

The goal of this thesis project would be to investigate and prototype how temporal resources could be combined with linear (or more generally, quantitative) types [3,4]. The aim is to be able to additionally statically model during typechecking and compilation time that certain resources can only be used once (or some other prescribed number of times), in addition to them only being available after a certain amount of time (as guaranteed by the existing types).

Going beyond discrete time for temporal resources

Temporal resources [1,2] is an approach for using a static type system to specify and verify temporal properties of the resources that programs use, e.g., that before an assembly robot can assemble pieces of furniture, they have dry for a certain amount of time after being painted, or that before a chemical solution can be used certain time needs to pass for necessary reactions to take place.

The goal of this thesis project is to investigate and prototype how to go beyond natural numbers based discrete time specifications in the lambda calculus and type system for temporal resources. In particular, currently both computations and resources are specified in terms of discrete time, but there is no need for this to be the case, especially as different kinds of resources might have a different notion of "time" that they have to be correct against, this could be discrete time, could also be certain sequences of events that have to take place before a particular resource is deemed available for to be used.

Dependently sorted algebraic theories for container data structures

Containers [1] are a neat mathematical model of many parameterised data structures (e.g., lists, streams, sequences, trees, graphs, etc) in which such data structures are described in terms of the shape of the data (e.g., length of a list) and the arrangement of positions in these shapes where actual data values are mapped to (e.g., the positions of a list of length n are natural numbers 0, 1, ..., n-1, i.e., the indices of such a list). Containers also enjoy a full and faithful interpretation as a certain nice class of set functors.

There are various natural restrictions one can impose on containers to capture data structures with additional properties, such as requiring each position in a shape to determine another, compatible sub-shape, such as present in (sub-)lists and (sub-)trees [2]. While some of these restrictions have natural corresponding restrictions on the class of set functors that containers interpret into (e.g., the subshape restriction corresponds to comonad structure on the functors interpreting such containers), others do not have them or they are far from (at least seemingly) being mathematically natural. The goal of this thesis project is to develop a general notion of dependently sorted algebraic theories (where sorts are the shapes and terms proper are the positions) to capture these different examples of containers, and work out and validate the details of interpreting such theories on the set functor interpretation of containers.

Combining runners of algebraic effects with general effect handlers

Algebraic effects and effect handlers [1,2] are an active modern research area for specifying and programming with a wide range of computational effects (e.g., state, exceptions, I/O, nondeterminism, probability, etc) in a single mathematically well-behaving framework. One of the most significant applications of effect handlers, and the reason why they are now natively incorporated into OCaml 5, is their ability to express a wide range of models of concurrency and to allow users to define and modularly switch between different schedulers in user code. However, when the correct behaviour of programs requires the linear use and correct finalisation of certain resources (such as opening and closing file handles), the use of general effect handlers can quickly lead to incorrect program behaviour. For such situations, a restriction of general effect handlers, called runners of algebraic effects, has been developed [3].

Unfortunately, while runners cover many examples that programmers typically want to use in their programs, they are unable to express concurrency. The goal of this project is to investigate how to safely combine runners of algebraic effects with general effect handlers, so that the linearity and finalisation guarantees given by runners are respected by the general effect handlers (e.g., in concurrency).

This project could either focus more on the theoretical study of such a combination, or instead develop the ideas practically by building on extending the two prototype implementations of runners of algebraic effects [4,5].


Defended thesises