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