Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.25741

Compiling Environment Classifiers to Contextual Modal Types

Tianyu Chen·Darshal Shetty·Jeremy G. Siek·Chao-Hong Chen·Weixi Ma·Arnaud Venet·Rocky Liu
View original source ↗Read source document ↗Export metadata ↓

Abstract

Type systems for metaprogramming take one of two approaches to safeguarding the scopes of variables in generated code. They either use Environment Classifiers (EC) to identify scopes by name (Taha and Nielsen, 2003), or they use Contextual Modal Type Theory (CMTT) to match scopes by structure (Nanevski, Pfenning, and Pientka, 2008). In this paper, we connect these two approaches by compiling a calculus with polymorphic environment classifiers, subtyping, and mutable references to a CMTT-based calculus with polymorphic contexts, mutable references, and first-class substitutions. The key idea is to map each environment classifier to a context. We prove that the compilation preserves types and that compilation preserves the behavior of metaprograms. Both proofs are mechanized in Agda. The compilation shows that CMTT is at least as expressive as environment classifiers. We conjecture that the converse compilation is difficult, because environment classifiers impose a stricter regime on the metaprogram.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, Rocky Liu. 2026-10-19. Compiling Environment Classifiers to Contextual Modal Types. https://arxiv.org/abs/2610.25741

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Instrumentation Optimization for Practical Dynamic Race Detection

Dynamic data race detectors are successful at flagging concurrency bugs, but their high runtime overhead limits adoption. This overhead stems primarily from pervasive instrumentation of memory accesses -- a significant fraction of which is for safe accesses. We address this inefficiency through a compiler-integrated approach that identifies safe accesses using static analysis and eliminates instrumentation for these. We strike a careful balance between analysis precision and cost, to ensure applicability to real-world applications. We show that our optimizations never cause ThreadSanitizer to miss races it would otherwise detect. We further observe that many checks are redundant: They only flag a race if a preceding check has already flagged an equivalent race for the same memory location. We show that, when reporting one representative per class is sufficient, even more instrumentation can be eliminated. Lastly, we introduce a dynamic technique that skips instrumentation when there is only one thread at runtime, even when this could not be determined statically. We integrate these static analyses and program transformations into the ThreadSanitizer race detector based on LLVM. Our experiments on a diverse suite of real-world applications, including Memcached, Redis, SQLite, MySQL, and Chromium, demonstrate that our optimizations reduce the number of instrumentation calls at runtime by up to 91% and yield application-level speedups of up to 1.91x, a geometric-mean Chromium speedup of 1.25x on Blink and 1.14x on Speedometer 3.0, and peak speedups reaching 2.28x on Memcached with two server threads. Our optimizations are in the process of being upstreamed into ThreadSanitizer.

cs.PL↗
arXiv2026

A Taxonomy of Predicate Transformer Monads for Specifying Monadic Programs

Monads of weakest precondition predicate transformers are the foundation of several verification frameworks for monadic programs. For specifying monadic computations with nondeterminism and nontermination, in addition to weakest preconditions, we introduce the first strongest postcondition monads covering all combinations of angelic or demonic nondeterminism and partial or total interpretations of nontermination. For extending these base strongest postcondition monads with side effects such as mutable state, monad transformers do not yield the expected monads, so we instead generalize the base monads to arrows and use arrow transformers. We give a taxonomy of weakest precondition and strongest postcondition monads, for the base monads and for their versions with state, and show that the known relationships between under- and over-approximate triples based on predicate transformers already hold at the level of the predicate transformers themselves. We use the predicate transformer monads to define under- and over-approximate triples and, where possible, Dijkstra monads. Finally, we relate these two specification styles.

cs.PL↗
arXiv2026

Blame-aware Recomposition for Secure Compilation Proofs of Low-Level Compartment Isolation

The security guarantees of existing formally verified compilers for compartmentalized programs in unsafe languages like C stop at a rather high level, assuming a built-in protection mechanism and a block-based memory model. Verifying a concrete, low-level enforcement mechanism for compartment isolation is still a major challenge for current proof techniques. In particular, Abate et al.'s proof technique fails because one of their proof steps, recomposition, essentially requires hiding all information about the code of each compartment, which is not practically achievable at a low level. We propose an extension of their proof technique to a low-level setting where compartments can fully observe each other's code. To do so, we introduce an overlay semantics that allows us to characterize these observations as a form of undefined behaviour, and we use a novel variant of recomposition that we call blame-aware recomposition, which essentially allows recomposing executions as needed in the original high-level proof technique, even if the low-level context observes the code, because this context is ultimately going to be discarded. We apply this new proof to a compartment isolation mechanism that uses a programmable tag-based reference monitor.

cs.PL↗