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.