Linear Contextual Metaprogramming and Session Types
<|reference_start|>Linear Contextual Metaprogramming and Session Types: 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.<|reference_end|>
@article{ângelo2024linear,
    title={Linear Contextual Metaprogramming and Session Types},
    author={Pedro ^Angelo (LIACC & Faculdade de Ci^encias da Universidade do
  Porto, Portugal), Atsushi Igarashi (Kyoto University, Kyoto, Japan), Vasco T.
  Vasconcelos (LASIGE, Faculdade de Ci^encias da Universidade de Lisboa,
  Portugal)},
    journal={EPTCS 401, 2024, pp. 1-10},
    year={2024},
    doi={10.4204/EPTCS.401.1},
    archivePrefix={arXiv},
    eprint={2404.05475},
    primaryClass={cs.LO cs.PL}
}