计算机科学中的逻辑

In systems modelling, a 'system' typically comprises located resources relative to which processes execute. One important use of logic in informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their…

Many important computational structures involve an intricate interplay between algebraic features (given by operations on the underlying set) and relational features (taking account of notions such as order or distance). This paper…

In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. In this paper, we explore the concept of equilibrium design, where incentives are designed to obtain a…

Arboreal categories, introduced by Abramsky and Reggio, axiomatise categories with tree-shaped objects. These categories provide a categorical language for formalising behavioural notions such as simulation, bisimulation, and…

We study the equivalence between eval-readback and eval-apply big-step evaluators in the general setting of the pure lambda calculus. We study `one-step' equivalence (same strategy) and also discuss `big-step' equivalence (same final…

A set of configurations $H$ is a home-space for a set of configurations $X$ of aPetri net if every configuration reachable from (any configuration in) $X$ can reach (some configuration in) $H$. The semilinear home-space problem for Petri…

In this paper we combine the principled approach to modalities from multimodal type theory (MTT) with the computationally well-behaved realization of identity types from cubical type theory (CTT). The result -- cubical modal type theory…

In adaptive systems, predictors are used to anticipate changes in the systems state or behavior that may require system adaption, e.g., changing its configuration or adjusting resource allocation. Therefore, the quality of predictors is…

The connection between inconsistent databases and Dung's abstract argumentation framework has recently drawn growing interest. Specifically, an inconsistent database, involving certain types of integrity constraints such as functional and…

We present the type system $\mathtt{d}$, an extended type system with lambda-typed lambda-expressions. It is related to type systems originating from the Automath project. $\mathtt{d}$ extends existing lambda-typed systems by an existential…

We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by…

The rise of digital platforms has led to an increasing reliance on technology-driven, home-based healthcare solutions, enabling individuals to monitor their health and share information with healthcare professionals as needed. However,…

Over the past two decades, the Web Ontology Language (OWL) has been instrumental in advancing the development of ontologies and knowledge graphs, providing a structured framework that enhances the semantic integration of data. However, the…

Reasoning about strategic abilities is key to AI systems comprising multiple agents, which provide a unified framework for formalizing various problems in game theory, social choice theory, etc. In this work, we propose a probabilistic…

An equivalence relation can be constructed from a given (homogeneous, binary) relation in two steps: first, construct the smallest reflexive and transitive relation containing the given relation (the "star" of the relation) and, second,…

Continuous double auctions are commonly used to match orders at currency, stock, and commodities exchanges. A verified implementation of continuous double auctions is a useful tool for market regulators as they give rise to automated…

The paper "Sorting with Bialgebras and Distributive Laws" by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using…

The Participants-as-Interfaces (PaI) approach to system composition suggests that participants of a system may be viewed as interfaces. Given a set of systems,one participant per system is chosen to play the role of an interface. When…

A provenance analysis for a query evaluation or a model checking computation extracts information on how its result depends on the atomic facts of the model or database. Traditional work on data provenance was, to a large extent, restricted…

Stock and flow diagrams are already an important tool in epidemiology, but category theory lets us go further and treat these diagrams as mathematical entities in their own right. In this chapter we use communicable disease models created…