计算机科学中的逻辑

We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable even for three processes each…

This paper introduces an ML / Haskell like programming language with nested inductive and coinductive algebraic datatypes called \chariot. Functions are defined by arbitrary recursive definitions and can thus lead to non-termination and…

A common technique for verifying the safety of complex systems is the inductive invariant method. Inductive invariants are inductive formulas that overapproximate the reachable states of a system and imply a desired safety property.…

This expository note describes two convenient techniques in the context of homotopy type theory for proving and formalizing that a given map is an equivalence. The first technique decomposes the map as a series of basic equivalences, while…

We report on the higher-order differential calculus library developed inside the Lean mathematical library mathlib. To support a broad range of applications, we depart in several ways from standard textbook definitions: we allow arbitrary…

Relational verification encompasses research directions such as reasoning about data abstraction, reasoning about security and privacy, secure compilation, and functional specificaton of tensor programs, among others. Several relational…

Suitable reachability conditions can make two different fixed point semantics of a transition system coincide. For instance, the total and partial expected reward semantics on Markov chains (MCs) coincide whenever the MC at hand is almost…

In the game-theoretic approach to controller synthesis, we model the interaction between a system to be controlled and its environment as a game between these entities, and we seek an appropriate (e.g., winning or optimal) strategy for the…

Reachability analysis of compositional hybrid systems, where individual components are modeled as hybrid automata, poses unique challenges. In addition to preserving the compositional semantics while computing system behaviors, algorithms…

This paper studies the verification of almost-sure B\"uchi objectives in MDPs with a known, compositional structure based on string diagrams. In particular, we ask whether there is a strategy that ensures that a B\"uchi objective is…

Wu's positive $\lambda$-calculus is a recent call-by-value $\lambda$-calculus with sharing coming from Miller and Wu's study of the proof-theoretical concept of focalization. Accattoli and Wu showed that it simplifies a technical aspect of…

We introduce Lattice Annotated Temporal (LAT) Logic, an extension of Generalized Annotated Logic Programs (GAPs) that incorporates temporal reasoning and supports open-world semantics through the use of a lower lattice structure. This logic…

Convex analysis and Gaussian probability are tightly connected, as mostly evident in the theory of linear regression. Our work introduces an algebraic perspective on such relationship, in the form of a diagrammatic calculus of string…

The stability rule for belief, advocated by Leitgeb [Annals of Pure and Applied Logic 164, 2013], is a rule for rational acceptance that captures categorical belief in terms of $\textit{probabilistically stable propositions}$: propositions…

We provide full certifications of two versions of merge sort of arrays in the verification-aware programming language Dafny. We start by considering schemas for applying the divide-and-conquer or partition method of solution to…

Chemical reactors are dynamic systems that can be described by systems of ordinary differential equations (ODEs). Reactor safety, regulatory compliance, and economics depend on whether certain states are reachable by the reactor, and are…

The goal of this paper is to establish that it remains undecidable whether a sequent is provable in two systems in which a weakening rule for an exponential modality is completely omitted from classical propositional linear logic…

This paper presents a theory of systemic undecidability, reframing incomputability as a structural property of systems rather than a localized feature of specific functions or problems. We define a notion of causal embedding and prove a…

We study L\"owenheim-Skolem and Omitting Types theorems in Transition Algebra, a logical system obtained by enhancing many sorted first-order logic with features from dynamic logic. The sentences we consider include compositions, unions,…

We develop the theory of continuous and algebraic domains in constructive and predicative univalent foundations, building upon our earlier work on basic domain theory in this setting. That we work predicatively means that we do not assume…