计算机科学中的逻辑

This volume contains the proceedings of the 20th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2025), which was held in Brasilia, the capital of Brazil, from October 7 to October 8, 2025. The aim of the LSFA series of…

Although they differ in the functionality they offer, low-level systems exhibit certain patterns of design and utilization of computing resources. In this paper, we argue the position that modalities, in the sense of modal logic, should be…

We present a universal construction of Diophantine equations with bounded complexity in Isabelle/HOL. This is a formalization of our own work in number theory. Hilbert's Tenth Problem was answered negatively by Yuri Matiyasevich, who showed…

Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to generate proof terms and synthesize programs. The tactic…

Over more than three decades, the Situation Calculus has established itself as an elegant, powerful, and concise formalism for specifying dynamical domains as well as for reasoning about the effects of actions of those domains both in the…

Safety-critical systems use redundant input units to improve their reliability and fault tolerance. A voting logic is then used to select a reliable input from the redundant sources. A fault detection and isolation rules help in selecting…

This paper undertakes a foundational inquiry into logical inferentialism with particular emphasis on the normative standards it establishes and the implications these pose for classical logic. The central question addressed herein is: 'What…

We present an adequacy theorem for a concurrent extension of probabilistic GCL. The underlying denotational semantics is based on the so-called mixed powerdomains, which combine non-determinism with probabilistic behaviour. The theorem…

The ABC conjecture implies many conjectures and theorems in number theory, including the celebrated Fermat's Last Theorem. Mason-Stothers Theorem is a function field analogue of the ABC conjecture that admits a much more elementary proof…

Recent works have shown that defining a behavioural equivalence that matches the observational properties of a quantum-capable, concurrent, non-deterministic system is a surprisingly difficult task. We explore coalgebras over distributions…

Reverse differentiation is an essential operation for automatic differentiation. Cartesian reverse differential categories axiomatize reverse differentiation in a categorical framework, where one of the primary axioms is the reverse chain…

We modify Gurevich's definition of sequential algorithms, so that it becomes amenable to computation with arbitrarily large sets on a sufficiently intuitive level. As a result, two classes of abstract algorithms are obtained, namely…

We present a complete formalization in Isabelle/HOL of the object part of an equivalence between L-mosaics and bounded join-semilattices, employing an AI-assisted methodology that integrates large language models as reasoning assistants…

We present a linearity theorem for a proof language of intuitionistic multiplicative additive linear logic, incorporating addition and scalar multiplication. The proofs in this language are linear in the algebraic sense. This work is part…

Proceedings of the Seventh International Conference on Applied Category Theory, held at the University of Oxford on 17 - 21 June 2024. The contributions to ACT 2024 ranged from pure to applied and included contributions in a wide range of…

Explainable systems expose information about why certain observed effects are happening to the agents interacting with them. We argue that this constitutes a positive flow of information that needs to be specified, verified, and balanced…

Skeletal call-by-need is an optimization of call-by-need evaluation also known as "fully lazy sharing": when the duplication of a value has to take place, it is first split into "skeleton", which is then duplicated, and "flesh" which is…

This paper investigates the proof-theoretic foundations of double negation introduction (DNI) and double negation elimination (DNE) in classical logic. By examining both sequent calculus and natural deduction, it is shown that these rules…

This paper establishes an equivalence between the halting problem in computability theory and the convergence of power series in mathematical analysis.

We introduce the G\"odel Mirror, a formal system defined in Lean 4 that treats contradiction as a control signal for recursive structural evolution. Inspired by G\"odelian self-reference, our system's operational semantics encode symbolic…