The Metatheory of Symmetric Metaprogramming
This note presents a simplified variant of principled metaprogramming and sketches its soundness proof. The variant treats only dialogues between two stages. A program can have quotes which can contain splices (which can contain quotes, which can contain splices, and so on). Or the program could start with a splice with embedded quotes. The essential restriction is that (1) a term can contain toplevel quotes or toplevel splices, but not both, and (2) quotes cannot appear directly inside quotes and splices cannot appear directly inside splices. In other words, the universe is restricted to two phases only.
Under this restriction we can simplify the typing rules so that there are always exactly two environments instead of having a stack of environments. The variant presented here differs from the full calculus also in that we replace evaluation contexts with contextual typing rules. While this is more verbose, it makes it easier to set up the meta theory.
Syntax
Terms t ::= x variable
(x: T) => t lambda
t t application
’t quote
~t splice
Simple terms u ::= x  (x: T) => u  u u
Values v ::= (x: T) => t lambda
’u quoted value
Types T ::= A base type
T > T function type
’T quoted type
Operational semantics
Evaluation
((x: T) => t) v > [x := v]t
t1 > t2

t1 t > t2 t
t1 > t2

v t1 > v t2
t1 ==> t2

’t1 > ’t2
Splicing
~’u ==> u
t1 ==> t2

(x: T) => t1 ==> (x: T) => t2
t1 ==> t2

t1 t ==> t2 t
t1 ==> t2

u t1 ==> u t2
t1 > t2

~t1 ==> ~t2
Typing Rules
Typing judgments are of the form E1 * E2  t: T
where E1, E2
are environments and *
is one of ~
and ’
.
x: T in E2

E1 * E2  x: T
E1 * E2, x: T1  t: T2

E1 * E2  (x: T1) => t: T > T2
E1 * E2  t1: T2 > T E1 * E2  t2: T2

E1 * E2  t1 t2: T
E2 ’ E1  t: T

E1 ~ E2  ’t: ’T
E2 ~ E1  t: ’T

E1 ’ E2  ~t: T
(Curiously, this looks a bit like a Christmas tree).
Soundness
The metatheory typically requires mutual inductions over two judgments.
Progress Theorem
 If
E1 ~  t: T
then eithert = v
for some valuev
ort > t2
for some termt2
.  If
’ E2  t: T
then eithert = u
for some simple termu
ort ==> t2
for some termt2
.
Proof by structural induction over terms.
To prove (1):
 the cases for variables, lambdas and applications are as in STLC.
 If
t = ’t2
, then by inversion we have’ E1  t2: T2
for some typeT2
. By the second induction hypothesis (I.H.), we have one of:t2 = u
, hence’t2
is a value,t2 ==> t3
, hence’t2 > ’t3
.
 The case
t = ~t2
is not typable.
To prove (2):

If
t = x
thent
is a simple term. 
If
t = (x: T) => t2
, then eithert2
is a simple term, in which caset
is as well. Or by the second I.H.t2 ==> t3
, in which caset ==> (x: T) => t3
. 
If
t = t1 t2
then one of three cases applies:t1
andt2
are a simple term, thent
is as well a simple term.t1
is not a simple term. Then by the second I.H.,t1 ==> t12
, hencet ==> t12 t2
.t1
is a simple term butt2
is not. Then by the second I.H.t2 ==> t22
, hencet ==> t1 t22
.

The case
t = ’t2
is not typable. 
If
t = ~t2
then by inversion we haveE2 ~  t2: ’T2
, for some typeT2
. By the first I.H., we have one oft2 = v
. Sincet2: ’T2
, we must havev = ’u
, for some simple termu
, hencet = ~’u
. By quotesplice reduction,t ==> u
.t2 > t3
. Then by the context rule for’t
,t ==> ’t3
.
Substitution Lemma
 If
E1 ~ E2  s: S
andE1 ~ E2, x: S  t: T
thenE1 ~ E2  [x := s]t: T
.  If
E1 ~ E2  s: S
andE2, x: S ’ E1  t: T
thenE2 ’ E1  [x := s]t: T
.
The proofs are by induction on typing derivations for t
, analogous to the proof for STL (with (2) a bit simpler than (1) since we do not need to swap lambda bindings with the bound variable x
). The arguments that link the two hypotheses are as follows.
To prove (1), let t = ’t1
. Then T = ’T1
for some type T1
and the last typing rule is
E2, x: S ’ E1  t1: T1

E1 ~ E2, x: S  ’t1: ’T1
By the second I.H. E2 ’ E1  [x := s]t1: T1
. By typing, E1 ~ E2  ’[x := s]t1: ’T1
. Since [x := s]t = [x := s](’t1) = ’[x := s]t1
we get [x := s]t: ’T1
.
To prove (2), let t = ~t1
. Then the last typing rule is
E1 ~ E2, x: S  t1: ’T

E2, x: S ’ E1  ~t1: T
By the first I.H., E1 ~ E2  [x := s]t1: ’T
. By typing, E2 ’ E1  ~[x := s]t1: T
. Since [x := s]t = [x := s](~t1) = ~[x := s]t1
we get [x := s]t: T
.
Preservation Theorem
 If
E1 ~ E2  t1: T
andt1 > t2
thenE1 ~ E2  t2: T
.  If
E1 ’ E2  t1: T
andt1 ==> t2
thenE1 ’ E2  t2: T
.
The proof is by structural induction on evaluation derivations. The proof of (1) is analogous to the proof for STL, using the substitution lemma for the beta reduction case, with the addition of reduction of quoted terms, which goes as follows:
 Assume the last rule was
t1 ==> t2  ’t1 > ’t2
By inversion of typing rules, we must have
T = ’T1
for some typeT1
such thatt1: T1
. By the second I.H.,t2: T1
, hence’t2:
T1`.
To prove (2):

Assume the last rule was
~’u ==> u
. The typing proof of~’u
must have the formE1 ’ E2  u: T  E1 ~ E2  ’u: ’T  E1 ’ E2  ~’u: T
Hence,
E1 ’ E2  u: T
. 
Assume the last rule was
t1 ==> t2  (x: S) => t1 ==> (x: T) => t2
By typing inversion,
E1 ' E2, x: S  t1: T1
for some typeT1
such thatT = S > T1
. By the I.H,t2: T1
. By the typing rule for lambdas the result follows. 
The context rules for applications are equally straightforward.

Assume the last rule was
t1 ==> t2  ~t1 ==> ~t2
By inversion of typing rules, we must have
t1: ’T
. By the first I.H.,t2: ’T
, hence~t2: T
.