Jacques: Created page with "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..."

2024-11-29T13:59:14Z

Created page with "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..."

New page

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.

WG211/M24Allais - Revision history

Jacques: Created page with "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..."