计算机科学中的逻辑

Electronic voting procedures are implementations of electoral systems, making it possible to conduct polls or elections with the help of computers. This paper reports on the development of an open-source library of electronic voting…

Given a Boolean relational specification between inputs and outputs, the problem of functional synthesis is to construct a function that maps each assignment of the input to an assignment of the output such that each tuple of input and…

We propose to extend the Dafny system with an interactive proof mode. We present a motivating example, how the IPM works, including the main design choices we make, and a prototype implementation.

Containers conveniently represent a wide class of inductive data types. Their derivatives compute representations of types of one-hole contexts, useful for implementing tree-traversal algorithms. In the category of containers and cartesian…

The Seifert-van Kampen theorem computes the fundamental group of a space from the fundamental groups of its constituents. We develop a modular SVK framework within the setting of computational paths - an approach to equality where witnesses…

Effectful Mealy machines, which we introduce, are a generalization of Mealy machines with global effects determined by an effectful triple. We provide semantics of effectful Mealy machines in terms of both bisimilarity and traces:…

In many real-life settings, agents must navigate dynamic environments while reasoning under incomplete information and acting on a corpus of unstable, context-dependent, and often conflicting norms. We introduce a general, non-modal,…

FC is a first-order logic that reasons over all factors of a finite word using concatenation, and can define non-regular languages like that of all squares (ww). In this paper, we establish that there are regular languages that are not…

In open multi-agent agent systems that cross organisational boundaries, agent actions must be regulated by complex policies. Consider medical data processing systems, which must observe generic laws (e.g., EU data protection regulations)…

The author has recently introduced an abstract algebraic framework of analogical proportions within the general setting of universal algebra. The purpose of this paper is to lift that framework from universal algebra to the strictly more…

We propose a new cubical type theory, termed (self-deprecatingly) the naive cubical type theory, and study its semantics using the universe category framework, which is similar to Uemura's categories with representable morphisms. In…

Hemaspaandra~et~al.~[JCSS 2010] conjectured that satisfiability for multi-modal logic restricted to the connectives XOR and 1, over frame classes T, S4, and S5, is solvable in polynomial time. We refute this for S5 frames, by proving…

We introduce Lambda-SX, a typed quantum lambda-calculus that supports multiple measurement bases. By tracking duplicability relative to arbitrary bases within the type system, Lambda-SX enables more flexible control and compositional…

We introduce a proof language for Intuitionistic Multiplicative Additive Linear Logic (IMALL), extended with a modality B to capture mixed-state quantum computation. The language supports algebraic constructs such as linear combinations,…

We introduce the $L_!^S$-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic (ILL). These algebraic operations enable the direct expression…

We note that Weihrauch problems can be regarded as containers over the category of projective represented spaces and that Weihrauch reductions correspond exactly to container morphisms. We also show that Bauer's extended Weihrauch degrees…

We present the first formal correctness proof of Edmonds' blossom shrinking algorithm for maximum cardinality matching in general graphs. We focus on formalising the mathematical structures and properties that allow the algorithm to run in…

Traditional approaches to modelling parallelism and algebraic structure in lambda calculi often rely on monads$\unicode{x2013}$as in Moggi's framework$\unicode{x2013}$or on rich categorical structures such as biproducts$\unicode{x2013}$as…

We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a…

The correct use of a Hardware Abstraction Layer (HAL) interface in embedded applications is crucial to prevent malfunctions, crashes, or even hardware damage. Software model checking has been successfully applied to check interface…