Type System for Computational Resource Management

To write secure programs, it is crucial to manage computational resources (such as computation time, memory, file handles, and variable ownership) safely.

We study the application of type systems (such as substructural types, coeffect types, and ownership types) to software development for managing various computational resources that appear in programs.