Abstract: We explore the integration of metaprogramming in a call-by-value linear lambda-calculus and sketch its extension to a session type system. We build on a model of contextual modal type theory with multi-level contexts, where contextual values, closing arbitrary terms over a series of variables, may then be boxed and transmitted in messages. Once received, one such value may then be unboxed (with a let-box construct) and locally applied before being run. We present a series of examples where servers prepare and ship code on demand via session typed messages.

Bio: Pedro Ângelo is a PhD student in the Doctoral Program in Computer Science at the Department of Computer Science, Faculty of Sciences, University of Porto. He is also an Invited Assistant Professor at the Department of Computer Science, Faculty of Sciences, University of Lisbon. His research interests cover type systems for functional languages, such as gradual typing and intersection types, and how these can be adapted to other paradigms, such as the object-oriented language Featherweight Java.