Por Pedro Ângelo (Universidade de Lisboa - LASIGE).
Session types enforce structured communication on concurrent and distributed systems, ensuring messages sent and received adhere to specified communication protocols. Programming language support for session types rests on linear type systems, paramount for maintaining a strict control over the use of resources, namely, channel endpoints. Staged metaprogramming consists of writing programs that generate and manipulate other programs, allowing type safe run-time code generation and manipulation, across computation stages. The intuitionistic fragment of the modal logic S4 serves as the underlying logical interpretation of binding times and computation stages. In this talk, we'll explore the integration of staged metaprogramming capabilities into a session-typed functional language, taking great care to ensure types expressing computation stages are safely integrated into the linear type system. We motivate this integration with an example of servers preparing and shipping code, via messages adhering to protocols described via session types. We conclude by discussing the future integration of staged metaprogramming into the in-house session typed language compiler Freest. This is joint work with Atsushi Igarashi, Yuito Murase and Vasco Vasconcelos.
Keywords: linear type systems, session types, structured communication, staged metaprogramming, code generation.
