Scoped and typed staging by evaluation

Research output: Working paperWorking Paper/Preprint

20 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 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.
Original languageEnglish
Place of PublicationIthaca, N.Y.
Number of pages11
DOIs
Publication statusPublished - 11 Jan 2024

Keywords

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

Fingerprint

Dive into the research topics of 'Scoped and typed staging by evaluation'. Together they form a unique fingerprint.

Cite this