Linear Contextual Metaprogramming and Session Types
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910402513731584 |
|---|---|
| author | Ângelo, Pedro Igarashi, Atsushi Vasconcelos, Vasco T. |
| author_facet | Ângelo, Pedro Igarashi, Atsushi Vasconcelos, Vasco T. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_05475 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Linear Contextual Metaprogramming and Session Types Ângelo, Pedro Igarashi, Atsushi Vasconcelos, Vasco T. Logic in Computer Science Programming Languages 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. |
| title | Linear Contextual Metaprogramming and Session Types |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2404.05475 |