We propose the integration of staged metaprogramming into a session-typed message passing functional language. 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 be boxed and transmitted in messages. Once received, one such value may then be unboxed and locally applied before being run. To motivate this integration, we present examples of real-world use cases, for which our system would be suitable, such as servers preparing and shipping code on demand via session typed messages. We present a type system that distinguishes linear (used exactly once) from unrestricted (used an unbounded number of times) resources, and further define a type checker, suitable for a concrete implementation. We show type preservation, a progress result for sequential computations and absence of runtime errors for the concurrent runtime environment, as well as the correctness of the type checker.

We present FJ&λ⋆, a new core calculus that extends Featherweight Java (FJ) with interfaces, λ-expressions, intersection types and a form of dynamic type. Intersection types can be used anywhere, in particular to specify target types of λ-expressions. The dynamic type is exploited to specify parts of the class tables and programs we want to exclude temporarily from static typing. Our main result is the gradual guarantee, which says that if a program is well typed in a class table, then replacing type annotations (from the program and from the class table) with the dynamic type always produces a program that is still well typed in the obtained class table. Furthermore, if a typed program evaluates to a value in a class table, then replacing type annotations with dynamic types always produces a program that evaluates to the same value in the obtained class table.

Intersection types have the power to type expressions which are all of many different types. Gradual types combine type checking at both compile-time and run-time. Here we combine these two approaches in a new typed calculus that harness both of their strengths. We incorporate these two contributions in a single typed calculus and define an operational semantics with type cast annotations. We also prove several crucial properties of the type system, namely that types are preserved during compilation and evaluation, and that the refined criteria for gradual typing holds.