计算机科学中的逻辑

We study the interpretation of the lambda-calculus in a framework based on tropical mathematics, and we show that it provides a unifying framework for two well-developed quantitative approaches to program semantics: on the one hand program…

Rely/guarantee reasoning provides a compositional way of reasoning about concurrency. The ABA problem occurs in many non-blocking concurrent data structures, where a change made by a concurrent process may be undetected by other processes.…

We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory \`a la Buss (expressed in this new language) precisely capture polytime random functions. Then, we…

Monadically stable and monadically NIP classes of structures were initially studied in the context of model theory and defined in logical terms. They have recently attracted attention in the area of structural graph theory, as they…

Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development…

Refinement calculus provides a structured framework for the progressive and modular development of programs, ensuring their correctness throughout the refinement process. This paper introduces a refinement calculus tailored for quantum…

We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a…

This paper introduces Concurrent Valuation Algebras (CVAs), a novel extension of ordered valuation algebras (OVAs). CVAs include two combine operators representing parallel and sequential products, adhering to a weak exchange law. This…

We propose $\omega$MSO$\Join$BAPA, an expressive logic for describing countable structures, which subsumes and transcends both Counting Monadic Second-Order Logic (CMSO) and Boolean Algebra with Presburger Arithmetic (BAPA). We show that…

We introduce a new paradigm for analysing and finding bugs in quantum circuits. In our approach, the problem is given by a triple $\{P\}\,C\,\{Q\}$ and the question is whether, given a set $P$ of quantum states on the input of a circuit…

This document is an elementary introduction to string diagrams. It takes a computer science perspective: rather than using category theory as a starting point, we build on intuitions from formal language theory, treating string diagrams as…

The task of logic synthesis is to map a technology-independent representation of an application to hardware-specific operations, taking into account various constraints and trading off different costs associated with the implementation.…

Our goal is to define an algebraic language for reasoning about non-deterministic computations. Towards this goal, we introduce an algebra of string-to-string transductions. Specifically, it is an algebra of partial functions on words over…

We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky's univalent foundations. We observe for the first…

The k-d tree is a classic binary space-partitioning tree used to organize points in k-dimensional space. While used in computational geometry and graphics, the data structure has a long history of application in nearest neighbor search. The…

We use a labelled deduction system ( LND$_{ED-}$TRS ) based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type, which allowed us to carry out in homotopic theory an approach using…

Higher Type Arithmetic (HA$^w$) is a first-order many-sorted theory. It is a conservative extension of Heyting Arithmetic obtained by extending the syntax of terms to all of System T: the objects of interest here are the functionals of…

Graph-based interactive theorem provers offer a visual representation of proofs, explicitly representing the dependencies and inferences between each of the proof steps in a graph or hypergraph format. The number and complexity of these…

We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is…

Sequential logic synthesis can provide better Power-Performance-Area (PPA) than combinational logic synthesis since it explores a larger solution space. As the gate cost in advanced technologies keeps rising, sequential logic synthesis…