A Dependently Typed Multi-Stage Calculus

Akira Kawata; Atsushi Igarashi

REVIEW 2 major objections 4 minor 46 references

A Dependently Typed Multi-Stage Calculus

T0 review · 2 major / 4 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 The paper develops λMD, a dependently typed multi-stage calculus, and proves type soundness, strong normalization, confluence, and progress.

desk verdict Real first formal combination of dependent types with MetaOCaml-style staging, but the paper's own motivating example contradicts its formal K-Csp rule. read the letter →

arxiv 1908.02035 v3 pith:YHJ4GBCX submitted 2019-08-06 cs.PL

Akira Kawata , Atsushi Igarashi This is my paper · ORCID

classification cs.PL

keywords multi-stageprogrammingdependenttypescross-stagepersistencequasi-quotationtypepreservationstrongnormalizationconfluencestagedreduction

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

Multi-stage programming lets programs build and run code at run time; dependent types let types mention values, such as the length of a vector. The paper asks whether the two can be combined without losing safety and shows that the answer is yes by defining λMD, an extension of the multi-stage calculus λ⊲% with dependent function types, code types indexed by stages, and cross-stage persistence at both term and type level. The paper proves preservation, strong normalization, and confluence for full reduction, and progress for staged call-by-value evaluation. If these results are correct, λMD is the first formal calculus to offer full-spectrum dependently typed multi-stage programming with quotation, escape, run, and cross-stage persistence all in one system, making it a foundation for code generators that emit code whose types certify invariants such as fixed vector sizes.

What carries the argument

The load-bearing mechanism is the stage annotation A decorating every typing judgment, together with the code type ⊲ατ that types quotations. Three rules carry the design: T-Csp embeds a term from stage A into stage Aα; K-Csp silently lifts a well-formed type to a deeper stage, which is how a type such as Vector (%αn) becomes usable inside code; and Q-% equates %αM with M whenever M is already well typed at the deeper stage, so that Vector 5 and Vector (%γ5) count as the same type. Strong normalization is obtained by the ♮-erasure, a translation that erases stages and dependencies down to the simply typed lambda calculus while preserving typing and reduction. The eight mutually recursive judgment forms are what let this argument go through, and they are also the component that must be scrutinized most closely.

What would settle it

Check the derivability of the judgment x:Int@ε ⊢Σ Vector x :: ∗@α: if a formalization of the rules derives it via K-Csp while Section 2.2 claims it is not well-formed, then either the rules or the motivating example must change, and until that is settled the metatheorems cannot be taken as applying to the intended system. A proof assistant can settle this directly by attempting to construct or refute that derivation.

Watch

Extended reading notes

Core claim

The central claim is that dependently typed multi-stage programming can be made sound by letting every type-theoretic judgment carry a stage annotation. The paper's calculus λMD extends λ⊲% with dependent function types Πx:τ.σ, kinds Πx:τ.K, and code types ⊲ατ, and it handles 'run' as instantiation of a stage abstraction with the empty stage. The key design choice is implicit cross-stage persistence at the type level: a type well-formed at stage A is accepted at stage Aα, so types like Vector (%αn) are usable inside quotations even when the index n is a value from outside. The paper proves that the calculus is well behaved — preservation, strong normalization, confluence for full reduction, and progress for staged reduction — and demonstrates the intended use with a vector-addition code generator whose generated function type mentions the vector length. The paper also claims this is the first formal treatment of full-spectrum dependent types together with quotation, escape, run, and cross-stage persistence.

Load-bearing premise

The results depend on the eight mutually recursive judgment forms being consistent, and that assumption is not entirely safe: the paper's Section 2.2 says Vector x should not be well-formed at stage α under x:Int@ε, yet its K-Csp rule derives exactly that judgment.

Editorial extensions

If this is right

Every well-typed λMD term terminates under full reduction, so no infinite reduction sequence can arise from typed code generators.
Full reduction is confluent, which means the result of running a generator does not depend on the order in which redexes are reduced.
The staged, call-by-value semantics is deterministic and every closed well-typed term is either a value or can take exactly one step, so generated code cannot get stuck at run time.
A code generator can return a function whose type mentions a runtime value, and the Q-% equivalence lets that generated code be spliced together with other fragments without a type mismatch.

Reading between the lines

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

The success of implicit type-level CSP suggests that a practical implementation could erase %α from types during type checking, treating Q-% as a definitional equality rather than an operational step.
The same stage-aware kinding discipline should extend to indexed type families and type operators; the paper already notes that type constructors taking arguments from different stages make term-level CSP necessary, so a matrix type indexed by rows and columns would be a natural test case.
A mechanized proof of the metatheorems would likely need to resolve the example in Section 2.2 where the informal discussion and the K-Csp rule appear to disagree, and such a verification could expose whether the rule set needs a side condition.
Because the paper leaves typechecking algorithms to future work, the next practical step is to design an algorithm that handles implicit type-level CSP and %-erasing equivalence, which the authors identify as the hard parts.

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

Let me skip the throat-clearing. This is a genuine step forward: λMD appears to be the first formal calculus that puts full-spectrum dependent types together with quasi-quotation, escape, run-as-stage-application, and cross-stage persistence, and the paper proves the standard package (preservation, confluence, SN, progress) with an erasure-based SN argument that is likely sound. The definitions are careful, and the choice of λLF as the dependent base is sensible. The novelty claim over the cited prior work (λH◦, Concoqtion, Brady-Hammond) looks supported.

The soft spot is real and not minor. Section 2.2 says that with x : Int@ε, the type Vector x is well-formed at ε but not at α, and uses that to motivate term-level CSP. But the formal K-Csp rule in Section 3.3 derives exactly the judgment x : Int@ε ⊢ Vector x :: ∗@α, with no side condition on free term variables. The stress-test note is correct. This is a contradiction between the informal overview and the formal system, and it weakens the paper's central motivating example. The calculus may still be coherent; the fix is either to constrain K-Csp (so implicit type-level CSP only applies to closed types or types whose index terms are stage-flexible) or to rewrite Section 2.2 to say that implicit CSP already lifts open types, and term-level CSP is needed when a type constructor takes arguments from different stages (which the authors themselves note in the remark after the example). As written, the two parts of the paper disagree, and a reader cannot tell which is intended.

There are smaller issues. Lemma 3 has a typo in the Λ-inversion case (σ = ∀α.σ should presumably be τ = ∀α.σ). The appendix proofs are sketches; representative cases are given but many are dispatched as “straightforward induction.” For this kind of paper that is contestable but not fatal, since the cases really do look routine. The Q-% rule is interesting and well rationalized.

Overall: the formal contribution is solid enough to warrant serious refereeing. The contradiction is in the exposition and the motivation, not obviously in the metatheory, but it needs to be resolved before the paper can be accepted. I would send it to a good PL venue and let the referees push on the K-Csp rule.

Referee Report

2 major / 4 minor

Summary. The paper introduces λMD, a calculus that extends Hanada and Igarashi's λ⊲% with LF-style dependent types. The calculus supports quasi-quotation ◮α, escape ◭α, stage abstraction Λα with application to stage sequences, run represented as application to ε, and cross-stage persistence %α; types are classified by kinds and equipped with congruences and special equivalences, with stages attached to typing, kinding, and equivalence judgments. The authors define full reduction and a staged small-step call-by-value semantics, state term and stage substitution lemmas and inversion lemmas, and claim preservation, strong normalization, and confluence for full reduction as well as unique decomposition and progress for staged reduction. The appendix gives the complete rule set and proof sketches, and a vector-addition example is used to motivate term-level CSP in type indices.

Significance. If the metatheorems hold, λMD is a useful first step toward a formal account of full-spectrum dependent types in MetaOCaml-style staging, and the paper identifies a genuine design question: how stages should interact with type well-formedness. The paper is explicit that typechecking, residualization, and detailed proofs are left to future work. Its strength is the concrete formal system and the erasure-based normalization strategy; the proofs are not machine-checked. However, the formal rule K-Csp contradicts the motivating discussion, and the strong-normalization proof contains a false claim about the size behavior of Λ-reduction. These issues do not, on my reading, invalidate the whole formal system, but they do mean that the central presentation and one load-bearing proof argument need substantial repair before the paper is publishable.

major comments (2)

[Section 2.2 / Section 3.3 (K-Csp)] The informal overview and the formal kinding rules are contradictory. Section 2.2 states that under x:Int@ε the type Vector x is well-formed at ε but not at α, and uses this to argue that λx:Int.◮α(λy:Vector x.M) is rejected without term-level CSP, so that Vector (%αx) is needed. However, K-Csp in Section 3.3 (and Appendix A.3) has no side condition and derives Γ ⊢Σ τ :: ∗@Aα from Γ ⊢Σ τ :: ∗@A. With Vector :: Πx:Int.∗ in the signature, K-TConst and K-App give x:Int@ε ⊢Σ Vector x :: ∗@ε, and one application of K-Csp with A = ε gives x:Int@ε ⊢Σ Vector x :: ∗@α. The type Vector x is therefore already legal at stage α, and the generator λx:Int.◮α(λy:Vector x.M) is typeable without %αx. The paper must either constrain or remove K-Csp (while preserving the matrix-type example in Section 3.3) or rewrite Section 2.2 so that implicit type-level CSP is presented as the lifting mechanism, with term-level CSP motivated only by index terms that genuinely live at different stages. As written, the paper's central motivation for term-level CSP in dependent types is not established.
[Appendix, proof of Theorem 10] The strong-normalization argument contains a false premise. The proof states: 'If there is an infinite reduction sequence in λMD then there are infinite beta reductions in the sequence. This is because reductions other than β-reduction reduce the size of a term.' Λ-reduction does not always reduce size: for example, (Λα.◮α◮αx) βγ reduces to ◮β◮γ◮β◮γx, which is syntactically larger. Thus the claim that any infinite sequence must contain infinitely many β-reductions is unsupported. The erasure proof needs a separate, correct argument that ◆- and Λ-reductions terminate (for instance, a well-founded measure on stage redexes), or an alternative normalization proof.

minor comments (4)

[Section 4, Lemma 3] Item 3 of Lemma 3 contains a typo: 'there is σ such that σ = ∀α.σ' should read 'there is σ such that τ = ∀α.σ'.
[Appendix B, Definition 1 (♮ translation)] The type case of the erasure is written ♮(τ x) = ♮(τ), but the syntax of types has arbitrary term applications τ M; the case should quantify over all M. Also, the context case ♮(Γ, X : K@A) refers to a form that is not in the grammar of Γ and should be removed or corrected.
[Appendix B, Lemma 15] Lemma 15 is stated as 'If Γ ⊢Σ M : τ @A and M −→β N in λMD then ♮(M) = ♮(N)', but the lemma is about Λ-reduction; the subscript should be Λ.
[Appendix, Theorem 11] The weak Church–Rosser justification is incomplete: for two redexes where one is inside the body of another, reducing the outer redex can duplicate the inner redex, so the sentence 'we can reduce one of them after we reduce another' is not by itself a proof. Please spell out the standard argument or cite a lemma covering this case.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: λMD's properties are proved from its own definitions, with SN reducing to the external strong normalization theorem for simply typed λ-calculus.

full rationale

The paper's central claims are metatheorems about a newly defined calculus, and the proof chain is self-contained. Section 3 defines syntax, reduction, and eight mutually recursive judgment forms; Section 4 (with proofs in the appendix) derives Term/Stage Substitution, Inversion, Preservation, SN, Confluence, and Progress from those definitions. The SN proof uses the standard external fact that the simply typed λ-calculus is strongly normalizing, via the ♮ translation; Λ- and ◆-reduction become equality under ♮, so no λMD property is imported. The Q-%, QT-Csp and QK-Csp rules are explicit equivalence axioms of the proposed design, not fitted parameters renamed as predictions, and no data are fitted anywhere. The base calculus λ⊲% is prior work that is restated in the paper, and no load-bearing argument reduces to a self-citation or to an imported uniqueness theorem. A separate correctness issue, flagged for completeness: Section 2.2 claims x:Int@ε ⊢ Vector x :: ∗@α is underivable, but rule K-Csp (Section 3.3) derives exactly that judgment from x:Int@ε ⊢ Vector x :: ∗@ε; this is an internal inconsistency in the motivational discussion, not a circularity in the formal development.

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

The calculus's soundness results are built on standard metatheorems (SN of simply typed lambda calculus, Newman's Lemma) and on standard assumptions about substitution and well-founded mutual inductive definitions. No empirical data or fitted parameters are involved. The rules K-Csp and Q-% are part of the object of study rather than hidden assumptions, but their design choices are worth auditing.

assumptions (4)

standard math Strong normalization of simply typed lambda calculus
Used in Theorem 2: the ♮ erasure translation maps λMD terms into simply typed lambda calculus, and an infinite λMD reduction sequence would produce an infinite β-reduction sequence in λ→.
standard math Newman's Lemma
Used in Theorem 3 to derive confluence from strong normalization plus weak Church-Rosser.
standard math Capture-avoiding substitution for terms and stages satisfies the standard substitution lemmas
Assumed in the proofs of preservation and the substitution lemmas; not proven explicitly in the paper.
domain assumption The mutual inductive definitions of the eight judgment forms are well-founded
The type system is defined by simultaneous induction over derivations; the paper does not discuss stratification, which is standard but unstated for LF-like systems.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A Dependently Typed Multi-Stage Calculus." pith.science (2026). https://pith.science/paper/YHJ4GBCX

@misc{pith2026190802035,
  author       = {Pith},
  title        = {Pith review of: A Dependently Typed Multi-Stage Calculus},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YHJ4GBCX}},
  note         = {Machine review of arXiv:1908.02035}
}

abstract

We study a dependently typed extension of a multi-stage programming language \`a la MetaOCaml, which supports quasi-quotation and cross-stage persistence for manipulation of code fragments as first-class values and an evaluation construct for execution of programs dynamically generated by this code manipulation. Dependent types are expected to bring to multi-stage programming enforcement of strong invariant -- beyond simple type safety -- on the behavior of dynamically generated code. An extension is, however, not trivial because such a type system would have to take stages of types -- roughly speaking, the number of surrounding quotations -- into account. To rigorously study properties of such an extension, we develop $\lambda^{MD}$, which is an extension of Hanada and Igarashi's typed calculus $\lambda^{\triangleright\%} $ with dependent types, and prove its properties including preservation, confluence, strong normalization for full reduction, and progress for staged reduction. Motivated by code generators that generate code whose type depends on a value from outside of the quotations, we argue the significance of cross-stage persistence in dependently typed multi-stage programming and certain type equivalences that are not directly derived from reduction rules.

Figures

Figures reproduced from arXiv: 1908.02035 by the authors.

**Figure 1.** Eight judgment forms of the type system of λ MD. To add declarations to a signature, the kind/type of a (type-level) constant has to be well-formed at stage ε so that it is used at any stage. In what follows, well-formedness is not explicitly mentioned but we assume that all signatures and type environments are well-formed. Kind Well-formedness and Kinding. The rules for kind well-formedness and kinding are a straig… view at source ↗

**Figure 2.** Typing Rules. capturing variables elsewhere. The rule T-Ins is for applications of stages to stage abstractions. The rule T-Csp is for CSP, which means that, if term M is of type τ at stage A, then %αM is of type τ at stage Aα. Note that CSP is also applied to the type τ (although it is implicit) in the conclusion. Thanks to implicit CSP, the typing rule is the same as in λ ⊲%. Kind, Type and Term Equivalence. Since… view at source ↗

**Figure 3.** Term Equivalence Rules. well-typed at the next stage Aα. For example, constants do not depend on the stage (see T-Const) and so Γ ⊢Σ %αc ≡ c : τ@Aα holds but variables do depend on stages and so this rule does not apply. Example. We show an example of a dependently typed code generator in a hypothetical language based on λ ⊲%. This language provides definitions by let, recursive functions (represented by fix), if-… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

46 extracted references · 46 canonical work pages

[1]

In: Pierce, B .C

Aspinall, D., Hofmann, M.: Dependent types. In: Pierce, B .C. (ed.) Advanced topics in types and programming languages, chap. 2. MIT pres s (2005)

work page 2005
[2]

Cambr idge University Press (1998)

Baader, F., Nipkow, T.: Term rewriting and all that. Cambr idge University Press (1998)

work page 1998
[3]

In: Federated logic conference (FLoC) s atellite workshop on intuitionistic modal logics and applications (IMLA) (1999 )

Benaissa, Z.E.A., Moggi, E., Taha, W., Sheard, T.: Logica l modalities and multi- stage programming. In: Federated logic conference (FLoC) s atellite workshop on intuitionistic modal logics and applications (IMLA) (1999 )

work page 1999
[4]

Logical Methods in Computer Science Volume 11, Issue 1 (Mar 2015)

Berger, M., Tratt, L.: Program Logics for Homogeneous Gen erative Run-Time Meta-Programming. Logical Methods in Computer Science Volume 11, Issue 1 (Mar 2015)

work page 2015
[5]

In: Trends in Functional Programming (2006)

Brady, E., Hammond, K.: Dependently typed meta-programm ing. In: Trends in Functional Programming (2006)

work page 2006
[6]

In: International Confe rence on Generative Programming and Component Engineering

Calcagno, C., Taha, W., Huang, L., Leroy, X.: Implementin g multi-stage languages using ASTs, gensym, and reﬂection. In: International Confe rence on Generative Programming and Component Engineering. pp. 57–76. Springe r (2003)

work page 2003
[7]

In: Pro- ceedings of the Eighth ACM SIGPLAN International Conferenc e on Functional Programming

Chen, C., Xi, H.: Meta-programming through typeful code r epresentation. In: Pro- ceedings of the Eighth ACM SIGPLAN International Conferenc e on Functional Programming. pp. 275–286. ICFP ’03, ACM, New York, NY, USA (2 003)

work page
[8]

In: Proceedings of the 31st ACM SIGPLAN Conferenc e on Programming Language Design and Implementation

Chlipala, A.: Ur: Statically-typed metaprogramming wit h type-level record com- putation. In: Proceedings of the 31st ACM SIGPLAN Conferenc e on Programming Language Design and Implementation. pp. 122–133. PLDI ’10, ACM, New York, NY, USA (2010)

work page 2010

Show all 46 references

[9]

Coquand, T., Huet, G.: The calculus of constructions. Inf . Comput. 76(2-3), 95– 120 (Feb 1988)

1988
[10]

In: Logic in Com- puter Science, 1996

Davies, R.: A temporal-logic approach to binding-time a nalysis. In: Logic in Com- puter Science, 1996. LICS’96. Proceedings., Eleventh Annu al IEEE Symposium on. pp. 184–195. IEEE (1996)

1996
[11]

Davies, R., Pfenning, F.: A modal analysis of staged comp utation. J. ACM 48(3), 555–604 (2001)

2001
[12]

PACMPL 1(ICFP), 34:1–34:29 (2017) A Dependently Typed Multi-Stage Calculus 19

Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal veriﬁcation. PACMPL 1(ICFP), 34:1–34:29 (2017) A Dependently Typed Multi-Stage Calculus 19

2017
[13]

Fogarty, S., Pasalic, E., Siek, J., Taha, W.: Concoqtion : Indexed types now! In: Proceedings of the 2007 ACM SIGPLAN Symposium on Partial Eva luation and Semantics-based Program Manipulation. pp. 112–121. PEPM ’07, ACM, New York, NY, USA (2007)

2007
[14]

In: Codish, M., Sumii, E

Hanada, Y., Igarashi, A.: On cross-stage persistence in multi-stage programming. In: Codish, M., Sumii, E. (eds.) Functional and Logic Progra mming. pp. 103–118. Springer International Publishing, Cham (2014)

2014
[15]

Journal of the ACM (JACM) 40(1), 143–184 (1993)

Harper, R., Honsell, F., Plotkin, G.: A framework for deﬁ ning logics. Journal of the ACM (JACM) 40(1), 143–184 (1993)

1993
[16]

In: Proc

Kim, I., Yi, K., Calcagno, C.: A polymorphic modal type sy stem for lisp-like multi- staged languages. In: Proc. of ACM SIGPLAN-SIGACT Symposiu m on Principles of Programming Languages (POPL 2003). pp. 257–268 (2006)

2006
[17]

NOW Publishing (2018)

Kiselyov, O.: Reconciling Abstraction with High Perfor mance: A MetaOCaml ap- proach. NOW Publishing (2018)

2018
[18]

In: Functional and Logic Programming - 12th Inte rnational Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014

Kiselyov, O.: The design and implementation of BER metao caml - system de- scription. In: Functional and Logic Programming - 12th Inte rnational Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings. p p. 86–102 (2014)

2014
[19]

In: Proc

Leijen, D., Meijer, E.: Domain speciﬁc embedded compile rs. In: Proc. of the 2nd Conference on Domain-Speciﬁc Languages (DSL ’99). pp. 109– 122 (1999)

1999
[20]

In: Proceedings of the 17th ACM SIGPLAN International Conferen ce on Functional Programming

Mainland, G.: Explicitly heterogeneous metaprogrammi ng with metahaskell. In: Proceedings of the 17th ACM SIGPLAN International Conferen ce on Functional Programming. pp. 311–322. ICFP ’12, ACM, New York, NY, USA (2 012)
[21]

Logic Collo- quium ’73 80 (01 1973)

Martin-L¨ of, P.: An intuitionistic theory of types: Pre dicative part. Logic Collo- quium ’73 80 (01 1973)

1973
[22]

In: Pro ceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages

Meyer, A.R., Reinhold, M.B.: “Type” is not a type. In: Pro ceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. pp. 287–295. POPL ’86, ACM, New York, NY, USA (1986)

1986
[23]

Milner, R.: A theory of type polymorphism in programming . J. Comput. Syst. Sci. 17, 348–375 (1978)

1978
[24]

In: Proc

Moggi, E., Taha, W., Benaissa, Z.E.A., Sheard, T.: An ide alized MetaML: Sim- pler, and more expressive. In: Proc. of European Symposium o n Programming (ESOP’99). Lecture Notes in Computer Science, vol. 1576, pp . 193–207 (1999)

1999
[25]

Nanevski, A., Pfenning, F.: Staged computation with nam es and necessity. J. Funct. Program. 15(5), 893–939 (2005)

2005
[26]

In: Proceedings of the Seventh ACM SIGPLAN International Co nference on Func- tional Programming

Pasalic, E., Taha, W., Sheard, T.: Tagless staged interp reters for typed languages. In: Proceedings of the Seventh ACM SIGPLAN International Co nference on Func- tional Programming. pp. 218–229. ICFP ’02, ACM, New York, NY , USA (2002)

2002
[27]

MIT Pres s (2002)

Pierce, B.C.: Types and Programming Languages. MIT Pres s (2002)

2002
[28]

In: Proceedings of the 29th ACM SIGPLAN-SIGACT Sympos ium on Princi- ples of Programming Languages

Shao, Z., Saha, B., Trifonov, V., Papaspyrou, N.: A type s ystem for certiﬁed bina- ries. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Sympos ium on Princi- ples of Programming Languages. pp. 217–232. POPL ’02, ACM, N ew York, NY, USA (2002)

2002
[29]

In: Gener- ative and Transformational Techniques in Software Enginee ring II, International Summer School, GTTSE 2007, Braga, Portugal, July 2-7, 2007

Taha, W.: A gentle introduction to multi-stage programm ing, part II. In: Gener- ative and Transformational Techniques in Software Enginee ring II, International Summer School, GTTSE 2007, Braga, Portugal, July 2-7, 2007. Revised Papers. pp. 260–290 (2007)

2007
[30]

In: Pr oc

Taha, W., Nielsen, M.F.: Environment classiﬁers. In: Pr oc. of ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (P OPL’03). pp. 26–37. ACM, New York, NY, USA (2003)

2003
[31]

Taha, W., Sheard, T.: MetaML and multi-stage programmin g with explicit anno- tations. Theor. Comput. Sci. 248(1-2), 211–242 (Oct 2000) 20 A. Kawata, A. Igarashi

2000
[32]

Log- ical Methods in Computer Science 6(4) (Dec 2010)

Tsukada, T., Igarashi, A.: A Logical Foundation for Envi ronment Classiﬁers. Log- ical Methods in Computer Science 6(4) (Dec 2010)

2010
[33]

In: Proc

Xi, H., Chen, C., Chen, G.: Guarded recursive datatype co nstructors. In: Proc. of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’03). pp. 224–235 (2003)

2003
[34]

In: Proc

Xi, H., Pfenning, F.: Eliminating array bound checking t hrough dependent types. In: Proc. of the ACM SIGPLAN Conference on Programming Langu age Design and Implementation (PLDI’98). pp. 249–257 (1998) A Dependently Typed Multi-Stage Calculus 21 A Full Deﬁnition of λ MD A.1 Sy...

1998
[35]

If Γ ⊢Σ τ :: K@A, then Γ ⊢Σ K kind@A
[36]

If Γ ⊢Σ M : τ @A, then Γ ⊢Σ τ :: ∗@A
[37]

If Γ ⊢Σ K ≡ J@A, then Γ ⊢Σ K kind@A and Γ ⊢Σ J kind@A
[38]

If Γ ⊢Σ τ ≡ σ :: K@A, then Γ ⊢Σ τ :: K@A and Γ ⊢Σ σ :: K@A
[39]

If Γ ⊢Σ M ≡ N : τ @A, then Γ ⊢Σ M : τ @A and Γ ⊢Σ N : τ @A. Proof. We can prove using induction on the derivation tree. We show some ca ses as examples. Case K-Csp: Γ ⊢Σ K :: ∗@Aα is derived from Γ ⊢Σ K :: ∗@A. By W-Star, Γ ⊢Σ ∗ kind@Aα. Case T-Csp: Γ ⊢Σ %αM :: τ @Aα is derive...
[40]

If Γ ⊢Σ (λx : σ.M) : ρ, then there are σ′ and τ ′ such that ρ = Πx : σ′.τ ′, Γ ⊢Σ σ ≡ σ′@A and Γ, x : σ′@A ⊢Σ M : τ ′@A
[41]

A Dependently Typed Multi-Stage Calculus 27

If Γ ⊢Σ ρ ≡ (Πx : σ.τ) : K@A, then there are σ′, τ ′, K, and J such that ρ = Πx : σ′.τ ′, Γ ⊢Σ σ ≡ σ′ : K@A, and Γ, x : σ@A ⊢Σ τ ≡ τ ′ : J@A. A Dependently Typed Multi-Stage Calculus 27
[42]

If Γ ⊢Σ (Πx : σ.τ) ≡ ρ : K@A, then there are σ′, τ ′, K, and J such that ρ = Πx : σ′.τ ′, Γ ⊢Σ σ ≡ σ′ : K@A, and Γ, x : σ@A ⊢Σ τ ≡ τ ′ : J@A. Proof. We can prove using induction on the derivation tree. We show a few ma in cases. Case T-Abs: Γ ⊢Σ σ :: ∗@A and Γ, x : σ@A ⊢Σ M : ...
[43]

M can be uniquely decomposed into an evaluation context and a r edex, that is, there uniquely exist B, E A B , and RB such that M = EA B [RB]. Proof. We prove by induction on the type derivation tree of Γ ⊢Σ M : τ @A. 32 A. Kawata, A. Igarashi Case T-V ar: Γ ⊢Σ x : τ @A is the...
[44]

– If M ∈ V A is true • and A = ε, then M = ◮αvα from Inversion Lemma and ◭α◮αvα = Eα α [Rα]

There is an unique triple of ( B, E A B , RB) such that ( B = ε or B = β) and M = EA B [RB]. – If M ∈ V A is true • and A = ε, then M = ◮αvα from Inversion Lemma and ◭α◮αvα = Eα α [Rα]. • and A ⁄= ε, then ◭αvA ∈ V Aα. – If there is an unique triple of ( B, E A B , RB) such tha...
[45]

• If M ∈ V ε, M = Λα.vε from Inversion Lemma

there is a unique triple of ( B, E ε B, RB) such that ( B = ε or B = β) and M = Eε B[RB]. • If M ∈ V ε, M = Λα.vε from Inversion Lemma. Thus, Λα.vε C = Eε ε [Rε] • If there is an unique triple of ( B, E ε B, RB) such that ( B = ε or B = β) and M = Eε B[RB], we can decompose Eε...
[46]

• If M ∈ V A, it is clear that vA C ∈ V A

there is a unique triple of ( B, E A B , RB) such that ( B = ε or B = β) and M = EA B [RB]. • If M ∈ V A, it is clear that vA C ∈ V A. • If there are an unique triple of ( B, E A B , RB) such that ( B = ε or B = β) and M = EA B [RB], we can decompose EA B [RB] C uniquely becau...

Pith tools

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

[1] [1]

In: Pierce, B .C

Aspinall, D., Hofmann, M.: Dependent types. In: Pierce, B .C. (ed.) Advanced topics in types and programming languages, chap. 2. MIT pres s (2005)

work page 2005

[2] [2]

Cambr idge University Press (1998)

Baader, F., Nipkow, T.: Term rewriting and all that. Cambr idge University Press (1998)

work page 1998

[3] [3]

In: Federated logic conference (FLoC) s atellite workshop on intuitionistic modal logics and applications (IMLA) (1999 )

Benaissa, Z.E.A., Moggi, E., Taha, W., Sheard, T.: Logica l modalities and multi- stage programming. In: Federated logic conference (FLoC) s atellite workshop on intuitionistic modal logics and applications (IMLA) (1999 )

work page 1999

[4] [4]

Logical Methods in Computer Science Volume 11, Issue 1 (Mar 2015)

Berger, M., Tratt, L.: Program Logics for Homogeneous Gen erative Run-Time Meta-Programming. Logical Methods in Computer Science Volume 11, Issue 1 (Mar 2015)

work page 2015

[5] [5]

In: Trends in Functional Programming (2006)

Brady, E., Hammond, K.: Dependently typed meta-programm ing. In: Trends in Functional Programming (2006)

work page 2006

[6] [6]

In: International Confe rence on Generative Programming and Component Engineering

Calcagno, C., Taha, W., Huang, L., Leroy, X.: Implementin g multi-stage languages using ASTs, gensym, and reﬂection. In: International Confe rence on Generative Programming and Component Engineering. pp. 57–76. Springe r (2003)

work page 2003

[7] [7]

In: Pro- ceedings of the Eighth ACM SIGPLAN International Conferenc e on Functional Programming

Chen, C., Xi, H.: Meta-programming through typeful code r epresentation. In: Pro- ceedings of the Eighth ACM SIGPLAN International Conferenc e on Functional Programming. pp. 275–286. ICFP ’03, ACM, New York, NY, USA (2 003)

work page

[8] [8]

In: Proceedings of the 31st ACM SIGPLAN Conferenc e on Programming Language Design and Implementation

Chlipala, A.: Ur: Statically-typed metaprogramming wit h type-level record com- putation. In: Proceedings of the 31st ACM SIGPLAN Conferenc e on Programming Language Design and Implementation. pp. 122–133. PLDI ’10, ACM, New York, NY, USA (2010)

work page 2010