  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.
