计算机科学中的逻辑

The Boolean satisfiability problem (SAT) holds a central place in computational complexity theory as the first shown NP-complete problem. Due to this role, SAT is often used as the benchmark for polynomial-time reductions: if a problem can…

A system $\boldsymbol\lambda_{\theta}$ is developed that combines modal logic and simply-typed lambda calculus, and that generalizes the system studied by Montague and Gallin. Whereas Montague and Gallin worked with Church's simple theory…

We introduce a first-order quantum programming language, named FOQ, whose terminating programs are reversible. We restrict FOQ to a strict and tractable subset, named PFOQ, of terminating programs with bounded width, that provides a first…

Let a quantified inequality constraint over the reals be a formula in the first-order predicate language over the structure of the real numbers, where the allowed predicate symbols are $\leq$ and $<$. Solving such constraints is an…

Logical specifications are widely used to represent software systems and their desired properties. Under system degradation or environmental changes, commonly seen in complex real-world robotic systems, these properties may no longer hold…

We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a generic denotational reduction -- namely, a denotational…

This paper investigates the admissibility of the substitution rule in cyclic-proof systems. The substitution rule complicates theoretical case analysis and increases computational cost in proof search since every sequent can be a conclusion…

A bilateralist take on proof-theoretic semantics can be understood as demanding of a proof system to display not only rules giving the connectives' provability conditions but also their refutability conditions. On such a view, then, a…

This paper presents the first study of the complexity of the optimization problem for integer linear-exponential programs which extend classical integer linear programs with the exponential function $x \mapsto 2^x$ and the remainder…

\textbf{T-BAT} logic is a formal system designed to express the notion of informal provability. This type of provability is closely related to mathematical practice and is quite often contrasted with formal provability, understood as a…

In the context of 2-player zero-sum infinite-duration games played on (potentially infinite) graphs, the memory of an objective is the smallest integer k such that in any game won by Eve, she has a strategy with <= k states of memory. For…

We present a verification challenge based on the fractional cascading (FC) technique for accelerating repeated searches across a collection of sorted arrays. The specific context is nuclear cross section lookup in a simulation code, where a…

Sparse matrix vector multiplication (SpMV) is a fundamental kernel in scientific codes that rely on iterative solvers. In this first part of our work, we present both a sequential and a basic MPI parallel implementations of SpMV, aiming to…

Earth System Models (ESMs) are critical for understanding past climates and projecting future scenarios. However, the complexity of these models, which include large code bases, a wide community of developers, and diverse computational…

We describe a challenge problem for verification based on the MPICH implementation of MPI. The MPICH implementation includes several algorithms for allreduce, all of which should be functionally equivalent to reduce followed by broadcast.…

The dependency pair (DP) framework is one of the most powerful techniques for automatic termination and complexity analysis of term rewrite systems. While DPs were extended to prove almost-sure termination of probabilistic term rewrite…

The approach taken by Gheorghiu, Gu and Pym in their paper on giving a Base-extension Semantics for Intuitionistic Multiplicative Linear Logic is an interesting adaptation of the work of Sandqvist for IPL to the substructural setting. What…

We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not be unfolded in the remainder of a development; unfolding…

This volume contains the proceedings of the Verification of Scientific Software (VSS 2025) workshop, held on 4 May 2025 at McMaster University, Canada, as part of ETAPS 2025. VSS brings together researchers in software verification and…

We investigate an extension of nominal many-sorted signatures in which abstraction has a form of instantiation, called generalised concretion, as elimination operator (similarly to lambda-calculi). Expressions are then classified using a…