Theoretical studies on multi-stage programming owe a lot to seminal work by
Davies and Pfenning [1]} and
Davies [2]}, who found Curry-Howard correspondence
between multi-stage calculi and modal logic. In particular, Davies'
\(\lambda ^\circ \)  [2]} has been a basis for several
multi-stage calculi with quasi-quotation. \(\lambda ^\circ \)  did not have
operators for run and CSP; a few
studies [4]}, [5]} enhanced and
improved \(\lambda ^\circ \)  towards the development of a type-safe multi-stage
calculus with quasi-quotation, run, and CSP, which were proposed by Taha and
Sheard as constructs for multi-stage programming [6]}.
Finally, Taha and Nielsen invented the concept of environment
classifiers [7]} and developed a typed calculus
\(\lambda ^\alpha \) , which was equipped with all the features above in a type
sound manner and formed a basis of earlier versions of MetaOCaml. Different
approaches to type-safe multi-stage programming with slightly different
constructs for composing and running code values have been studied by Kim,
Yi, and Calcagno [8]} and Nanevski and
Pfenning [9]}.
