Scoped and typed staging by evaluation

Allais, Guillaume (2024) Scoped and typed staging by evaluation. Other. arXiv, Ithaca, N.Y.. (https://doi.org/10.48550/arXiv.2310.13413)

[thumbnail of Allais-arXiv-2024-Scoped-and-typed-staging]
Preview
 Text. Filename: Allais-arXiv-2024-Scoped-and-typed-staging.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (819kB)| 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 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.

ORCID iDs

Allais, Guillaume ORCID logoORCID: https://orcid.org/0000-0002-4091-657X;
  • Item type:Monograph(Other)
    ID code:87893
    Dates:
    Date
    Event
    11 January 2024
    Published
    20 October 2023
    Published Online
    Notes:As submitted to PEPM 2024
    Subjects:Science > Mathematics > Electronic computers. Computer science
    Department:UNSPECIFIED
    Depositing user: Pure Administrator
    Date deposited:24 Jan 2024 15:29
    Last modified:20 Nov 2024 01:41
    URI:https://strathprints.strath.ac.uk/id/eprint/87893
CORE (COnnecting REpositories)