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.

翻译：本文提出将分阶段元编程技术集成到一种基于会话类型的消息传递函数式语言中。我们构建了一个基于多级上下文的上下文模态类型理论模型，其中上下文值（即对一系列变量闭合的任意项）可以被封装并通过消息传递。接收方在收到此类值后，可将其解封并进行本地应用后执行。为阐明该集成的实际意义，我们列举了若干现实应用场景的示例，例如服务器通过会话类型消息按需准备并传输代码的场景，这些场景均适用于本系统。我们提出了一种类型系统，能够区分线性资源（仅使用一次）与非受限资源（可无限次使用），并进一步设计了适用于具体实现的类型检查器。我们证明了类型保持性、顺序计算中的进展性质，以及并发运行时环境下的运行时错误消除，同时验证了类型检查器的正确性。