## Temporal resources

Organisatsiooni nimi

Laboratory for Software Science

Kokkuvõte

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.

[1] https://arxiv.org/abs/2210.07738

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.

[1] https://arxiv.org/abs/2210.07738

Lõputöö kaitsmise aasta

2024-2025

Juhendaja

Danel Ahman

Suhtlemiskeel(ed)

eesti keel, inglise keel

Nõuded kandideerijale

Tase

Bakalaureus, Magister

Märksõnad

### Kandideerimise kontakt

Nimi

Danel Ahman

Tel

E-mail