1. Project Title: Dependent session types and applications to the verification of concurrent programs

2. Area of Knowledge: Physical Sciences, Mathematics and Engineering Panel

3. Group of disciplines: Theoretical and Applied Mathematics, Computer Sciences and IT

4. Research project:
Developing concurrent programs was, is, and probably shall continue to be an arduous task. The subtle interactions among concurrent tasks easily evade the understanding of the best programmers. Session types have arisen as a tool to describe exchanges in concurrent programs. To cope with the ceaseless increasing complexity of software, new abstractions are required. This research project consists in expanding the expressive power of session types by stating dependencies among the messages exchanged by processes. It will strive to combine session types with dependent types, by proposing a theory that allows expressing both dependencies on the content of messages and on the type or number of messages to be exchanged. In this way, we could readily stipulate that integer messages in a session are exchanged in ascending order, or that the first message defines the number of messages that will be exchanged thereafter.
The main objective of the project involves exploring how dependent types can be compounded with session types to formulate expressive theories to model and verify properties of concurrent programs. This work provides a relevant and valuable theoretical contribution to type theory. These formal methods are of utmost importance to ensure the correct implementation of message passing protocols with explicit dependency between exchanged messages. The development of a prototype in the form of a compiler for a concurrent functional programming language incorporating linear dependent types will enable to validate the results. The proper integration of these formal methods into programming languages used by industry is expected to have a positive impact on software development and verification.

5. Job position description:
The research shall start with an overall familiarization with the techniques and formalism used in type theory, ranging from session types, linear type systems, linear interpretations of session types, dependent type systems, and linear dependent types.
The study then continues by looking into the combination of dependent types with session types so that values exchanged in messages may feature dependencies. The starting point is the recent proposals by McBride and Atkey to introduce linearity in traditional dependent session types systems, whereby variables in contexts are annotated with the number of times they may be computationally used: a zero means something unusable for consumption (computation), yet available for static contemplation (type formation). The combination of dependent types with session types accentuates the need for replication of limited resources in a way they can be used as many times as needed and after that can be contemplated. The main purpose of this research work consists in exploring and proposing a type theory able to formally specify dependencies on the content of exchanged messages and on the type or number of messages to be exchanged.
To validate the results, the workplan includes the incorporation of the proposed methodologies and types in a prototype that can be made from scratch, built on top of the Idris programming language, or even on languages such as Rust or Go. This prototype shall then be uses to verify the properties of some
message passing protocols. Several case studies shall be conducted to attest the flexibility of the approach, by identifying, formalising and, ultimately, verifying properties involving dependency between the types of exchanged messages.

6. Group leader:
Title: Doctor
Full name: Vasco T. Vasconcelos
Email: vmvasconcelos@ciencias.ulisboa.pt
Research group website: https://lasige.pt/research-line/reliable-software-systems/