Gradual Metaprogramming

Arnaud Venet; Chao-Hong Chen; Darshal Shetty; Jeremy G. Siek; Rocky Liu; Tianyu Chen; Weixi Ma

REVIEW 2 major objections 6 minor 11 references

Gradual Metaprogramming

T0 review · 2 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read A gradually typed metaprogramming calculus can guarantee that successful code generation never produces an ill-typed object program.

desk verdict A clean, mechanized reference calculus for gradual metaprogramming; the type-safety result is real but the claimed object-language agnosticism is not supported by the STLC-specific development. read the letter →

arxiv 2506.09043 v3 pith:TS5JZ242 submitted 2025-06-10 cs.PL

Tianyu Chen , Darshal Shetty , Jeremy G. Siek , Chao-Hong Chen , Weixi Ma , Arnaud Venet , Rocky Liu This is my paper

classification cs.PL

keywords gradualmetaprogrammingtypingquoteandsplicetypesafetyblametrackingdatapipelineDSLscoercionsAgdamechanization

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

Data engineers write Python-embedded DSLs that generate SQL or machine-learning pipeline code, and type mismatches in the generated code are usually found only at deployment, far from the line that caused them. This paper proposes gradual metaprogramming: a gradually typed metalanguage with quote and splice that type-checks code fragments at the moment they are spliced together, and blames the exact source location when a cast fails. The calculus MetaGTLC is given semantics by compilation to a cast calculus MetaCC with explicit coercions; the central theorem is that metaevaluation of a well-typed metaterm never produces an ill-typed object program (if it produces a quoted term at all, that term is well typed). This gives a migration path from fully dynamic metaprograms to fully static ones, with earlier error detection at each step. MetaGTLC, MetaCC, and the type-safety proof are mechanized in Agda.

What carries the argument

The central mechanism is the compilation function from MetaGTLC to MetaCC, which inserts coercions at every point where a metaterm's type is only consistent with the expected type rather than equal to it. Coercions are combinators of the form $\vdash c : A \Rightarrow B$: identities, injections into $\star$, projections out of $\star$ with blame labels, function coercions, and sequencing; MetaCC adds code-level variants $\mathsf{code!}_T$ and $\mathsf{code?}_{\ell,T}$ between $\mathsf{Code}\,\star$ and $\mathsf{Code}\,T$. Splice is checked bidirectionally, so when $\sim^\ell M$ appears in an object term, the typing context supplies the expected object type $T$ and compilation inserts $\mathsf{coerce}\,A\,(\mathsf{Code}\,T)\,\ell$ around $M$. The operational semantics then does the checking: matching injection/projection pairs cancel, mismatched pairs raise blame $\ell$, and blames propagate out of splices and quotes. The theorem rides on this machinery because the generated object term is validated exactly at the moment its type ceases to be unknown.

What would settle it

Run the paper's own Example 2.1 under the implementation: the theory predicts the splice of a quoted string into an integer context blames the splice location and never yields the ill-typed query; a run that produced the ill-typed query, or a well-typed MetaGTLC term that reduced to a stuck non-value in MetaCC, would refute Theorem 6.6.

Watch

Extended reading notes

Core claim

The paper's central claim, Theorem 6.6, is that MetaGTLC is type safe in exactly the sense data engineers need: if $\emptyset \vdash_m M : \mathsf{Code}\,T$ and metaevaluation of $M$ yields a quoted term, that term is well typed at $T$. The argument has four load-bearing pieces: a type-preserving compilation from MetaGTLC into MetaCC, progress and preservation for MetaCC, and a canonical-form lemma showing that any value of type $\mathsf{Code}\,T$ is a quoted simply typed $\lambda$ term. The genuinely new ingredient is that the standard gradual-typing relations extend to code types: consistency between $\mathsf{Code}\,\star$ and $\mathsf{Code}\,T$, coercions $\mathsf{code!}_T$ and $\mathsf{code?}_{\ell,T}$, and a bidirectional typing rule for splice that lets the surrounding object code determine the target type of the inserted cast. The discovery, in short, is that an explicitly cast version of gradual metaprogramming exists and has the MetaML-style well-typed-code guarantee while still tolerating unknown types in the generating program.

Load-bearing premise

The type-safety proof is carried out only for the simply typed lambda calculus as the object language, and the paper's assertion that MetaGTLC is agnostic to the object language is a design choice rather than a stated genericity theorem, so the guarantee as written does not automatically transfer to SQL, Spark, or feature-engineering DSLs with records, polymorphism, or subtyping.

Editorial extensions

If this is right

A metaprogram that is only partially annotated still gets checked during metaevaluation, so a type error inside a library is reported while the pipeline is being generated, not after it is deployed.
Blame labels identify the source location responsible for a cast failure, so a wrong argument type is attributed to the caller's code rather than to the library that raised the error.
If all annotations are added and the metaprogram type-checks statically, the generated object code is guaranteed well typed without needing runtime checks, recovering the MetaML-style guarantee in the simply typed setting.
Because ill-typed generated programs are prevented, developers can debug entirely in terms of the metaprogram source and usually never need to inspect the generated SQL or Spark code.

Reading between the lines

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

The formal theorem treats blame and divergence as well-typed outcomes, so the guarantee that matters in practice is conditional: whenever metaevaluation terminates with a quoted value, that value is well typed.
The calculus is proved against the simply typed lambda calculus as the object language; extending the same design to object languages with records, polymorphism, or subtyping would require new code coercions and new canonical-form arguments, so the claimed agnosticism to the object language is architectural, not yet a theorem.
The proof's divergence case invokes the law of excluded middle; the paper does not state whether the Agda mechanization postulates classical logic or reformulates that case constructively, so the mechanized statement is the place to check the classical step.
The same splice-boundary coercions suggest a general recipe: any property that can be attached to object-code types and checked by projection coercions could be enforced incrementally during metaevaluation, including schema well-formedness or information-flow labels.

Share X Bluesky LinkedIn Reddit HN

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

This paper gives the field something useful: a gradual metaprogramming calculus (MetaGTLC) that uses the standard gradual typing machinery (explicit ★, coercions in the style of λC) together with quote/splice and blame tracking. That combination is genuinely new relative to Miao and Siek's type-reflective calculus and to Yaguchi and Kameyama's parallel λG◦ work. The writing is clear, the related work is honest, and the central theorem is what it appears to be: well-typed MetaGTLC metaterms of type Code T, when metaevaluation succeeds without blame, produce well-typed STLC object terms. The proof is a standard progress/preservation argument plus compilation preservation, and the paper claims a full Agda mechanization with named files. That is a real, citable contribution, and the STLC theorem itself holds up.

The soft spots are proportionate. The biggest one is the mismatch between the introduction's claim that the calculus is 'agnostic to the details of the object language' and the actual development. Figure 4 fixes the object language to STLC; the bidirectional typing, the code reduction rules, the canonical-form lemma, and Theorem 6.6 all rely on STLC-specific facts. There is no object-language interface, no parameterization, and no genericity argument. So the paper's motivating promise about SQL/Spark/F3 pipelines is unsupported. That is a paper-level overclaim, not a flaw in the STLC result; the fix is to soften the wording or supply an interface. A second, minor issue: Theorem 6.6's proof invokes the law of excluded middle to classify divergence, and the paper does not explain how the Agda development handles that classical step. This is rephrasable as partial correctness and does not threaten the theorem. The artifact also lacks a commit hash, so the mechanization claim cannot be checked precisely; that is easy to remedy. The migration and backward-compatibility discussion is motivational rather than proved, which is fine as long as it is read that way.

Who gets value from this: PL researchers working on gradual typing, metaprogramming, or both, and language designers for embedded data pipeline DSLs who want a formal reference point. The paper deserves a serious referee; the STLC result is solid and the design space is worth documenting. I would ask the authors, in revision, to either provide an object-language interface or explicitly retract the generality claim, and to pin the artifact to a commit.

Recommendation: send it to peer review. My own verdict would be conditional on that genericity fix, but the core result is sound.

Referee Report

2 major / 6 minor

Summary. The paper proposes gradual metaprogramming as a way to debug dynamically-typed DSLs that generate statically-typed code, motivated by data pipeline languages such as SQL and Spark. It defines MetaGTLC, a calculus with a gradually-typed metalanguage and a statically-typed object language (chosen as simply-typed lambda calculus, STLC), with quote/splice constructs and blame tracking. The semantics is given by a typed compilation to a cast calculus MetaCC that extends the λC calculus with code coercions. The main result (Theorem 6.6) states that metaevaluation of a well-typed MetaGTLC term produces a well-typed result, and the proof is claimed to be mechanized in Agda.

Significance. If established, the result provides a new point in the design space of metaprogramming calculi: a gradual metalanguage generating statically-typed object code, with a machine-checked proof of type safety and blame tracking. The use of coercions and the explicit unknown type follows the standard GTLC approach, and the paper gives intuitive examples of earlier and more precise error detection. However, the formal development is specialized to STLC, so the more ambitious claims about object-language agnosticism and applicability to SQL/Spark pipelines are not supported by the theorems as stated. The paper's central proof is a standard progress-and-preservation argument, and its main value is as a clean, mechanized foundation that could be extended.

major comments (2)

[§1.2, Figures 4, 7, 8, Lemma 6.5] The statement in §1.2 that the calculus is 'agnostic to the details of the object language, just that it should be statically typed' is not substantiated by the formal development. The object language is fixed to STLC throughout: the typing rules (Figure 4), the reduction rules (Figure 7), the ground types and coercions (Figures 3 and 5), the coerce function (Figure 8), and the canonical-form lemma (Lemma 6.5) all rely on STLC-specific notions such as a fixed set of base types and the STLC reduction relation. No object-language interface, parameterization, or genericity theorem is provided. Consequently, the paper's motivating guarantee for SQL/Spark pipeline languages is not established; it is a claim about the STLC instantiation. I recommend either (a) abstracting the object language (e.g., via a type language with ground types and a reduction relation satisfying suitable properties) and proving the key lemmas polymorphically, or (b) explicitly scoping the claims to STLC and stating which features of the proof would need to change for richer object languages.
[§6, Theorem 6.6] The proof of Theorem 6.6 invokes the law of excluded middle to split the behaviour of M_c into value, blame, divergence, or stuck. This is a classical argument, and Definition 3.2 defines meta-eval as a total function with a divergence case, so the theorem as stated is inherently classical. Since the paper claims full mechanization in Agda (§1.5 and Lemmas 6.1, 6.2, 6.4, with file names Progress.agda, Preservation.agda, CompilePres.agda), it should report whether the formalization uses postulates or classical axioms, and state the exact theorem proved in Agda. If the theorem is proved constructively, please explain how the divergence case is handled (e.g., by a partial-function formulation or a coinductive definition).

minor comments (6)

[§1.5] The artifact URL does not include a commit hash or build environment information (Agda version, standard library version); please provide these to make the mechanization independently verifiable.
[Figure 8] The pattern-matching clauses for coerce ★ A and coerce A ★ overlap with the ground-type clauses (coerce ★ 𝐺 and coerce 𝐺 ★) when A is a ground type such as Code★; please state the intended rule priority or make the clauses disjoint.
[§2.1] The sentence 'the return value of read_c is bound to r' refers to a function named read_and_quote in Example 2.1; please fix the typo.
[§1.4] The sentence 'MetaGTLC is novel in the realm of metaprogramming languages...' is immediately followed by the acknowledgment that Miao and Siek [2010] is in the same category; consider rephrasing to match the more precise claim in §1.5, e.g., 'the first to use the standard GTLC approach with an explicit unknown type'.
[Figure 4] The metaterm grammar shows a mandatory annotation λx:A.M_m, while the text says omitted annotations default to ★; please add a note explaining how omitted annotations are elaborated.
[§6, Theorem 6.6] Because Figure 10 includes rule WT-diverge, the theorem's case for divergence is trivially true; stating the theorem in the form 'if meta-eval M_m = M_s then M_s is well-typed' would highlight the non-trivial content.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the type-safety theorem is proved from a newly defined calculus by standard syntactic methods and is mechanized in Agda, with no fitted inputs or self-citation chain doing the work.

full rationale

The paper defines MetaGTLC and MetaCC from scratch (Figures 3-10) and proves Theorem 6.6 by composing Lemma 6.4 (compilation preserves types), Lemma 6.3 (multi-step reduction preserves types), Lemma 6.5 (canonical form of quoted code), and Lemma 6.1 (progress). No parameter is fitted to data, no prediction is renamed from an input, and no target result appears in the premises of the proof. The stated conclusion, that successful metaevaluation yields a well-typed STLC object program, is a genuine theorem about the newly introduced calculus rather than an equivalent restatement of its definitions. The background citations, including the λC calculus of Siek et al. and the earlier Miao-Siek calculus, supply terminology and inspiration for the cast representation, but the present paper defines its own coercion syntax, typing rules, reduction rules, and compilation rules, and it reports a machine-checked proof of the main lemmas. The invocation of the law of excluded middle in Theorem 6.6 is a proof-technique observation about case classification, not a circular step. The paper's claim that the calculus is agnostic to the object language is broader than what is proved, since the formal development fixes the object language to STLC; however, an unsupported generalization is an overclaim, not a circularity. Under the review rules, concerns of that kind belong to correctness risk rather than to the circularity score.

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

The central theorem rests on standard PL metatheory: the cast calculus λC, classical logic for divergence, and the choice of STLC as the object language. No free parameters or invented entities are introduced; the calculi MetaGTLC and MetaCC are the paper's contribution, not unexplained assumptions.

assumptions (4)

standard math Law of excluded middle
Invoked explicitly in the proof of Theorem 6.6 to split on whether the compiled term reduces to a value, reduces to blame, diverges, or gets stuck. This is classical logic; in Agda it would require a postulate or a constructive reformulation, which the paper does not discuss.
standard math Meta-theory of the λC cast calculus (Siek et al. 2021)
MetaCC is defined as an extension of λC (§4); the paper relies on the standard coercion framework and its properties (progress/preservation structure) without redeveloping them.
domain assumption Simply-typed lambda calculus is an adequate stand-in for statically-typed data pipeline DSLs
§1.2 states the object language is STLC as 'a simple representative' and that the calculus is agnostic to object language details, but no generic object-language interface is given; all theorems are specialized to STLC.
domain assumption Call-by-value, left-to-right evaluation with frames
MetaCC's operational semantics (Figure 7) is CBV; the metaprogramming semantics and meta-eval function depend on this evaluation order, which may not match Python's semantics in the motivating DSLs.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Gradual Metaprogramming." pith.science (2026). https://pith.science/paper/TS5JZ242

@misc{pith2026250609043,
  author       = {Pith},
  title        = {Pith review of: Gradual Metaprogramming},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TS5JZ242}},
  note         = {Machine review of arXiv:2506.09043}
}

read the original abstract

Data engineers increasingly use domain-specific languages (DSLs) to generate the code for data pipelines. Such DSLs are often embedded in Python. Unfortunately, there are challenges in debugging the generation of data pipelines: an error in a Python DSL script is often detected too late, after the execution of the script, and the source code location that triggers the error is hard to pinpoint. In this paper, we focus on the scenario where a DSL embedded in Python (so it is dynamically-typed) generates data pipeline description code that is statically-typed. We propose gradual metaprogramming to (1) provide a migration path toward statically typed DSLs, (2) immediately provide earlier detection of code generation type errors, and (3) report the source code location responsible for the type error. Gradual metaprogramming accomplishes this by type checking code fragments and incrementally performing runtime checks as they are spliced together. We define MetaGTLC, a metaprogramming calculus in which a gradually-typed metalanguage manipulates a statically-typed object language, and give semantics to it by translation to the cast calculus MetaCC. We prove that successful metaevaluation always generates a well-typed object program and mechanize the proof in Agda.

Figures

Figures reproduced from arXiv: 2506.09043 by the authors.

**Figure 1.** Difficulty in debugging dynamically-typed metaprograms that generate data pipelines by translation to its cast calculus MetaCC. We prove type safety for MetaGTLC, which means successful metaevaluation will always generate a well-typed object program. We mechanize MetaGTLC, MetaCC, and the type safety proof in Agda. 1.1 Generating Data Pipelines and Challenges in Error Detection A data pipeline specifies the steps i… view at source ↗

**Figure 2.** Our proposed workflow of generating data pipelines using gradual metaprogramming and Moggi [Moggi et al. 1999]. MetaML shows that it is possible to obtain a strong type safety guarantee: if the metaprogram successful type checks, then the code generated during metaevaluation will also type check. MetaML obtains this guarantee by tracking the type of a code fragment and by manipulates code fragments in a purely fu… view at source ↗

**Figure 3.** Types of MetaGTLC. Consistency between metalanguage types this cast wraps scale in a proxy that checks whether the arguments and return values match the expected type. So when the function compose makes a function call to scale and scale returns ≺ false ≻, the proxy signals an error and blames the function application of compose on line 9 of Carol’s code. MetaGTLC enables modular error reasoning through blame track… view at source ↗

Figures from the paper (7 more)

**Figure 4.** Figure 4: Syntax and typing of the gradual metaprogramming calculus MetaGTLC 𝜆x .≺ 1 + ∼ (x⟨ 𝑐 ⟩) ≻ But what should be the target type of the cast? Bidirectional typing provide a mechanism for inferring that type from the code that surrounds the splice. In this case, the additi…

**Figure 5.** Figure 5: Syntax and typing of coercions casts from 𝐴 to 𝐵, with the sub-coercion 𝑑, which casts from 𝐵 to 𝐶, and forms a coercion from 𝐴 to 𝐶. Compared with 𝜆C, we introduce four new coercions between code types (highlighted in [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]

**Figure 6.** Figure 6: Syntax and typing of the cast calculus MetaCC in MetaGTLC terms into coercions (specifically, projections and code projections) in MetaCC terms. Compared with the bidirectional typing of the code terms in MetaGTLC, the typing for code terms is uni-directional in MetaCC…

**Figure 7.** Figure 7: Small-step operational semantics of MetaCC 5 Compilation From MetaGTLC to MetaCC In this section, we define the compilation from the gradual metaprogramming language MetaGTLC to its cast calculus MetaCC by inserting casts. We first define the coerce function that takes…

**Figure 8.** Figure 8: The “coerce” function that generates coercions between types We define a predicate Emptym Γ, which says that there is no metalanguage variable in the typing context Γ: Emptym ∅ Emptym Γ Emptym (Γ, 𝑥:otype 𝑇 ) “Progress” says that a well-typed MetaCC term is either a va…

**Figure 9.** Figure 9: Compilation rules from MetaGTLC to MetaCC ⊢ 𝑟 : 𝑇 WT-STLC ∅ ⊢𝑜𝑐 𝑀𝑠 : 𝑇 ⊢ 𝑀𝑠 : 𝑇 WT-blame ⊢ blame ℓ : 𝑇 WT-diverge ⊢ diverge : 𝑇 [PITH_FULL_IMAGE:figures/full_fig_p013_9.png]

**Figure 10.** Figure 10: Well-typed metaevaluation results 7 Conclusion In this paper, we proposed an improvement to the error detection of dynamically-typed DSLs that generate staticallytyped data pipeline descriptions. We introduced gradual metaprogramming, which incrementally type checks…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

11 extracted references · 8 canonical work pages

[6]

In GPCE ’10: Proceedings of the international conference on Generative programming and component engineering

Incremental Type-Checking for Type- Reflective Metaprograms. In GPCE ’10: Proceedings of the international conference on Generative programming and component engineering. TyDe ’25, October 12–18, 2025, Singapore, Singapore T. Chen et al. Eugenio Moggi, Walid Taha, Zine El-Abidine Benaissa, and Tim Sheard

work page 2025
[7]

doi:10.1017/S0956796821000101 Guy L

Blame and coer- cion: Together again for the first time.Journal of Functional Programming 31 (2021), e20. doi:10.1017/S0956796821000101 Guy L. Steele, Jr

doi:10.1017/s0956796821000101 2021
[1994]

Science of Computer Programming 22, 3 (June 1994), 197–230

Dynamic typing: syntax and proof theory. Science of Computer Programming 22, 3 (June 1994), 197–230. doi:10.1016/0167- 6423(94)00004-2 IBM

doi:10.1016/0167- 1994
[1995]

C++ Report 7, 4 (May 1995), 36–43

Using C++ template metaprograms. C++ Report 7, 4 (May 1995), 36–43. Reprinted in C++ Gems, ed. Stanley Lippman. Hiroto Yaguchi and Yukiyoshi Kameyama

work page 1995
[1997]

In PEPM ’97: Proceedings of the 1997 ACM SIGPLAN sym- posium on Partial evaluation and semantics-based program manipulation (Amsterdam, The Netherlands)

Multi-stage programming with explicit annotations. In PEPM ’97: Proceedings of the 1997 ACM SIGPLAN sym- posium on Partial evaluation and semantics-based program manipulation (Amsterdam, The Netherlands). ACM Press, New York, NY, USA, 203–

work page 1997
[2000]

Theoretical computer science 248, 1-2 (2000), 211–242

MetaML and multi-stage programming with explicit annotations. Theoretical computer science 248, 1-2 (2000), 211–242. David Vandevoorde and Nicolai M. Josuttis

work page 2000
[2010]

Technical Report PLT-TR- 2010-1

Reference: Racket. Technical Report PLT-TR- 2010-1. PLT Design Inc. https://racket-lang.org/tr1/. Ronald Garcia and Andrew Lumsdaine

work page 2010
[2013]

ACM SIGPLAN Notices 48, 9 (2013), 403–416

A practical theory of language-integrated query. ACM SIGPLAN Notices 48, 9 (2013), 403–416. Paul Crickard

work page 2013

Show all 11 references

[2021]

ACM Computing Surveys (CSUR) 54, 5 (2021), 1–38

Bidirectional typing. ACM Computing Surveys (CSUR) 54, 5 (2021), 1–38. Robert Bruce Findler and Matthias Felleisen. 2002.Contracts for Higher-Order Functions. Technical Report NU-CCS-02-05. Northeastern University. doi:10.1145/2502508.2502521 Matthew Flatt and PLT

2021
[2024]

Proceedings of the ACM on Programming Languages 8, PLDI (2024), 1609–1632

Quest Complete: The Holy Grail of Gradual Security. Proceedings of the ACM on Programming Languages 8, PLDI (2024), 1609–1632. doi:10.1145/3656442 James Cheney, Sam Lindley, and Philip Wadler

2024 doi
[2025]

In Proceedings of the 24th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences

Staged Gradual Typing. In Proceedings of the 24th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences. 94–104. Received 22 June 2025; accepted 23 July 2025

2025

Pith tools

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

[1] [6]

In GPCE ’10: Proceedings of the international conference on Generative programming and component engineering

Incremental Type-Checking for Type- Reflective Metaprograms. In GPCE ’10: Proceedings of the international conference on Generative programming and component engineering. TyDe ’25, October 12–18, 2025, Singapore, Singapore T. Chen et al. Eugenio Moggi, Walid Taha, Zine El-Abidine Benaissa, and Tim Sheard

work page 2025

[2] [7]

doi:10.1017/S0956796821000101 Guy L

Blame and coer- cion: Together again for the first time.Journal of Functional Programming 31 (2021), e20. doi:10.1017/S0956796821000101 Guy L. Steele, Jr

doi:10.1017/s0956796821000101 2021

[3] [1994]

Science of Computer Programming 22, 3 (June 1994), 197–230

Dynamic typing: syntax and proof theory. Science of Computer Programming 22, 3 (June 1994), 197–230. doi:10.1016/0167- 6423(94)00004-2 IBM

doi:10.1016/0167- 1994

[4] [1995]

C++ Report 7, 4 (May 1995), 36–43

Using C++ template metaprograms. C++ Report 7, 4 (May 1995), 36–43. Reprinted in C++ Gems, ed. Stanley Lippman. Hiroto Yaguchi and Yukiyoshi Kameyama

work page 1995

[5] [1997]

In PEPM ’97: Proceedings of the 1997 ACM SIGPLAN sym- posium on Partial evaluation and semantics-based program manipulation (Amsterdam, The Netherlands)

Multi-stage programming with explicit annotations. In PEPM ’97: Proceedings of the 1997 ACM SIGPLAN sym- posium on Partial evaluation and semantics-based program manipulation (Amsterdam, The Netherlands). ACM Press, New York, NY, USA, 203–

work page 1997

[6] [2000]

Theoretical computer science 248, 1-2 (2000), 211–242

MetaML and multi-stage programming with explicit annotations. Theoretical computer science 248, 1-2 (2000), 211–242. David Vandevoorde and Nicolai M. Josuttis

work page 2000

[7] [2010]

Technical Report PLT-TR- 2010-1

Reference: Racket. Technical Report PLT-TR- 2010-1. PLT Design Inc. https://racket-lang.org/tr1/. Ronald Garcia and Andrew Lumsdaine

work page 2010

[8] [2013]

ACM SIGPLAN Notices 48, 9 (2013), 403–416

A practical theory of language-integrated query. ACM SIGPLAN Notices 48, 9 (2013), 403–416. Paul Crickard

work page 2013