Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Linear Contextual Metaprogramming and Session Types

Pedro Ângelo, Atsushi Igarashi, Vasco T. Vasconcelos

TL;DR

This work tackles the challenge of integrating metaprogramming with linear context tracking and session types to enable typed code generation and remote code exchange. It develops a call-by-value linear lambda calculus with multi-level contexts and a box modality to stage contextual code and track free variables via contextual types. It sketches extensions to concurrency and session types, introducing primitives for channel-based communication and a process layer to support servers producing code on demand. The work lays a foundation for safe distributed metaprogramming with linear resources and points toward algorithmic type checking and richer session-type features in future work.

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.

Linear Contextual Metaprogramming and Session Types

TL;DR

This work tackles the challenge of integrating metaprogramming with linear context tracking and session types to enable typed code generation and remote code exchange. It develops a call-by-value linear lambda calculus with multi-level contexts and a box modality to stage contextual code and track free variables via contextual types. It sketches extensions to concurrency and session types, introducing primitives for channel-based communication and a process layer to support servers producing code on demand. The work lays a foundation for safe distributed metaprogramming with linear resources and points toward algorithmic type checking and richer session-type features in future work.

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.
Paper Structure (15 sections, 1 theorem, 5 equations)

This paper contains 15 sections, 1 theorem, 5 equations.

Table of Contents

  1. Introduction
  2. Linear staged metaprogramming
  3. Syntax
  4. Contexts for local and outer variables
  5. Substitution
  6. Evaluation
  7. Typing contextual terms
  8. Typing variables
  9. Typing $\lambda$ abstraction and application
  10. Typing * introduction and elimination
  11. Typing box introduction and elimination
  12. An example from Mœ bius
  13. From linear staged to session staged metaprogramming
  14. Conclusion and future work
  15. Acknowledgements

Key Result

Lemma 2.1

Theorems & Definitions (1)

  • Lemma 2.1: Substitution principle