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

ALT Mechanisation of a mathematical definition (also referred to as formalisation) has many benefits. Here, we focus on mechanising denotational semantic definitions of programming languages by embedding them in the Agda language. The Agda type-checker detects and reports any issues with the wellformedness and type correctness of the embedded definitions. To minimise the effort required, and to facilitate correlation of the original definition with its Agda embedding, mechanisation should not involve significant reformulation or extension. Here, we show how to embed conventional Scott-Strachey denotational definitions in Agda with almost no changes to λ-notation or domain equations. Agda notation for definitions of types and functions corresponds closely to the conventional meta-notation of denotational semantics. We have developed a collection of Agda modules with postulated types for commonly used domain constructors and their associated operations. We illustrate our approach with mechan

ALT In this paper, we show how a recently introduced λ-calculus for randomized computation, called λBLL, can accurately capture the notions of first- and second-order polytime computations used in cryptographic definitions and proofs. These results, spelled out in the style of so-called implicit computational complexity, imply that λBLL is sufficiently powerful to express experiments and adversaries as used in cryptography, and that reductions, when formulated within the calculus, are guaranteed to be complexity-preserving. Remarkably, while polynomial-time soundness holds for the full calculus, polynomial-time completeness already follows in presence of a minimal finite set of basic functions.

ALT Liquid Haskell is an extension of the Glasgow Haskell compiler (GHC) that adds support for refinement types: types restricted by logical predicates. Specifications are automatically checked by an SMT solver, thus offering lightweight verification directly within the language. However, the necessarily large trusted codebase behind Liquid Haskell (from GHC to the SMT solver to the refinement typechecker itself) raises the question of trust in the verification and the necessity for a formalized semantics of Liquid Haskell linked to its implementation. Grounding Liquid Haskell in theory is complicated by the interaction between two semantic levels in the language: a computational one and a logical one (for refinement predicates). While both are well understood separately, their interaction is subtle and has only been partially described. We give a semantics to Liquid Haskell by translation to Rocq. Both the computational and logical parts are translated to the same language, with a well-un

ALT The layout algebra behind NVIDIA's CuTe library describes how tensor tiles map onto threads and memory. A layout is a shape with a stride for each entry, so a coordinate's address is the sum of its indices times their strides. As formalized by Shah and by Cecka, its central operations (e.g., composition, complement, division, product) are guarded by at least six interacting admissibility conditions. We show that this complexity is an artifact of a representational choice, not of the domain. We present a layout algebra in which every layout names the space its inputs and outputs live in: logical, physical, or thread-value indices. A layout into logical or thread-value space must be a bijection from its N coordinates onto [0,N). A layout into physical space must be alias-free: distinct coordinates land on distinct addresses, except under broadcast, where many threads read one value on purpose and the layout must mark where. Nothing maps out of a physical index. Composing f with g require