arXiv subjects

Yuito Murase

Publications and source records attributed to Yuito Murase.

5 recordsLinked to original sources

arXiv2026

Refined^2 Environment Classifiers

MetaML-style multi-stage programming (MSP) supports quasi-quotation-based code generation, runtime execution of generated code, and cross-stage persistence (CSP). However, its interaction with computational effects is subtle: mutable state can cause scope extrusion, where generated code escapes the scope of variables on which it depends. This paper presents a type system for MetaML-style MSP with mutable state that statically rules out harmful scope extrusion while supporting multi-level code generation, runtime execution, and a variant of CSP. Our system builds on refined environment classifiers (RECs), a discipline that annotates code types with the variable scopes on which generated code depends. To scale RECs to the MetaML-style setting, we refine classifiers so that they track not only variable scopes, but also the scopes of classifiers themselves. Further, we integrated polymorphism over classifiers, enabling more general and reusable code generation patterns in a multi-level setting. For the resulting system, we define an operational semantics via a definitional interpreter and prove type soundness and safety of offline code generation, showing that generated code can be extracted as standalone well-typed programs. We provide working implementations and mechanized proofs in Rocq.

cs.PL↗

arXiv2026

Bounded Modal Logic: Explicit Scope Dependencies in Multi-Stage Programming

It is widely known that proof systems for modal logic can be interpreted as type systems for multi-stage programming (MSP). However, existing modal-logical foundations for MSP do not fully account for staged programs with complex scoping structures. For example, a modal account of cross-stage persistence, in which free variables in generated code may refer to run-time bindings, has not yet been fully established. This paper presents *Bounded Modal Logic* (BML), a constructive modal logic with modalities bounded by names for scopes and first-order-style quantification over those names. This makes scope dependencies of code fragments explicit, thereby enabling reasoning about staged programs with nontrivial scoping behavior, including cross-stage persistence. We present a natural deduction system and a Kripke semantics for BML, and prove their soundness and completeness. We also provide a computational counterpart of BML as a typed lambda calculus for MSP. In addition to standard metatheoretic properties such as confluence and strong normalization, we develop a staged semantics for the calculus, showing that the type system supports the stage-by-stage execution model required for multi-stage programming.

cs.LO↗

arXiv2026

Contextual Metaprogramming for Session Types

We propose the integration of staged metaprogramming into a session-typed message passing functional language. We build on a model of contextual modal type theory with multi-level contexts, where contextual values, closing arbitrary terms over a series of variables, may be boxed and transmitted in messages. Once received, one such value may then be unboxed and locally applied before being run. To motivate this integration, we present examples of real-world use cases, for which our system would be suitable, such as servers preparing and shipping code on demand via session typed messages. We present a type system that distinguishes linear (used exactly once) from unrestricted (used an unbounded number of times) resources, and further define a type checker, suitable for a concrete implementation. We show type preservation, a progress result for sequential computations and absence of runtime errors for the concurrent runtime environment, as well as the correctness of the type checker.

cs.PL↗

arXiv2023

Contextual Modal Type Theory with Polymorphic Contexts

Modal types -- types that are derived from proof systems of modal logic -- have been studied as theoretical foundations of metaprogramming, where program code is manipulated as first-class values. In modal type systems, modality corresponds to a type constructor for code types and controls free variables and their types in code values. Nanevski et al. have proposed contextual modal type theory, which has modal types with fine-grained information on free variables: modal types are explicitly indexed by contexts -- the types of all free variables in code values. This paper presents $λ_{\forall[]}$, a novel extension of contextual modal type theory with parametric polymorphism over contexts. Such an extension has been studied in the literature but unlike earlier proposals, $λ_{\forall[]}$ is more general in that multiple parts of a single context can be abstracted. We formalize \lamfb with its type system and operational semantics given by $β$-reduction and prove its basic properties including subject reduction, strong normalization, and confluence. Moreover, to demonstrate the expressive power of polymorphic contexts, we show a type-preserving embedding from a two-level fragment of Davies' $λ_{\bigcirc}$, which is based on linear-time temporal logic, to $λ_{\forall[]}$.

cs.LO↗

arXiv2018

Modality via Iterated Enrichment

This paper investigates modal type theories by using a new categorical semantics called change-of-base semantics. Change-of-base semantics is novel in that it is based on (possibly infinitely) iterated enrichment and interpretation of modality as hom objects. In our semantics, the relationship between meta and object levels in multi-staged computation exactly corresponds to the relationship between enriching and enriched categories. As a result, we obtain a categorical explanation of situations where meta and object logics may be completely different. Our categorical models include conventional models of modal type theory (e.g., cartesian closed categories with a monoidal endofunctor) as special cases and hence can be seen as a natural refinement of former results. On the type theoretical side, it is shown that Fitch-style modal type theory can be directly interpreted in iterated enrichment of categories. Interestingly, this interpretation suggests the fact that Fitch-style modal type theory is the right adjoint of dual-context calculus. In addition, we present how linear temporal, S4, and linear exponential modalities are described in terms of change-of-base semantics. Finally, we show that the change-of-base semantics can be naturally extended to multi-staged effectful computation and generalized contextual modality a la Nanevski et al. We emphasize that this paper answers the question raised in the survey paper by de Paiva and Ritter in 2011, what a categorical model for Fitch-style type theory is like.

cs.LO↗