Space-Efficient Gradual Typing in Coercion-Passing Style

Atsushi Igarashi; Tomoya Tabuchi; Yuya Tsuda

REVIEW 2 major objections 5 minor 26 references

Space-Efficient Gradual Typing in Coercion-Passing Style

T0 review · 2 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Coercion-passing style lets gradual-typing compilers keep tail calls in constant space without changing observable behavior.

desk verdict A solid, well-proved coercion-passing translation with an honest implementation study—but the main theorem covers a variant of λS, not the original, and the abstract oversells the match. read the letter →

arxiv 1908.02414 v2 pith:IOCEM4L6 submitted 2019-08-07 cs.PL

Yuya Tsuda , Atsushi Igarashi , Tomoya Tabuchi This is my paper · ORCID

classification cs.PL

keywords gradualtypingcoercion-passingstylespaceefficiencyfirst-classcoercionstail-calloptimizationcoercioncompositionoperationalsemanticsblametracking

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Gradually typed languages insert run-time checks where statically typed and dynamically typed code meet; when such checks sit at tail positions, they can break tail-call optimization and make recursive programs use space proportional to the recursion depth. This paper claims that the problem can be solved by translating programs into coercion-passing style: every function receives an extra argument that carries "the rest of the run-time checks," and checks are composed eagerly before the call instead of accumulating after it. The authors formalize this as a translation from the space-efficient coercion calculus $\lambda S$ to a new calculus $\lambda S_1$ with first-class coercions, and prove that the translation preserves semantics: a closed base-type term evaluates to a value, diverges, or produces the same blame error exactly when its translation does. Implemented in an existing gradual-typing compiler, the translation prevents stack overflow on tail-recursive programs at the cost of up to 3 times slower execution for most partially typed benchmark configurations.

What carries the argument

The mechanism is the continuation coercion: the extra parameter $\kappa$ added to every translated function, which carries "the rest of the run-time checks" just as a CPS continuation carries the rest of the computation. The translation $\mathcal{K}\llbracket M\rrbracket_K$ turns a source term $M$ together with a continuation coercion $K$ into a $\lambda S_1$ term, while the auxiliary $C\llbracket M\rrbracket$ avoids wrapping values and coercion applications in administrative identity coercions; the object-level operator $M\;;\;N$ computes the composition $s\#t$ at run time. The type constructor $A\Rightarrow B$ packages the extra argument: it is the type of a function that takes an $A$ and a coercion from $B$ to some fresh target type, so one function can be called with continuation coercions of different target types. These pieces together replace the nonstandard (R-MergeC) rule of $\lambda S$ with a standard call-by-value semantics in which coercions have already been composed before the recursive call happens.

What would settle it

Run the mutually recursive even/odd benchmark with both return types set to the dynamic type, using the translated compiler with a fixed stack limit (the paper uses 8 MB), and increase the input $n$; if the program overflows the stack for large $n$, the claim that the translation prevents stack overflow is false. Formally, a closed base-type $\lambda S$ term $M$ for which $M$ terminates but $C\llbracket M\rrbracket$ diverges, or vice versa, would contradict Theorem 15.

Watch

Extended reading notes

Core claim

The paper's central discovery is that eager coercion composition can be moved from a nonstandard reduction rule into an ordinary call-by-value translation. The translation sends $\lambda S$ terms to $\lambda S_1$ terms; $\lambda S_1$ uses first-class coercions and function types $A\Rightarrow B$, where a call supplies not only an argument of type $A$ but also a continuation coercion $\kappa$ of type from $B$ to a fresh target type, which is applied to the value the function returns. A source coercion application $M\langle s\rangle$ is translated as a let-expression that first composes $\Psi(s)$ with the current continuation coercion $K$ and then runs the translation of $M$ with that composition; a source $\lambda x.M$ becomes $\lambda(x,\kappa).(\mathcal{K}\llbracket M\rrbracket_\kappa)$. The correctness theorem (Theorem 15) states that a closed base-type term evaluates to a constant, diverges, or blames exactly when its translation does. The simulation proof removes only the administrative identity coercions that the translation itself introduces—the auxiliary function $C\llbracket M\rrbracket$ is what keeps values and coercion applications from being wrapped in spurious identities—so each source redex is matched by a target redex. Because $\lambda S_1$ is an ordinary call-by-value calculus without the nonstandard context rule of $\lambda S$, the result is a semantics that a compiler can implement directly.

Load-bearing premise

The correctness proof covers a modified version of the earlier $\lambda S$ calculus, not the original as published, and the stack-overflow experiments assume the C compiler performs tail-call optimization; if the modification changes observable behavior, the link to the original space-efficient semantics is not fully established.

Editorial extensions

If this is right

Any call-by-value compiler that can represent coercions as first-class values can implement the space-efficient semantics of gradual typing without a nonstandard reduction rule or nonstandard evaluation contexts.
Tail-recursive gradually typed programs that cross the typed/untyped boundary will no longer accumulate run-time checks on the stack, so they can run in constant space like unchecked programs.
Because the translation preserves evaluation to a value, divergence, and blame, it can serve as a semantics-preserving compilation phase: programs' observable behavior does not change.
The measured cost of the extra coercion parameter is up to 3 times slower execution for most partially typed practical programs, with heavier overhead in call-heavy programs such as tak and even-odd.
Over-optimizing the translation—removing identity coercions that were present in the original program—breaks the simulation property, so a correct implementation must remove only administrative identities.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Not claimed by the paper, but the reported slowdown upper bound comes from a first implementation; specializing the common case where the continuation coercion is the identity could reduce the gap, since the paper itself notes some configurations run faster for unexplained reasons.
The same recipe should transfer to other blame-tracking cast or contract systems that have a compact coercion composition operation; whether the overhead pattern of roughly 3x carries over is a testable empirical question.
Because the target calculus is deliberately restricted (coercions for coercion types may only be identities, and variables cannot appear under coercion constructors), lifting those restrictions could give a more general first-class-coercion calculus; the paper lists this as future work.
If the modified source calculus is observationally different from the original $\lambda S$, a bridge theorem connecting the two would be needed for the stated claim that the translation implements the original space-efficient semantics; the experiments cannot settle this because they compile the modified variant.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Colleague,

This paper is worth your time if you care about space-efficient gradual typing. The authors introduce λS1, a first-class coercion calculus, give a CPS-style translation from the space-efficient coercion calculus λS to λS1, prove a simulation result, and implement it in Grift. The stack-overflow fix is real: the even/odd benchmark no longer blows the stack, and the cost is up to 3x slowdown, which is honestly reported.

The formal core is genuinely good. The target calculus is a natural fit for coercion-passing, the distinction between U⟨s⟩ and U⟨⟨d⟩⟩ is used well, and the simulation proof in the appendix looks careful. The lemmas about evaluation contexts and the elimination of administrative coercions are the right machinery. I believe the correctness statement for the variant is solid.

The soft spot is the exact claim about the source calculus. The paper's abstract and contributions say 'from λS by Siek et al.' But Section 2.1 changes the grammar: ground coercions in this λS include id_A for every non-⋆ type and exclude 'virtually identity' coercions like id_ι→id_ι. The translation is not total on the original calculus: Ψ(id_ι→id_ι) = id_ι⇒id_ι, and λS1's ground coercions don't allow s⇒t when both s and t are identities (Figure 6). So any original typing derivation that uses CT-Fun with id_ι→id_ι—for example a value U⟨⟨id_ι→id_ι⟩⟩—cannot be translated. The paper explicitly says the variant is chosen 'to simplify our proof,' and it claims the two calculi are extensionally the same, but no equivalence proof is given. That means Theorem 15 is proved for the variant, not for the λS that the literature knows. This is a real gap in the paper's framing, and it should be fixed—either by extending the translation to handle virtually identity coercions (or normalizing them away) or by clearly stating the results are for the modified calculus. It is not a fatal flaw in the technique, but it is a flaw in the advertised result.

Minor issues: the implementation relies on clang's tail-call optimization, excludes recursive types, and the code doesn't appear to be released. The benchmarks are honest but limited. None of these change my read.

This paper deserves a serious referee. I'd send it to review, with the expectation that the authors address the scope mismatch before publication.

Referee Report

2 major / 5 minor

Summary. The paper studies coercion-passing style as a way to implement space-efficient gradual typing. It introduces λS1, a call-by-value calculus with first-class coercions and continuation coercions, and defines a translation from a variant of Siek et al.'s space-efficient coercion calculus λS into λS1. The main formal result, Theorem 15, states that for closed base-type terms the translation preserves evaluation to a constant, blame, and divergence; the proof is built on a simulation lemma (Lemma 17) supported by detailed appendix proofs. The paper also reports an implementation in the Grift compiler and benchmark results showing that stack overflow can be avoided at the cost of up to 3 times slower execution for most partially typed configurations.

Significance. If the source-calculus scope is clarified, this is a solid contribution to gradual typing implementation. The paper gives a formal coercion-passing translation for a space-efficient coercion calculus, proves type preservation, progress, and preservation for both calculi, and proves a nontrivial simulation property with careful treatment of administrative coercions. The proof details are extensive, and the evaluation is honest about disclosed limitations such as the exclusion of recursive types and reliance on C-level tail-call optimization. The up-to-3× overhead measurement is a useful data point for the community. The main weakness is that the correctness theorem is proved for a modified λS rather than Siek et al.'s original calculus, while the abstract and parts of the introduction claim the original.

major comments (2)

[§2.1, §3.1, Figure 9, Theorem 15] The correctness theorem is not proved for Siek et al.'s original λS. Section 2.1 states that this paper's λS differs from the original in that ground coercions include identity coercions for every function type and exclude 'virtually identity' coercions such as id_ι→id_ι, whose reduction behavior is said to differ although they are extensionally the same. The translation of Figure 9 is thereby not total on original λS type derivations: Figure 6 does not admit id_ι⇒id_ι as a coercion because the arrow-coercion clause requires s≠id or t≠id, while Ψ(id_ι→id_ι) = id_ι⇒id_ι, so any term containing U⟨⟨id_ι→id_ι⟩⟩ has no translation under the given rules. Consequently Theorem 15 and Lemma 17 establish preservation only for the modified calculus, and the abstract's 'from λS by Siek et al.' overstates the result. Please either prove that the modified calculus is observationally equivalent to the original λS, or restrict the title, abstract, and introduction to the variant and state the restriction explicitly wherever Theorem 15 is invoked.
[§5.1] Section 5.1 says that Grift's coercion semantics is the D semantics while λS1 is UD, and dismisses the difference because 'the main difference is in the coercion composition.' Since the experiments are used to claim that the λS1 semantics can be implemented and prevents stack overflow, the paper should provide either an implementation of the UD semantics or a clear argument (with, ideally, a targeted experiment) that the D/UD difference cannot affect the tail-call behavior measured in Section 5.2 and Section 5.3.

minor comments (5)

[§5.2] The displayed code `(- n ⟨int?p2⟩1)` and `(if (= 0 n ⟨int?p1⟩)` appear malformed; please check the placement of parentheses and arguments.
[§5.2] The phrase 'it is our surprise' should be rephrased to 'surprisingly' or 'to our surprise'.
[Appendix A, proof of Theorem 10] In the case for T-Cmp, the proof says 'Take M′ = s # t by (R-Op)' but the applicable reduction rule is (R-Cmp), not (R-Op).
[§3.1] The paper uses A↝ B both for the coercion-judgment relation and as a type constructor in λS1; this is potentially confusing and deserves an explicit remark distinguishing the two uses.
[§5.3, Appendix B] The scatter plots in Figure 12 are not referenced in the body of Section 5.3; please cite them when discussing per-benchmark behavior.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the target semantics and the translation are independently defined, and Theorem 15 is proved by simulation; the λS-variant scope gap is a correctness concern, not a circular one.

full rationale

The paper's derivation chain is self-contained against independently defined inputs. The source calculus λS (with the Section 2.1 variant) has its own syntax, typing rules, and reduction semantics; the target calculus λS1 is a newly defined calculus with its own syntax and operational semantics; and the coercion-passing translation is given by explicit rules in Figure 9. Correctness is established by a simulation lemma (Lemma 17) and Theorem 15, whose proofs use auxiliary lemmas about coercion composition, substitution, and evaluation contexts rather than assuming the conclusion. No parameter is fitted to the experimental results: the benchmarks measure stack overflow and runtime ratios after the translation, and those outcomes are not used as inputs to the formal construction. The only notable caveat is that Section 2.1 changes Siek et al.'s λS by adding identity coercions id_A for all function types and excluding virtually identity coercions such as id_ι→id_ι, so Theorem 15 is proved for this modified calculus rather than for the original λS exactly. This is a scoping or correctness gap regarding the advertised 'from λS by Siek et al.' claim, not circularity: the theorem's hypotheses do not contain its conclusion, and no self-citation is load-bearing. Prior work supplies the problem setting and the source calculus, but the translation's correctness proof is original and does not reduce to a prior unverified result.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper introduces a new calculus lambda S1 but no free parameters or invented physical entities. The theoretical results rely only on standard proof techniques and the explicitly stated semantic choices.

assumptions (4)

ad hoc to paper The modified lambda S, which adopts id_A for all A and excludes virtually identity coercions, is a faithful enough presentation of the space-efficient semantics.
Section 2 states the definition differs from the original and that the change is made to simplify the proof. The paper does not prove full equivalence to the original lambda S.
domain assumption The C compiler (clang -O3) performs tail-call optimization on the generated C code, which is required for constant-space execution.
Section 5.1: 'the implementation ... relies on the C compiler to perform tail-call optimizations.'
domain assumption The Grift compiler's run-time check scheme D is close enough to lambda S1's UD that the modification is sound.
Section 5.1: 'Since the main difference is in the coercion composition, our technique can be applied to Grift.'
standard math Standard induction and substitution lemmas for the calculi.
Used throughout Appendix A proofs, e.g., Lemma A.20 and Lemma A.21.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Space-Efficient Gradual Typing in Coercion-Passing Style." pith.science (2026). https://pith.science/paper/IOCEM4L6

@misc{pith2026190802414,
  author       = {Pith},
  title        = {Pith review of: Space-Efficient Gradual Typing in Coercion-Passing Style},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IOCEM4L6}},
  note         = {Machine review of arXiv:1908.02414}
}

abstract

Herman et al. pointed out that the insertion of run-time checks into a gradually typed program could hamper tail-call optimization and, as a result, worsen the space complexity of the program. To address the problem, they proposed a space-efficient coercion calculus, which was subsequently improved by Siek et al. The semantics of these calculi involves eager composition of run-time checks expressed by coercions to prevent the size of a term from growing. However, it relies also on a nonstandard reduction rule, which does not seem easy to implement. In fact, no compiler implementation of gradually typed languages fully supports the space-efficient semantics faithfully. In this paper, we study coercion-passing style, which Herman et al. have already mentioned, as a technique for straightforward space-efficient implementation of gradually typed languages. A program in coercion-passing style passes "the rest of the run-time checks" around---just like continuation-passing style (CPS), in which "the rest of the computation" is passed around---and (unlike CPS) composes coercions eagerly. We give a formal coercion-passing translation from $\lambda$S by Siek et al. to $\lambda$S$_1$, which is a new calculus of first-class coercions tailored for coercion-passing style, and prove correctness of the translation. We also implement our coercion-passing style transformation for the Grift compiler developed by Kuhlenschmidt et al. An experimental result shows stack overflow can be prevented properly at the cost of up to 3 times slower execution for most partially typed practical programs.

Figures

Figures reproduced from arXiv: 1908.02414 by the authors.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

26 extracted references · 25 canonical work pages

[1]

If i : A↝ B then A⁄=⋆

work page
[2]

If g : A↝ B, then A⁄=⋆and B⁄=⋆and A∼G and G∼B for some uniqueG. Proof. (1) By case analysis oni with (2). (2) By case analysis ong. ◀ ▶ Proposition A.1. Coercion compositions # t is terminating. Proof. The sum of sizes of two arguments gets smaller at each recursive call of#. ◀ ▶ Lemma 2. If s : A↝ B and t : B↝ C, then (s # t) : A↝ C. Proof. We prove the ...

work page
[3]

M = blame p for some p. Proof. By induction on the derivation of∅⊣S M : A with case analysis on the rule applied last. ◀ ▶ Lemma 4 (Determinacy). If M↦−→S N and M↦−→S N′, then N = N′. Proof. By Lemma A.3. ◀ We state type safety forλS with auxiliary lemmas. Y. Tsuda, A. Igarashi, and T. Tabuchi 8:31 ▶ Lemma A.4 (Canonical Forms). If∅⊣S V : A, then one of t...

work page
[5]

Similar

V = s and A = A1↝ A2 for some s, A1, A2. Proof. By case analysis on the typing rule applied to∅⊣S1 V : A. ◀ In the proof of the following theorem, we only write down case(T-Op) in detail and write “Similar.” for the other cases. ▶ Theorem 10 (Progress). If∅⊣S1 M : A, then one of the following holds: (1)M↦−→S1 M′ for some M′; (2) M = V for some V; or (3)M ...

work page
[7]

V =λx.M and A = A1→A2 for some x, M, A1, A2

work page
[8]

V = U⟨⟨s→t⟩⟩and A = A1→A2 for some U, s, t, A1, A2

work page
[9]

▶ Theorem 5 (Progress)

V = U⟨⟨g; G!⟩⟩and A =⋆for some U, g, G. ▶ Theorem 5 (Progress). If∅⊣S M : A, then one of the following holds: (1)M↦−→S M′for some M′; (2) M = V for some V; or (3)M = blame p for some p. Proof. By Lemma A.3. ◀ ▶Lemma A.5(Preservation of Types under Substitution). If Γ, x : A⊣S M : B and Γ⊣S V : A, then Γ⊣S M[x := V ] : B. ▶ Lemma A.6 (Preservation for Redu...

work page 2020
[10]

There uniquely exist a redexM1 and an evaluation contextE such that M =E[M1]

work page

Show all 26 references

[11]

M = blame p for some p. Proof. Similarly for Theorem 10.15 ◀ ▶ Lemma 9 (Determinacy). If M↦−→S1 N and M↦−→S1 N′, then N = N′. Proof. By Lemma A.10. ◀ We state type safety forλS1 with auxiliary lemmas. We omit inversion lemmas for the typing judgments. ▶ Lemma A.11 (Canonical F...
[12]

V = a and A =ιfor some a,ι
[13]

V =λ(x,κ).M and A = A1⇒A2 for some x,κ,M, A1, A2
[14]

V = U⟨⟨s⇒t⟩⟩and A = A1⇒A2 for some U, s, t, A1, A2
[15]

V = U⟨⟨g; G!⟩⟩and A =⋆for some U, g, G
[17]

E[N11] = (op(□, N2))[E1[N11]] = (op(□, N2))[N1] = op(N1, N2) E[N′ 11] = op(N′ 1, N2) By (E-Ctx) withE = (op(□, N2))[E1], we haveop(N1, N2)↦−→op(N′ 1, N2)

TakeE = (op(□, N2))[E1] by Lemma A.8. E[N11] = (op(□, N2))[E1[N11]] = (op(□, N2))[N1] = op(N1, N2) E[N′ 11] = op(N′ 1, N2) By (E-Ctx) withE = (op(□, N2))[E1], we haveop(N1, N2)↦−→op(N′ 1, N2). Take M′= op(N′ 1, N2). Subsubcase (E-Abort) : We are given N1 =E1[blame p] N′ 1 = bl...

2020
[18]

Then, (T-Let) and (T-App) ﬁnish this case

By (T-Crc) and (T-Cmp), we have ∅⊣V⟨s⟩: A′ 1 ∅⊣t ;; W : A′ 2↝ A. Then, (T-Let) and (T-App) ﬁnish this case. Case (R-Let) : We are given M = let x = V in M1 N = M1[x := V ] for some x, V, M1. By inversion on∅⊣let x = V in M1 : A, ∅⊣V : A1 x : A1⊣M1 : A for some A1. By Lemma A.1...

2020
[19]

If Γ⊣S M : A and s : A↝ B , then Ψ(Γ) ⊣S1 (K JM KΨ( s)) : Ψ( B)
[20]

If Γ⊣S V : A, then Ψ(Γ) ⊣S1 Ψ( V ) : Ψ( A). Proof. Simultaneously proved by induction on the derivation ofΓ⊣S M : A and Γ⊣S V : A. ◀ A.4 Translation Preserves Semantics ▶ Lemma A.15 (Composition). If s # t = s′in λS, then Ψ( s) # Ψ( t) = Ψ( s′). Proof. By induction on the deri...

2020
[21]

C JM K[x := Ψ( V )] = C JM[x := V ]K
[22]

If x /∈FV (K), then (K JM KK)[x := Ψ( V )] = K JM[x := V ]KK. Proof. The two items are simultaneously proved by induction on the derivations ofC JM K and K JM KK. (1) By case analysis on the form ofM. We ﬁrst consider the cases whereM is a value: M = W. We must showΨ( W )[x :=...

2020
[23]

For anyF, there existsE′such that for anyM, C JF[M]K =E′[C JM K]
[24]

For anyF and s, there existsE′such that for anyM, C JF[M⟨s⟩]K =E′[K JM KΨ( s)]. Proof. Two items are simultaneously proved by induction on the structure ofF. (1) By case analysis on the structure ofF. CaseF =□ : By□[M] = M, we must showC JM K =E′[C JM K]. TakeE′=□. CaseF =F1[o...

2020
[25]

If M e −→S N , then K JM KK e ↦−→S1 c ↦−→∗ S1 K JN KK
[26]

If M c −→S N, then C JM K c ↦−→+ S1 C JN K. Proof. (1) By case analysis on the reduction rule applied toM e −→S N. Case (R-Op) : We are given M = op(a1, a2) N = a δ(op, a1, a2) = a ECOOP 2020 8:44 Space-Eﬃcient Gradual Typing in Coercion-Passing Style for some op, a1, a2, a. W...

2020
[27]

If M e ↦−→S N, then C JM K e ↦−→S1 c ↦−→∗ S1 C JN K
[28]

M e S // C J_K N C J_K C JM K e S1 // c ∗ S1 // C JN K M c S // C J_K N C J_K C JM K c + S1 // C JN K Proof

If M c ↦−→S N, then C JM K c ↦−→+ S1 C JN K. M e S // C J_K N C J_K C JM K e S1 // c ∗ S1 // C JN K M c S // C J_K N C J_K C JM K c + S1 // C JN K Proof. (1) By case analysis on the evaluation rule applied toM e ↦−→S N. Case (E-CtxE) withE =F : We are given M1 e −→S N1 M =F[M1...

2020
[2015]

38 Jeremy G

doi:10.1145/2737924.2737968. 38 Jeremy G. Siek and Philip Wadler. Threesomes, with and without blame. InProceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 365–376, 2010.doi:10.1145/1...

2010

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

If i : A↝ B then A⁄=⋆

work page

[2] [2]

If g : A↝ B, then A⁄=⋆and B⁄=⋆and A∼G and G∼B for some uniqueG. Proof. (1) By case analysis oni with (2). (2) By case analysis ong. ◀ ▶ Proposition A.1. Coercion compositions # t is terminating. Proof. The sum of sizes of two arguments gets smaller at each recursive call of#. ◀ ▶ Lemma 2. If s : A↝ B and t : B↝ C, then (s # t) : A↝ C. Proof. We prove the ...

work page

[3] [3]

M = blame p for some p. Proof. By induction on the derivation of∅⊣S M : A with case analysis on the rule applied last. ◀ ▶ Lemma 4 (Determinacy). If M↦−→S N and M↦−→S N′, then N = N′. Proof. By Lemma A.3. ◀ We state type safety forλS with auxiliary lemmas. Y. Tsuda, A. Igarashi, and T. Tabuchi 8:31 ▶ Lemma A.4 (Canonical Forms). If∅⊣S V : A, then one of t...

work page

[4] [5]

Similar

V = s and A = A1↝ A2 for some s, A1, A2. Proof. By case analysis on the typing rule applied to∅⊣S1 V : A. ◀ In the proof of the following theorem, we only write down case(T-Op) in detail and write “Similar.” for the other cases. ▶ Theorem 10 (Progress). If∅⊣S1 M : A, then one of the following holds: (1)M↦−→S1 M′ for some M′; (2) M = V for some V; or (3)M ...

work page

[5] [7]

V =λx.M and A = A1→A2 for some x, M, A1, A2

work page

[6] [8]

V = U⟨⟨s→t⟩⟩and A = A1→A2 for some U, s, t, A1, A2

work page

[7] [9]

▶ Theorem 5 (Progress)

V = U⟨⟨g; G!⟩⟩and A =⋆for some U, g, G. ▶ Theorem 5 (Progress). If∅⊣S M : A, then one of the following holds: (1)M↦−→S M′for some M′; (2) M = V for some V; or (3)M = blame p for some p. Proof. By Lemma A.3. ◀ ▶Lemma A.5(Preservation of Types under Substitution). If Γ, x : A⊣S M : B and Γ⊣S V : A, then Γ⊣S M[x := V ] : B. ▶ Lemma A.6 (Preservation for Redu...

work page 2020

[8] [10]

There uniquely exist a redexM1 and an evaluation contextE such that M =E[M1]

work page