Advances in hardware technology have proven incapable of keeping up with the growing needs of increasingly complex software systems. To bridge this gap, it would be possible to design software that would allow different tasks to be performed out of order (concurrently)concurrently, rather than in sequence, and then distributed over multiple computing cores to achieve parallel computation.
A type system acts as a programmer’s guide through a language, a set of logical rules through which the compiler can discern programs which have meaning from those that do not and hence protects the programmer from being able to write nonsensical programs. Unfortunately, many of the type systems for mainstream programming languages do not provide any protections for concurrent programs and as it so happens, implementing concurrent software is a notoriously difficult task. The interactions of different concurrent processes with each other and with shared resources introduce whole new families of software bugs. Furthermore, the non-deterministic nature of concurrency makes these bugs exceedingly hard to locate, understand, and ultimately fix.
To address the above mentioned difficulties, session types [1] have been proposed as a formalism for describing interactions between concurrent processes. Embedding such a formalism into a type system would present the programmer with guidance and safety guarantees when developing concurrent programs.
This final-year project has focused on a particular session type formalism, namely the semi-axiomatic sequent calculus (SAX) [2] whose operational interpretation corresponds to asynchronous message-passing concurrency. The aim was to adapt SAX’s theoretical type specification to render it suitable for implementation and practical for the programmer, by applying the technique of bidirectional typing [3] to the existent type system.
The above objectives are to produce a deterministic type-checking algorithm, along with a corresponding implementation, while a secondary objective is to limit the type annotation burden placed on the programmer when writing programs in SAX.
Figure 1. A one-place buffer (OPB) encoded in SAX
Figure 2. A type Inference and bidirectional rules OPB derivations
Student: Benjamin Borg
Supervisor : Prof. Adrian Francalanza