Scoped and Typed Staging by Evaluation

TL;DR

This work addresses the challenge of providing a formally well-scoped, typed two-level staging framework with a static and a dynamic layer. It develops an intrinsically scoped-and-typed two-level calculus whose staging is realized by a Kripke-based normalisation-by-evaluation model, and demonstrates practical extensions including natural numbers and static pairs, culminating in a circuit-generation application. The approach yields a principled, type-safe platform for metaprogramming and circuit description, mechanised in Agda, and positioned within the landscape of partial evaluation, typed metaprogramming, and circuit-description languages. It outlines concrete directions for further work, including soundness proofs and generic two-level constructions that could generalize the framework to broader languages and dependently typed circuit languages.

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.