Contextual Metaprogramming for Session Types
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866914270789238784 |
|---|---|
| author | Ângelo, Pedro Igarashi, Atsushi Murase, Yuito Vasconcelos, Vasco T. |
| author_facet | Ângelo, Pedro Igarashi, Atsushi Murase, Yuito Vasconcelos, Vasco T. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_15180 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Contextual Metaprogramming for Session Types Ângelo, Pedro Igarashi, Atsushi Murase, Yuito Vasconcelos, Vasco T. Programming Languages 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. |
| title | Contextual Metaprogramming for Session Types |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2601.15180 |