计算机科学中的逻辑

Monads are a ubiquitous structure in functional programming used for modelling computational effects. For example, the state monad models the effect of a computation interacting with a memory system. Here we introduce the quantum instrument…

Small language models can run locally on consumer hardware, but structured reasoning often pushes users toward repeated sampling or larger models. This article studies a bounded neuro-symbolic alternative for local inference: a model…

The probabilistic bisimilarity distance provides a quantitative measure of behavioural difference for labelled Markov chains, but it may be discontinuous under perturbations of the transition probabilities. This lack of continuity…

Parameterized verification of finite-state processes with rendez-vous synchronization is notoriously undecidable when processes are linearly ordered. In this paper we study two kinds of bounds under which we determine the complexity of…

The reachability problem for Vector Addition Systems (VAS) is a central decision problem in the theory of infinite-state systems, first solved by Kosaraju and Mayr in the 1980s. An alternative, conceptually simpler approach introduced by…

The Jumping Abstract Machine (JAM), an evaluation mechanism for the $\lambda$-calculus, was introduced by Danos and Regnier as an optimization of the Interaction Abstract Machine (IAM), itself an operational counterpart to Girard's Geometry…

We present a Lean formalization of a general hybrid modal logic with many-sorted signatures and polyadic modal operators. The system borrows ideas from both algebraic specification and dynamic logics, and is designed to serve as a uniform…

We investigate the complexity of the model checking problem for distributed knowing how. We show that the problem is $\Delta^p_2$-complete.

We present AXLE (Axiom Lean Engine), a cloud service for Lean 4 proof manipulation, extraction, and verification. Recent progress in AI for mathematics -- reinforcement learning pipelines, agentic proving workflows, dataset curation --…

The increasing integration of deep neural networks in critical systems has spawned a theoretical and practical interest in formally guaranteeing safety properties about their behavior. To achieve this, contemporary verification algorithms…

We describe a verification pipeline that takes production Rust cryptographic code and produces machine-checked correctness proofs in Lean 4. The pipeline combines three components: symbolic extraction tools (Charon and Aeneas, or Hax) that…

Certification for Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas (DQBF) is an ongoing challenge. Recent proof complexity work has shown that the majority of QBF and DQBF techniques can be p-simulated by using…

Monotonic semantic path orders and weighted path orders are powerful reduction orders for proving termination of term rewrite systems. In this paper we present their simple unification as reduction orders and reduction pairs. We also…

We present mstlo (mistletoe), a Rust library for high-performance online monitoring of signal temporal logic (STL), with Python bindings. The library provides: (i) a unified interface for multiple STL semantics, including Robust…

Automated theorem proving systems built on Lean 4 increasingly rely on parallel tactic search over partially specified proofs, such as those generated by Draft-Sketch-Prove (DSP) pipelines. In current systems, each search branch…

This paper introduces LTLF, a temporal logic designed to express the frequency properties of event series in a natural but rigorous manner. By introducing novel, measure-sensitive operators, LTLF allows for the evaluation of frequencies and…

In recent years, numerous techniques were developed to automatically prove termination of different kinds of probabilistic programs. However, there are only few automated methods to disprove their termination. In this paper, we present the…

Building on ideas of Gurevich and Shelah for the G\"odel Class, we present a new probabilistic proof of the finite model property for the Guarded Fragment of First-Order Logic. Our proof is conceptually simple and yields the optimal…

The classical Church synthesis problem, solved by Buchi and Landweber, treats the synthesis of finite state systems. The synthesis of infinite state systems, on the other hand, has only been investigated few times since then, with no…

LLMs are increasingly used for software modernization, code translation, and database migration. However, LLM-based Oracle2PostgreSQL migration remains constrained by high token consumption, long-context degradation, dialect-specific…