Danel Ahman
Formal verification of effectful 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 programmind languages (e.g., Agda) are also welcome to get in contact.
- [1] https://fstar-lang.org
- [2] https://arxiv.org/abs/1903.01237
- [3] https://www.fstar-lang.org/papers/indexedeffects/indexedeffects.pdf
- [4] https://fstar-lang.org/tutorial/book/pulse/pulse.html
- [5] https://github.com/danelahman/esp32-fstar
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]. 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].
A thesis in this area could involve studying further aspects of the meta-theory of the underlying core effectful lambda-calculus (e.g., by studying the normalisation properties of its sequential part), or extending the underlying core effectful lambda-calculus and the prototype implementation in new and exciting ways (e.g., by designing type system-based means to tame the current broadcast-everywhere communication policy; or by extending the calculus with general effect handlers, while preserving the predictable programming model).
- [1] https://arxiv.org/abs/2003.02110
- [2] https://arxiv.org/abs/2307.13795
- [3] https://github.com/matijapretnar/aeff
- [4] https://homepages.inf.ed.ac.uk/slindley/papers/handlers.pdf
Temporal resources
Temporal resources [1] 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.
A thesis in this area would involve extending the core effectful lambda-calculus underlying the temporal resources approach in new and exciting ways. Example topics include:
- extending the calculus to being able to speak about more general specifications than simply natural number-valued time (e.g., to traces of program events);
- adding support for expiring resources;
- adding support for sub-typing and sub-effecting;
- combining temporal resources with linear types, so that one could also specify the spatial properties of such resources; and
- extending the modal type and effect system to dependent types.
For more applied students, another topic in this area would be to program an prototype implementation for the core effectful lambda-calculus underlying the temporal resources approach (either as a standalone typechecker and interpreter, or as a DSL in a language such as Haskell or OCaml), and to explore example uses of this approach.
Contact for more info: Danel Ahman (danel.ahman@ut.ee)