Scoped and typed staging by evaluation

Allais, Guillaume; Keller, Gabriele and Wang, Meng, eds. (2024) Scoped and typed staging by evaluation. In: PEPM 2024. Association for Computing Machinery, Inc, GBR, pp. 83-93. ISBN 9798400704871 (https://doi.org/10.1145/3635800.3636964)

[thumbnail of Allais-PEPM-2024-Scoped-and-typed-staging-by-evaluation]
Preview
 Text. Filename: Allais-PEPM-2024-Scoped-and-typed-staging-by-evaluation.pdf
Accepted Author Manuscript
License: Strathprints license 1.0
Download (862kB)| Preview

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.

CORE (COnnecting REpositories)