keywords: type systems, formal type theory, session types, language design

Currently I am working on session types. In particular, how session type theory can be integrated into a large-scale distributed programming model.

Given the upswing of interconnected devices, there are critical networks of interconnected devices where the tolerance for failure is low or non-existing. In order to assist the programmer of writing sturdy fault-proof code, session types can be used to statically verify the communication between the nodes on the network, which given the context of the application is a very - if not the most - important part of the application.

Combined with network-centric programming abstractions and on-line code updates we aim to provide a solid programming model for large scale distributed applications we call "grid applications".