ALT L4 is a generic, reversible, linearly-typed, low-level language intended as an intermediate language for compiling reversible programming languages to reversible machines. L4 is intended to replace and generalise RSSA, a reversible SSA form. Inspiration is drawn from other low-level reversible languages such as HSSA. In this paper, we define L4 first informally, and then give a formal type system and a bidirectional small-step semantics for L4: The rules have direction indicators to determine forwards or backwards execution, and the direction can be changed during execution.

ALT Multiparty session types (MPST) is a type discipline for ensuring distributed programs are implemented correctly by construction. MPST starts by specifying a choreographic protocol as a global type and projects it onto each participant, generating local types with a guarantee of type soundness and deadlock-freedom. A central issue of MPST is that its type soundness is fragile, as it must be proven each time with respect to a chosen projection algorithm under specific semantics with a specific program correctness goal. To overcome this problem, we propose general criteria for a good projection – a set of requirements for projection algorithms by which type soundness, deadlock-freedom and liveness of distributed programs are automatically derived. Using the criteria, we prove that 8 distinct projections in the literature are good under both synchronous and asynchronous semantics, and that 4 are incorrect, failing type soundness. We extend the good projection criteria to mixed choice glob

ALT In industrial cells, commands from learned policies, operators and schedulers reach the controller after inference, confirmation and transport, and the plant may have changed meanwhile, for instance by an operator pause. Such a command is released, or takes effect, when it is no longer correct. We call this the execution gap and ask which component should make the last check, and against which version of which state. The Action Intent Schema (AIS) is a contract in which a producer states how long its decision stays valid and what it assumes. The runtime XAIR rechecks each intent before release, can commit its authorization atomically in the context store, and can release it as a version-conditional command, which the controller executes only if its version of the state is unchanged. In controlled ablations with declared ground truth on emulated and physical cells, OpenPLC and ARM and RISC-V boards, a check on a replica always left an unprotected interval: a pause written from a few to

ALT This paper introduces a novel calculus that models first-class environments and function application paradigms using standard record types. By proposing new extensions to general record types, we achieve a design that is remarkably simple and principled. We formalise this design in a core calculus and prove several desirable properties, including type soundness, normalization, and a simulation of the simply typed lambda calculus. Additionally, we extend the design with mutable references. The calculus, its semantics, along with the extension, and all stated properties are fully mechanized in the Lean 4 proof assistant, alongside an interpreter formally verified to be equivalent to the operational semantics.

ALT Hardware components communicate through clock-cycle-sensitive protocols. Hardware Description Languages (HDLs), however, provide limited support for expressing these protocols or for checking that independently developed components agree on them. When components disagree, the composed design can perform unsynchronized exchanges or stop making progress. We call these failures communication-safety violations. Communication safety is therefore a global property, determined by interactions between multiple components. This makes it difficult to check modularly. This paper presents Pact, a typed extension of Anvil for modular verification of communication safety in synchronous hardware. Pact types describe message-passing, control-flow, and clock-cycle behaviour. Each component is checked against its type. Compatible types then guarantee that the components compose into a communication-safe system. Pact also supports incremental design. It can check a subsystem before the full system contex

ALT Static type systems for Scheme have traditionally followed one of two paths: manifest type checking with multi-dispatch (Clifton and Leavens, 2005) or latent occurrence typing tailored for untyped interoperation (Tobin-Hochstadt and Felleisen, 2008). In this paper, we propose Polarized Scheme, a static foundation built upon polarized type theory and the duality of computation. In Polarized Scheme, values are positive data producers (A+) and continuations are negative observation consumers ( A+). Functions operate symmetrically under dual viewpoints: as forward value-transformers and as backward continuation-transformers. Computation exists exclusively at the interaction cut <P|K> executed on a focus-and-context abstract machine separating positive data focus from negative return contexts (R). Delimited control (shift/reset) and continuation marks are expressed directly as Return Stack frame operations parameterized by the prompt's ambient answer type without polluting producer data typ

ALT 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 o

ALT 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

ALT Evaluating autoformalized mathematical statements requires determining whether a candidate preserves the mathematical claim intended by a trusted reference. Existing methods approach this problem from complementary directions: reference-free learned evaluators estimate semantic agreement but are not constrained to a formal equivalence relation, while reference-based proof methods typically employ whole-statement logical equivalence to provide formal certificates, which is too coarse for translation fidelity and may identify mathematically unrelated statements. We introduce Structure-Aware Equivalence (SAE), a role-preserving formal equivalence relation between syntactic and whole-statement logical equivalence that allows formally justified reformulations while preserving translation-relevant mathematical structure. We operationalize SAE in the Autoformalization Correctness Evaluator (ACE), which provides certified equivalence or inequivalence judgments and reports Inconclusive otherwis

ALT Modern statistical model development begins with a high-level specification in an automatic differentiation framework such as PyTorch, JAX, or TensorFlow, which is then lowered to a target backend by a compiler or implemented manually by a research engineer. In this paper, we study whether frontier language models can correctly perform the latter task by generating GPU kernels from high-level benchmark specifications. We introduce a framework in which a language-model agent uses Velvet, a program verifier for imperative programs embedded in Lean, to prove semantic equivalence between a high-level specification and a generated CUDA kernel under an explicit set of assumptions. It also asks the LLM to prove thread safety and data race freedom of the generated kernel in VerCors, a deductive verifier for parallel code. Our main contribution to the formal verification of LLM- generated GPU kernels is showing that a combination of Lean automation and language-model-guided proof construction c

ALT 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 monad

ALT We study modalities in the linear lambda calculus, by interpreting them as endofunctors in monoidal closed categories. We support functors that do not distribute over products, including (co)monads. We also support arbitrary natural transformations as conversion between modalities. We provide a generic categorical semantics, which we then specialise to a sound and complete resource semantics. We use this resource semantics to derive normalisation by evaluation. Along the way, we describe several applications of such models. This work aims at providing a foundation for future programming languages with modalities. The paper is backed by a mechanisation in Agda.

ALT In previous works on normalization by evaluation (NbE) with an untyped domain model, explicit substitutions are a major decision choice, which, in retrospect, is taken to simplify subsequent semantic proofs. This choice hence is taken for a purely technical reason. In addition, there is no obvious lemma to test the completeness of the definition or the laws for explicit substitutions. In this technical report, we investigate NbE in a typical setting, i.e. defining substitutions as operations. We show that this setting brings simplifications in proving syntactic properties and soundness of NbE, though complications are introduced in the completeness proof of NbE.

ALT System F<:⊤ has decidable subtyping but lacks minimum types. We prove that typechecking is decidable for arbitrary explicitly annotated terms with unrestricted subsumption. The difficulty is that type abstraction uses a variable's declared bound to type its body, while quantified subtyping forgets that bound. We construct finite covers that preserve all required subtype comparisons across this change of context. These covers yield a compositional finite typing basis and a decision procedure. We then derive a backward checker that propagates acceptable targets without constructing the complete typing basis. Rectangularity of typing families gives a uniform elimination domain while retaining every result type, even when the canonical type is not least. Finite inverse families transport targets through type substitution. The same inverse specification recovers bound forgetting and yields finite type-avoidance families. Both typechecking procedures are total Rocq functions proved equivalen

ALT Much of Ethereum's most consequential code is immutable bytecode: old output of unverified compilers, and protocol logic run as contract code. We show that such bytecode can be verified as it is, without trusting what produced it, without simplifying the machine it runs on, and with no axioms beyond Lean's own. Blanc, a Lean 4 verification stack, reads fixed runtime bytes via kernel-checked certificates and states every theorem against Jaune, an executable semantics of the EVM and block processing that passes all 34,205 blockchain-test cases of Ethereum's fixture release v20.0.2 that involve only forks that have governed mainnet since May 2025. Eight artifacts, deployed from 2017 to 2026, come from seven compiler versions and an assembler. For the EIP-7002 contract, we prove that the end-of-block call to it, whose failure would invalidate the block, succeeds whatever its storage holds, and that each block's withdrawal requests are exactly the oldest pending submissions; mainnet met the

ALT We introduce FormCraft, a framework for representing acquired operations as first-class capabilities that can be recursively composed, directly invoked, and selectively retained in a persistent library through domain-specific verification. The framework separates capability well-formedness and public callability from later admission to persistent storage while preserving formation provenance and operational identity. We formalize recursive compositional closure over a uniform capability space and show that formed composites can be reused through the same public interface without re-forming their historical derivation. Experiments across continuous, discrete, propositional, and sequence domains demonstrate instance-independent reuse, independent checking, persistent acquisition, and reduced reuse-time search work under first-class exposure.

ALT Quantum computing introduces specialized software stacks and programming interfaces that are often tightly coupled to specific ecosystems and hardware backends, limiting interoperability and software reuse. For HPCQC application developers, this complicates the integration of quantum accelerators into existing applications. Existing quantum frameworks also use ecosystem-specific circuit representations and compilation pipelines, hindering integration with established heterogeneous compiler infrastructures. We propose OpenMQPI, an MLIR-based OpenMP extension for quantum programming that leverages OpenMP's standardized target offloading infrastructure to integrate quantum resources into HPC applications. OpenMQPI introduces QPIR, a lightweight MLIR dialect for representing quantum circuits within OpenMP target regions, and a compiler pipeline that performs quantum-specific optimizations and lowers circuits to executables compatible with OpenMP offloading. At runtime, an MQSS plugin enabl

ALT We study the compositional, intensional information geometry of probabilistic programs. For a first-order probabilistic programming language with finite random variables, we construct a contravariant lax monoidal functor that, for a program of type X → Y, pulls back a (degenerate) Riemannian metric on Y to X. It specialises to the Fisher metric in the case of standard statistical models and to ordinary pullback in the case of deterministic programs. We further justify this construction in two ways. First, we show that this functor arises as a pullback of geometry from a universal space of programs over a type Y with a fixed trace space. Second, we show that it is a special case of a more general pullback construction over weighted measures. Our compositional geometry depends on the presentation of the program, and we study how it relates to the (non-compositional) geometry of the realised measures by establishing a three-level inequality relating our score-velocity metric for the progr

ALT Formal verification of distributed protocols is still dominated by inductive-invariant proofs, whose central challenge is discovering strengthening assertions that rule out unreachable states. This burden is often misaligned with how protocol designers reason: they explain correctness by following representative executions, causal histories, and phase-structured interactions among nodes. This paper introduces scenario proofs, a verification methodology that makes such execution-oriented reasoning formal. A scenario is a structured expression describing representative protocol executions, enriched with ghost variables. Rather than enumerate all possible interleavings, a scenario describes canonical executions and uses a sound semi-commutation relation to account for reorderings that preserve feasibility and final states. Verification then factors into two main obligations. Coverage shows that every feasible protocol execution is equivalent, up to semi-commutation, to one described by th

ALT In a type theory with a cumulative universe hierarchy, subtyping is often incorporated to lift lower universe levels to higher ones. In practice, kernels of proof assistants typically implement universe subtyping conservatively: subtyping only propagates covariantly into the output types of Π types, while input types must be equivalent. A full-blown subtyping relation also compares the input types contravariantly. However, contravariant subtyping is not justified by the existing set-theoretic model, and poses challenges in the development of a complete subtyping algorithm. We present mclttsub, a complete mechanized study of contravariant universe subtyping for a core Martin-Löf type theory (MLTT), built as an extension of the verified McTT kernel in Rocq. We re-establish the syntactic meta-theory and the soundness and completeness properties of the normalization-by-evaluation (NbE) algorithm. To complete the verified pipeline for a type-checker, we give two complete and sound subtyping