Contextual MetaML: Syntax and Full Abstraction

Andrzej S. Murawski; C.-H. Luke Ong; Haoxuan Yin

arxiv: 2602.03033 · v2 · pith:H75QP7H6new · submitted 2026-02-03 · 💻 cs.PL

Contextual MetaML: Syntax and Full Abstraction

Haoxuan Yin , Andrzej S. Murawski , C.-H. Luke Ong This is my paper

Pith reviewed 2026-05-21 15:01 UTC · model grok-4.3

classification 💻 cs.PL

keywords metaprogrammingcontextual modal typesfull abstractionoperational game semanticscontextual equivalencetype safetyopen codehigher-order references

0 comments

The pith

Contextual MetaML supports storing and running open code under strong type safety and proves the first full abstraction result for an imperative MetaML-style language.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Contextual MetaML, a metaprogramming language that uses contextual modal types to track free variables in code, enabling storage and execution of open code while preserving type safety. It constructs a semantic model from operational game semantics traces that represent programs by their possible interactions with the environment. This model delivers full abstraction for contextual equivalence, so programs are equivalent precisely when their traces match. The work includes a novel closed instances of use theorem covering both call-by-value and call-by-name closing substitutions. A reader would care because the result lets programmers perform meaning-preserving optimizations on metaprograms without introducing type errors from escaped variables.

Core claim

Contextual MetaML is the first metaprogramming language that supports storing and running open code under a strong type safety guarantee by using contextual modal types to track free variables explicitly, and its operational game semantics trace model establishes the first full abstraction result for contextual equivalence in an imperative MetaML-style language together with a novel closed instances of use theorem that accounts for call-by-value and call-by-name closing substitutions.

What carries the argument

The trace model derived via operational game semantics that defines the meaning of a program by its possible interactions with the environment, together with contextual modal types that explicitly track and reason about free variables in code.

If this is right

Optimized programs preserve original meaning whenever their trace models coincide.
Type safety holds when storing and running code even if free variables can escape their original binders.
Program equivalence can be decided by comparing trace sets instead of quantifying over all possible contexts.
The closed instances of use theorem permits reasoning about both call-by-value and call-by-name substitutions in metaprogramming.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The trace-based technique could be lifted to other metaprogramming calculi that include references.
Real implementations of staged computation might adopt the model to certify optimizations automatically.
The handling of open code opens a route to verifying code generators that produce fragments with unbound identifiers.
Adding recursion or other features while keeping the trace model fully abstract would be a direct next test.

Load-bearing premise

The operational game semantics trace model accurately captures all possible contextual interactions without omitting or over-approximating behaviors that would distinguish programs under contextual equivalence.

What would settle it

A concrete counterexample consisting of two programs in Contextual MetaML that are distinguished by some context yet possess identical trace sets, or that are contextually equivalent yet possess different trace sets, would falsify the full abstraction theorem.

Figures

Figures reproduced from arXiv: 2602.03033 by Andrzej S. Murawski, C.-H. Luke Ong, Haoxuan Yin.

**Figure 1.** Figure 1: Syntax 𝛿 that provides values for free variables in the term represented by 𝑢. An occurrence of 𝑢 in a term is also either free or bound. In the former case, it shall appear in the global variable context Ψ as 𝑢 : (Γ ⊢ 𝑇 ), which reads “𝑢 is of type 𝑇 under local variable context Γ”. In the latter case, it shall be bound by a Letbox construct letbox 𝑢 ← 𝑀1 in 𝑀2, which we shall explain now. LMML features t… view at source ↗

**Figure 2.** Figure 2: Well-formed types and typing contexts corresponds to MetaML’s ⟨1+ ~𝑀⟩. Compared with MetaML, LMML takes a more uniform and elegant approach to unboxing code, and avoids the problem that evaluations can go under lambda, as noted by Inoue and Taha [2016]. 2.2 Type System The typing rules of LMML are presented in Figures 2, 3, and 4. The way global variables are typed in the rule (Tm-GVar) should be read as f… view at source ↗

**Figure 3.** Figure 3: Well-typed terms [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗

**Figure 4.** Figure 4: Well-typed heaps, contexts and substitutions [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗

**Figure 5.** Figure 5: The rule (Letbox) does two things simultaneously. First, it extracts the content 𝑀1 from the code box 𝑀1, reminiscent of MetaML’s Escape and Run. Second, it substitutes 𝑀1 for all the occurrences of the global variable 𝑢 in 𝑀2, reminiscent of call-byname 𝛽-reductions. Reduction rules: (𝑀, ℎ) → (𝑀′ , ℎ′ ) (𝛽) ( (𝜆𝑥.𝑀)𝑉 , ℎ) → (𝑀 [𝑉 /𝑥], ℎ) (Arith) (𝑛b1 ⊕ 𝑛b2, ℎ) → (𝑛1 ⊕ 𝑛2, ℎ) 𝑛 ≠ 0 (If true) (if 𝑛bthen 𝑀… view at source ↗

**Figure 6.** Figure 6: Transition rules for Program LTS (P𝜏) is a silent transition that embeds the operational semantics into the LTS. (PA) concerns cases when the LTS has reached a value. The value is then announced in abstracted form 𝐴 through the action (𝐴, Σ, 𝜒), where 𝜒 is the abstraction of the current heap ℎ, restricted to locations that have been revealed to the context. (PQF) corresponds to reaching a 𝛽-redex where the… view at source ↗

read the original abstract

MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Contextual MetaML, \textit{the first metaprogramming language that supports storing and running open code under a strong type safety guarantee}. The type system utilises contextual modal types to track and reason about free variables in code explicitly. A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for Contextual MetaML, establishing \textit{the first full abstraction result for an imperative MetaML-style language}. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Contextual MetaML adds contextual modal types to safely store and run open code with references and claims the first full abstraction for imperative MetaML via operational game semantics traces.

read the letter

The main takeaway is a language design that uses contextual modal types to track free variables in code fragments explicitly, which lets the system support storing and executing open code under higher-order references without losing type safety. They pair this with a trace semantics drawn from operational game semantics and prove full abstraction for contextual equivalence, plus a closed-instances theorem that handles both call-by-value and call-by-name substitutions for code values. This combination is presented as new for the imperative MetaML setting and does not obviously collapse to earlier cited results. The type system looks like a direct response to the escape problem that has been a known issue in prior staging languages, and the semantic model gives a concrete way to reason about equivalence that could matter for optimizations. The trace approach itself is a standard external technique, so there is no obvious circularity in the construction. The soft spot is the completeness direction of full abstraction. The model must account for every environment interaction, including cases where the context supplies a closing substitution for free variables inside code that has already been stored in a reference. The paper invokes the closed-instances theorem for this, but if that theorem misses some imperative context that can observe the substitution after storage, the equivalence result would not hold in both directions. Without the full proof details it is hard to judge how tightly the theorem covers those cases. This work is for people who care about metaprogramming type systems and semantic models for equivalence. Readers working on safe staging or on game semantics for languages with state would get concrete technical material to build on. It has enough formal substance and a clear claim to deserve a serious referee who can check the interaction between the modal types and the trace model.

Referee Report

2 major / 2 minor

Summary. The paper introduces Contextual MetaML, a metaprogramming language that uses contextual modal types to ensure type safety when storing and running open code in the presence of higher-order references. It develops a semantic model based on traces from operational game semantics to capture contextual equivalence and claims the first full-abstraction result for an imperative MetaML-style language, supported by a novel closed-instances-of-use theorem that handles both call-by-value and call-by-name closing substitutions.

Significance. If the full-abstraction result holds, the work would be significant as the first semantic model for contextual equivalence in metaprogramming with mutable code references, enabling rigorous reasoning about optimizations. The operational game semantics traces and the closed-instances-of-use theorem are strengths that address key challenges in handling substitutions on stored open code.

major comments (2)

[Closed Instances of Use Theorem] Closed Instances of Use Theorem: The theorem is invoked to ensure the trace model captures all contextual interactions, including environment-provided closing substitutions on open code stored in higher-order references. However, its statement and proof sketch do not explicitly enumerate or cover all imperative contexts that can observe such substitutions after storage, which risks incompleteness in the full-abstraction claim.
[Semantic Model] Semantic Model (§4): The definition of the trace semantics via operational game semantics must be shown to be both sound and complete w.r.t. contextual equivalence. It is unclear whether the model fully accounts for all possible environment interactions with references containing open code, particularly call-by-name substitutions supplied post-storage.

minor comments (2)

[Abstract] The abstract's claim of being 'the first' metaprogramming language with these guarantees would benefit from a short comparison paragraph situating it against prior MetaML variants.
[Type System] Notation for contextual modal types should be introduced with a small example early in the type system section to aid readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading and constructive comments. We address the major points below and will revise the manuscript to improve clarity on the coverage of contexts and interactions while maintaining the strength of the full-abstraction result.

read point-by-point responses

Referee: [Closed Instances of Use Theorem] Closed Instances of Use Theorem: The theorem is invoked to ensure the trace model captures all contextual interactions, including environment-provided closing substitutions on open code stored in higher-order references. However, its statement and proof sketch do not explicitly enumerate or cover all imperative contexts that can observe such substitutions after storage, which risks incompleteness in the full-abstraction claim.

Authors: The Closed Instances of Use Theorem is formulated to encompass all relevant closing substitutions by integrating both call-by-value and call-by-name mechanisms within the operational game semantics framework. The proof sketch demonstrates how these are captured in the trace model to ensure completeness for contextual equivalence. We acknowledge that the current presentation may not make the coverage of all imperative contexts sufficiently explicit. Therefore, in the revised version of the manuscript, we will provide an expanded statement of the theorem and a more detailed proof that explicitly enumerates and addresses the possible contexts involving stored open code. revision: yes
Referee: [Semantic Model] Semantic Model (§4): The definition of the trace semantics via operational game semantics must be shown to be both sound and complete w.r.t. contextual equivalence. It is unclear whether the model fully accounts for all possible environment interactions with references containing open code, particularly call-by-name substitutions supplied post-storage.

Authors: Soundness and completeness of the trace semantics with respect to contextual equivalence are proven in Section 4 (Theorems 4.1 and 4.2). These results rely on the closed instances of use theorem to handle substitutions on open code, including call-by-name cases after storage in higher-order references. The operational game semantics traces are designed to model all environment interactions. To resolve any ambiguity, we will revise §4 to include additional explanations and examples illustrating how post-storage call-by-name substitutions are accounted for in the model. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation relies on standard external game semantics techniques

full rationale

The paper defines Contextual MetaML with contextual modal types and constructs a trace-based semantic model via operational game semantics to capture contextual equivalence, then proves full abstraction. This relies on an independently developed operational semantics and a novel closed-instances-of-use theorem for handling substitutions on stored open code. No step reduces by definition to its own output, no fitted parameters are renamed as predictions, and no load-bearing self-citation chain is invoked to force the result. The model is presented as capturing interactions with the environment rather than being defined in terms of the target equivalence, making the derivation self-contained against external benchmarks in game semantics.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claims rest on standard definitions of operational semantics and game-semantic traces plus the new contextual modal type rules; no numerical parameters are fitted and no new physical entities are postulated.

axioms (2)

domain assumption Operational game semantics traces faithfully represent contextual interactions of programs with their environment
Invoked when defining the semantic model that underpins the full abstraction result.
domain assumption Contextual modal types can be integrated with higher-order references while preserving type safety
Core premise of the language design stated in the abstract.

invented entities (1)

Contextual modal types no independent evidence
purpose: Track and reason about free variables in open code explicitly
New type construct introduced to solve the escape problem for free variables under higher-order references.

pith-pipeline@v0.9.0 · 5730 in / 1483 out tokens · 86399 ms · 2026-05-21T15:01:54.871166+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We provide a semantic model that captures contextual equivalence for Contextual MetaML, establishing the first full abstraction result for an imperative MetaML-style language. Our model is based on traces derived via operational game semantics... We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

The type system utilises contextual modal types to track and reason about free variables in code explicitly.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

16 extracted references · 16 canonical work pages

[1]

Then C′′ 2 =(𝑀 ′′, 𝑖, 𝑇 ,Σ′′ 2 , ℎ′′ 2 , 𝛾2, 𝜙2, 𝜉2, 𝜃2) where (𝑀, ℎ2) → (𝑀 ′′, ℎ′′ 2 ). Therefore, we have C1 ∧ ∧C2 =(𝜉 1 ∧ ∧𝜉2) [𝑀], ℎ2 +ℎ 1) [𝜄(𝛾1 ⊎𝛾 2)] →C1 ∧ ∧C′′ 2 =(𝜉 1 ∧ ∧𝜉2) [𝑀′′], ℎ′′ 2 +ℎ 1) [𝜄(𝛾1 ⊎𝛾 2)] Notice in particular that the above reduction is also valid under the special reduction rule (Letbox name). AsC ′′ 2 𝜏 − → ∗ C′ 2 in 𝑘− 1steps...

work page
[2]

Proof.We prove by case analysis ona

ThenC 1 ∧ ∧C2 = C′ 2 ∧ ∧ C′ 1. Proof.We prove by case analysis ona. •(PA). ThenC 2 (𝐴,Σ3,𝜒) − − − − − − →C′ 2 andC 1 (𝐴,Σ3,𝜒) − − − − − − →C′ 1, where –C 2 =(𝑉 , 𝑖, 𝑇 ,Σ 2, ℎ2, 𝛾2, 𝜙2, 𝜉2, 𝜃2) –C ′ 2 =(Σ 2, ℎ2, 𝛾2 ⊎𝛾 ′ 2 ⊎𝛾 ′′ 2 , 𝜙′ 2, 𝜉2,dom(𝜒)) – C1 =(Σ 1, ℎ1, 𝛾1, 𝜙1, 𝜉′ 1 : (Σ ′ 1 ⊢𝐾 : (·; ·;𝑇 ; 𝑖) → (· ; ·;𝑇 ′; 𝑖′)), 𝜃1) –C ′ 1 =(𝐾[𝐴], 𝑇 ′, 𝑖′,Σ 1 ∪Σ...

work page
[3]

∈A Val(Σ;·;· ⊢ 𝑖 𝑉:𝑇) –(𝜒, 𝛾 ′′ 2 ) ∈A Val(Σ;·;· ⊢ℎ 2 ↾𝜎∪𝜇(𝐴) :heap) Therefore, C1 ∧ ∧C2 =((𝜉 1 ∧ ∧𝜉2) [𝑉], ℎ2 +ℎ 1){𝜄(𝛾 1 ⊎𝛾 2)} =C′ 2 ∧ ∧C′ 1 =((𝜉 2 ∧ ∧𝜉′

work page
[4]

[𝐾[𝐴]],(𝜒+ℎ 1) +ℎ 2){𝛿(𝛾 1 ⊎ (𝛾 2 ⊎𝛾 ′ 2 ⊎𝛾 ′′ 2 ))} • (PQF). ThenC 2 (𝑓(𝐴),Σ 3,𝜒) − − − − − − − − − →C′ 2 andC 1 (𝑓(𝐴),Σ 3,𝜒) − − − − − − − − − →C′ 1, where –C 2 =(𝐾[𝑓 𝑉], 𝑖, 𝑇 ,Σ 2, ℎ2, 𝛾2, 𝜙2, 𝜉2, 𝜃2) – C′ 2 =(Σ 2, ℎ2, 𝛾2 ⊎𝛾 ′ 2 ⊎𝛾 ′′ 2 , 𝜙′ 2, 𝜉2 : (Σ 2 ⊢𝐾 : (·; ·;𝑇2; 𝑖3) → (·;·;𝑇;𝑖)),dom(𝜒)) –C 1 =(Σ 1, ℎ1, 𝛾1, 𝜙1, 𝜉1, 𝜎1) –C ′ 1 =(𝛾 1 (𝑓)𝐴, 𝑖 3, 𝑇2,...

work page
[5]

□ Now we show the other direction of the invariance, i.e., that reductions in the composed term correspond to transitions in con- figurations

∈A Val(Σ 2;·;· ⊢ 𝑖2 𝑉:𝑇 1) –𝑖 3 =max(𝑖 1, 𝑖2) –(𝜒, 𝛾 ′′ 2 ) ∈A Val(Σ;·;· ⊢ℎ 2 ↾𝜎∪𝜇(𝐴) :heap) Therefore, C1 ∧ ∧C2 =((𝜉 1 ∧ ∧𝜉2) [𝐾[𝑓 𝑉]], ℎ 2 +ℎ 1){𝜄(𝛾 1 ⊎𝛾 2)} =C′ 2 ∧ ∧C′ 1 =(((𝜉 2 :(Σ 2 ⊢𝐾:(·;·;𝑇 2;𝑖 3) → (·;·;𝑇;𝑖))) ∧ ∧𝜉 1) [𝛾1 (𝑓)𝐴],(𝜒+ℎ 1) +ℎ 2){𝛿(𝛾 1 ⊎𝛾 2 ⊎𝛾 ′ 2 ⊎𝛾 ′′ 2 )} •The other cases are similar therefore omitted. □ Now we show the other direc...

work page 2017
[6]

If any prefix of t′ contains at least as many (QB) actions as (A) actions, then by induction hypothesis we know that the number of (QB) actions in t′ is at most dep( #𝛾1 (𝑏) [𝜌])

SoC ′ 1 t′ − →C′′ 1 and C′ 2 t′ − →C′′ 2 , where t=(run𝑏 𝜌,Σ 3, 𝜒)t ′ and t′ consists only of (A) and (QB) actions. If any prefix of t′ contains at least as many (QB) actions as (A) actions, then by induction hypothesis we know that the number of (QB) actions in t′ is at most dep( #𝛾1 (𝑏) [𝜌]) . There- fore, the number of (QB) actions int is at mostdep( #...

work page
[7]

is an active configuration whose next tran- sition is a 𝜏 transition, or (b)C ′ 1 (orC ′

work page
[8]

In other words, there does not exist infinite sequences of𝜏-free transitions

is an active configuration whose next transition is a (PA) transition, andC ′ 2 (orC ′ 1, resp.) is a passive configuration whose stack 𝜉 is empty. In other words, there does not exist infinite sequences of𝜏-free transitions. Proof. We prove by case analysis on first step of transition the active configurationC 2. • (PQF). ThenC 2 (𝑓(𝐴),Σ 3,𝜒) − − − − − −...

work page
[9]

In the former case, the next transition ofC ′ 1 is a 𝜏 transition ((𝜆𝑥 .𝑀 ′)𝐴, 𝜒+ℎ 1) → (𝑀 ′ [𝐴/𝑥], 𝜒+ℎ 1), and clause (a) holds

∈A Val(Σ 2;·;· ⊢ 𝑖2 𝑉:𝑇 1) The term in the new active configurationC′ 1 is 𝛾1 (𝑓)𝐴 , where 𝛾1 (𝑓) is either 𝜆𝑥 .𝑀′ or 𝑓 ′ for some 𝑓 ′ ∈FNames 𝑇1→𝑇2,𝑖1. In the former case, the next transition ofC ′ 1 is a 𝜏 transition ((𝜆𝑥 .𝑀 ′)𝐴, 𝜒+ℎ 1) → (𝑀 ′ [𝐴/𝑥], 𝜒+ℎ 1), and clause (a) holds. In the latter case, the next transition ofC ′ 1 is a (PQF) transition (𝑓 ′...

work page
[10]

If there are multiple such 𝑖s, we choose the smallest one

is the smallest. If there are multiple such 𝑖s, we choose the smallest one. As a (QB) action increases siz(𝜉 𝑖

work page
[11]

by one, and an (A) action decreases siz(𝜉 𝑖

work page
[12]

By Lemma 19, this trace contains at most dep(𝑀 𝑖 ) (QB) actions, where 𝑀𝑖 is the term in the active configuration

by one, we know that the trace starting fromC 𝑖 1 andC 𝑖 2 always contains at least as many Layered Modal ML: Syntax and Full Abstraction Conference’17, July 2017, Washington, DC, USA (QB) actions as (A) actions. By Lemma 19, this trace contains at most dep(𝑀 𝑖 ) (QB) actions, where 𝑀𝑖 is the term in the active configuration. Therefore, this trace cannot ...

work page 2017
[13]

By induction bypothesis,C ′ 2 ∧ ∧C′ 1 ⇓0

ThenC ′ 2 | C′ 1 ↓t′ . By induction bypothesis,C ′ 2 ∧ ∧C′ 1 ⇓0. SupposeC 2 𝜏 − → ∗ C′′ 2 a − →C′ 2, and, obviously, C1 a − →C′

work page
[14]

By Lemma 17, C1 ∧ ∧C′′ 2 =C ′ 2 ∧ ∧C′

By Lemma 16,C 1 ∧ ∧C2 →∗ C1 ∧ ∧C′′ 2 . By Lemma 17, C1 ∧ ∧C′′ 2 =C ′ 2 ∧ ∧C′

work page
[15]

Then we prove ifC 1 ∧ ∧C2 ⇓0 thenC 1|C2 ↓t by induction on the number of steps in the reductionC 1 ∧ ∧C2 →∗ (𝑉 , ℎ′)

Therefore,C 1 ∧ ∧C2 ⇓0. Then we prove ifC 1 ∧ ∧C2 ⇓0 thenC 1|C2 ↓t by induction on the number of steps in the reductionC 1 ∧ ∧C2 →∗ (𝑉 , ℎ′). If there are 0 steps, then 𝑀 is a value, so empty trace is the t we are looking for. Otherwise,C 1 ∧ ∧C2 → (𝑀 ′′, ℎ′′) → ∗ (𝑉 , ℎ′). By Lemma 20, without loss of generality, there existsC ′ 1,C ′ 2 such thatC 1 t′ −...

work page
[16]

if(𝑥=𝐴)then()elseΩ

ThenC ′ 1 ∧ ∧C′ 2 ⇓0 as well, and by induction hypothesis we haveC 1|C2 ↓t′′ . Therefore, C1|C2 ↓t′ t′′ . □ The above result can be instantiated to initial configurations for programs and contexts to yield the following theorem. Theorem 12 (Correctness, Theorem 4).For any term Σ; Ψ; Γ⊢ 𝑖 𝑀 : 𝑇 , evaluation context Σ′ ⊢𝐾 : (·; ·; 𝑖;𝑇) → (· ; ·; 𝑖′;𝑇 ′), gl...

work page 2017

[1] [1]

Then C′′ 2 =(𝑀 ′′, 𝑖, 𝑇 ,Σ′′ 2 , ℎ′′ 2 , 𝛾2, 𝜙2, 𝜉2, 𝜃2) where (𝑀, ℎ2) → (𝑀 ′′, ℎ′′ 2 ). Therefore, we have C1 ∧ ∧C2 =(𝜉 1 ∧ ∧𝜉2) [𝑀], ℎ2 +ℎ 1) [𝜄(𝛾1 ⊎𝛾 2)] →C1 ∧ ∧C′′ 2 =(𝜉 1 ∧ ∧𝜉2) [𝑀′′], ℎ′′ 2 +ℎ 1) [𝜄(𝛾1 ⊎𝛾 2)] Notice in particular that the above reduction is also valid under the special reduction rule (Letbox name). AsC ′′ 2 𝜏 − → ∗ C′ 2 in 𝑘− 1steps...

work page

[2] [2]

Proof.We prove by case analysis ona

ThenC 1 ∧ ∧C2 = C′ 2 ∧ ∧ C′ 1. Proof.We prove by case analysis ona. •(PA). ThenC 2 (𝐴,Σ3,𝜒) − − − − − − →C′ 2 andC 1 (𝐴,Σ3,𝜒) − − − − − − →C′ 1, where –C 2 =(𝑉 , 𝑖, 𝑇 ,Σ 2, ℎ2, 𝛾2, 𝜙2, 𝜉2, 𝜃2) –C ′ 2 =(Σ 2, ℎ2, 𝛾2 ⊎𝛾 ′ 2 ⊎𝛾 ′′ 2 , 𝜙′ 2, 𝜉2,dom(𝜒)) – C1 =(Σ 1, ℎ1, 𝛾1, 𝜙1, 𝜉′ 1 : (Σ ′ 1 ⊢𝐾 : (·; ·;𝑇 ; 𝑖) → (· ; ·;𝑇 ′; 𝑖′)), 𝜃1) –C ′ 1 =(𝐾[𝐴], 𝑇 ′, 𝑖′,Σ 1 ∪Σ...

work page

[3] [3]

∈A Val(Σ;·;· ⊢ 𝑖 𝑉:𝑇) –(𝜒, 𝛾 ′′ 2 ) ∈A Val(Σ;·;· ⊢ℎ 2 ↾𝜎∪𝜇(𝐴) :heap) Therefore, C1 ∧ ∧C2 =((𝜉 1 ∧ ∧𝜉2) [𝑉], ℎ2 +ℎ 1){𝜄(𝛾 1 ⊎𝛾 2)} =C′ 2 ∧ ∧C′ 1 =((𝜉 2 ∧ ∧𝜉′

work page

[4] [4]

[𝐾[𝐴]],(𝜒+ℎ 1) +ℎ 2){𝛿(𝛾 1 ⊎ (𝛾 2 ⊎𝛾 ′ 2 ⊎𝛾 ′′ 2 ))} • (PQF). ThenC 2 (𝑓(𝐴),Σ 3,𝜒) − − − − − − − − − →C′ 2 andC 1 (𝑓(𝐴),Σ 3,𝜒) − − − − − − − − − →C′ 1, where –C 2 =(𝐾[𝑓 𝑉], 𝑖, 𝑇 ,Σ 2, ℎ2, 𝛾2, 𝜙2, 𝜉2, 𝜃2) – C′ 2 =(Σ 2, ℎ2, 𝛾2 ⊎𝛾 ′ 2 ⊎𝛾 ′′ 2 , 𝜙′ 2, 𝜉2 : (Σ 2 ⊢𝐾 : (·; ·;𝑇2; 𝑖3) → (·;·;𝑇;𝑖)),dom(𝜒)) –C 1 =(Σ 1, ℎ1, 𝛾1, 𝜙1, 𝜉1, 𝜎1) –C ′ 1 =(𝛾 1 (𝑓)𝐴, 𝑖 3, 𝑇2,...

work page

[5] [5]

□ Now we show the other direction of the invariance, i.e., that reductions in the composed term correspond to transitions in con- figurations

∈A Val(Σ 2;·;· ⊢ 𝑖2 𝑉:𝑇 1) –𝑖 3 =max(𝑖 1, 𝑖2) –(𝜒, 𝛾 ′′ 2 ) ∈A Val(Σ;·;· ⊢ℎ 2 ↾𝜎∪𝜇(𝐴) :heap) Therefore, C1 ∧ ∧C2 =((𝜉 1 ∧ ∧𝜉2) [𝐾[𝑓 𝑉]], ℎ 2 +ℎ 1){𝜄(𝛾 1 ⊎𝛾 2)} =C′ 2 ∧ ∧C′ 1 =(((𝜉 2 :(Σ 2 ⊢𝐾:(·;·;𝑇 2;𝑖 3) → (·;·;𝑇;𝑖))) ∧ ∧𝜉 1) [𝛾1 (𝑓)𝐴],(𝜒+ℎ 1) +ℎ 2){𝛿(𝛾 1 ⊎𝛾 2 ⊎𝛾 ′ 2 ⊎𝛾 ′′ 2 )} •The other cases are similar therefore omitted. □ Now we show the other direc...

work page 2017

[6] [6]

If any prefix of t′ contains at least as many (QB) actions as (A) actions, then by induction hypothesis we know that the number of (QB) actions in t′ is at most dep( #𝛾1 (𝑏) [𝜌])

SoC ′ 1 t′ − →C′′ 1 and C′ 2 t′ − →C′′ 2 , where t=(run𝑏 𝜌,Σ 3, 𝜒)t ′ and t′ consists only of (A) and (QB) actions. If any prefix of t′ contains at least as many (QB) actions as (A) actions, then by induction hypothesis we know that the number of (QB) actions in t′ is at most dep( #𝛾1 (𝑏) [𝜌]) . There- fore, the number of (QB) actions int is at mostdep( #...

work page

[7] [7]

is an active configuration whose next tran- sition is a 𝜏 transition, or (b)C ′ 1 (orC ′

work page

[8] [8]

In other words, there does not exist infinite sequences of𝜏-free transitions

is an active configuration whose next transition is a (PA) transition, andC ′ 2 (orC ′ 1, resp.) is a passive configuration whose stack 𝜉 is empty. In other words, there does not exist infinite sequences of𝜏-free transitions. Proof. We prove by case analysis on first step of transition the active configurationC 2. • (PQF). ThenC 2 (𝑓(𝐴),Σ 3,𝜒) − − − − − −...

work page

[9] [9]

In the former case, the next transition ofC ′ 1 is a 𝜏 transition ((𝜆𝑥 .𝑀 ′)𝐴, 𝜒+ℎ 1) → (𝑀 ′ [𝐴/𝑥], 𝜒+ℎ 1), and clause (a) holds

∈A Val(Σ 2;·;· ⊢ 𝑖2 𝑉:𝑇 1) The term in the new active configurationC′ 1 is 𝛾1 (𝑓)𝐴 , where 𝛾1 (𝑓) is either 𝜆𝑥 .𝑀′ or 𝑓 ′ for some 𝑓 ′ ∈FNames 𝑇1→𝑇2,𝑖1. In the former case, the next transition ofC ′ 1 is a 𝜏 transition ((𝜆𝑥 .𝑀 ′)𝐴, 𝜒+ℎ 1) → (𝑀 ′ [𝐴/𝑥], 𝜒+ℎ 1), and clause (a) holds. In the latter case, the next transition ofC ′ 1 is a (PQF) transition (𝑓 ′...

work page

[10] [10]

If there are multiple such 𝑖s, we choose the smallest one

is the smallest. If there are multiple such 𝑖s, we choose the smallest one. As a (QB) action increases siz(𝜉 𝑖

work page

[11] [11]

by one, and an (A) action decreases siz(𝜉 𝑖

work page

[12] [12]

By Lemma 19, this trace contains at most dep(𝑀 𝑖 ) (QB) actions, where 𝑀𝑖 is the term in the active configuration

by one, we know that the trace starting fromC 𝑖 1 andC 𝑖 2 always contains at least as many Layered Modal ML: Syntax and Full Abstraction Conference’17, July 2017, Washington, DC, USA (QB) actions as (A) actions. By Lemma 19, this trace contains at most dep(𝑀 𝑖 ) (QB) actions, where 𝑀𝑖 is the term in the active configuration. Therefore, this trace cannot ...

work page 2017

[13] [13]

By induction bypothesis,C ′ 2 ∧ ∧C′ 1 ⇓0

ThenC ′ 2 | C′ 1 ↓t′ . By induction bypothesis,C ′ 2 ∧ ∧C′ 1 ⇓0. SupposeC 2 𝜏 − → ∗ C′′ 2 a − →C′ 2, and, obviously, C1 a − →C′

work page

[14] [14]

By Lemma 17, C1 ∧ ∧C′′ 2 =C ′ 2 ∧ ∧C′

By Lemma 16,C 1 ∧ ∧C2 →∗ C1 ∧ ∧C′′ 2 . By Lemma 17, C1 ∧ ∧C′′ 2 =C ′ 2 ∧ ∧C′

work page

[15] [15]

Then we prove ifC 1 ∧ ∧C2 ⇓0 thenC 1|C2 ↓t by induction on the number of steps in the reductionC 1 ∧ ∧C2 →∗ (𝑉 , ℎ′)

Therefore,C 1 ∧ ∧C2 ⇓0. Then we prove ifC 1 ∧ ∧C2 ⇓0 thenC 1|C2 ↓t by induction on the number of steps in the reductionC 1 ∧ ∧C2 →∗ (𝑉 , ℎ′). If there are 0 steps, then 𝑀 is a value, so empty trace is the t we are looking for. Otherwise,C 1 ∧ ∧C2 → (𝑀 ′′, ℎ′′) → ∗ (𝑉 , ℎ′). By Lemma 20, without loss of generality, there existsC ′ 1,C ′ 2 such thatC 1 t′ −...

work page

[16] [16]

if(𝑥=𝐴)then()elseΩ

ThenC ′ 1 ∧ ∧C′ 2 ⇓0 as well, and by induction hypothesis we haveC 1|C2 ↓t′′ . Therefore, C1|C2 ↓t′ t′′ . □ The above result can be instantiated to initial configurations for programs and contexts to yield the following theorem. Theorem 12 (Correctness, Theorem 4).For any term Σ; Ψ; Γ⊢ 𝑖 𝑀 : 𝑇 , evaluation context Σ′ ⊢𝐾 : (·; ·; 𝑖;𝑇) → (· ; ·; 𝑖′;𝑇 ′), gl...

work page 2017