Scoped and Typed Staging by Evaluation
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929206983655424 |
|---|---|
| author | Allais, Guillaume |
| author_facet | Allais, Guillaume |
| contents | Using a dependently typed host language, we give a well scoped-and-typed by construction presentation of a minimal two level simply typed calculus with a static and a dynamic stage. The staging function partially evaluating the part of a term that are static is obtained by a model construction inspired by normalisation by evaluation.
We then go on to demonstrate how this minimal language can be extended to provide additional metaprogramming capabilities, and to define a higher order functional language evaluating to digital circuit descriptions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_13413 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Scoped and Typed Staging by Evaluation Allais, Guillaume Programming Languages D.3.1; F.3.2 Using a dependently typed host language, we give a well scoped-and-typed by construction presentation of a minimal two level simply typed calculus with a static and a dynamic stage. The staging function partially evaluating the part of a term that are static is obtained by a model construction inspired by normalisation by evaluation. We then go on to demonstrate how this minimal language can be extended to provide additional metaprogramming capabilities, and to define a higher order functional language evaluating to digital circuit descriptions. |
| title | Scoped and Typed Staging by Evaluation |
| topic | Programming Languages D.3.1; F.3.2 |
| url | https://arxiv.org/abs/2310.13413 |