Scoped and typed staging by evaluation

Guillaume Allais

doi:10.1145/3635800.3636964

Scoped and typed staging by evaluation

Guillaume Allais^*

^*Corresponding author for this work

University Of Strathclyde

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

39 Downloads (Pure)

Abstract

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 parts 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.

Original language	English
Title of host publication	PEPM 2024
Subtitle of host publication	Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation
Editors	Gabriele Keller, Meng Wang
Place of Publication	New York, NY
Pages	83-93
Number of pages	11
ISBN (Electronic)	9798400704871
DOIs	https://doi.org/10.1145/3635800.3636964
Publication status	Published - 11 Jan 2024
Event	2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation - London, United Kingdom Duration: 16 Jan 2024 → 16 Jan 2024

Conference

Conference	2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation
Abbreviated title	PEPM 2024
Country/Territory	United Kingdom
City	London
Period	16/01/24 → 16/01/24

Keywords

Agda
dependent types
hardware descriptions
normalisation by evaluation
staging
two level type theory

Access to Document

10.1145/3635800.3636964

Allais-PEPM-2024-Scoped-and-typed-staging-by-evaluationAccepted author manuscript, 842 KBLicence: Strath_1

Scoped and Typed Staging by Evaluation
Allais, G. (Invited speaker)
3 Dec 2024
Activity: Talk or presentation types › Invited talk

Cite this

@inproceedings{46a58d1dc54f4f0ea4eed23c0f377566,

title = "Scoped and typed staging by evaluation",

abstract = "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 parts 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.",

keywords = "Agda, dependent types, hardware descriptions, normalisation by evaluation, staging, two level type theory",

author = "Guillaume Allais",

year = "2024",

month = jan,

day = "11",

doi = "10.1145/3635800.3636964",

language = "English",

pages = "83--93",

editor = "Gabriele Keller and Meng Wang",

booktitle = "PEPM 2024",

note = "2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, PEPM 2024 ; Conference date: 16-01-2024 Through 16-01-2024",

}

Allais, G 2024, Scoped and typed staging by evaluation. in G Keller & M Wang (eds), PEPM 2024: Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation. New York, NY, pp. 83-93, 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, London, United Kingdom, 16/01/24. https://doi.org/10.1145/3635800.3636964

TY - GEN

T1 - Scoped and typed staging by evaluation

AU - Allais, Guillaume

PY - 2024/1/11

Y1 - 2024/1/11

N2 - 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 parts 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.

AB - 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 parts 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.

KW - Agda

KW - dependent types

KW - hardware descriptions

KW - normalisation by evaluation

KW - staging

KW - two level type theory

U2 - 10.1145/3635800.3636964

DO - 10.1145/3635800.3636964

M3 - Conference contribution book

AN - SCOPUS:85182921783

SP - 83

EP - 93

BT - PEPM 2024

A2 - Keller, Gabriele

A2 - Wang, Meng

CY - New York, NY

T2 - 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation

Y2 - 16 January 2024 through 16 January 2024

ER -

Scoped and typed staging by evaluation

Abstract

Conference

Keywords

Access to Document

Fingerprint

Activities

Scoped and Typed Staging by Evaluation

Cite this