计算机科学中的逻辑

Probabilistic partial observability is a phenomenon occuring when computer systems are deployed in environments that behave probabilistically and whose exact state cannot be fully observed. In this work, we lay the theoretical groundwork…

We present a tractable, incremental framework for topological dialogue semantics based on finite, discrete semantic spaces. Building on the intuition that utterances correspond to open sets and their combinatorial relations form a…

Deep reinforcement learning has emerged as a powerful tool for obtaining high-performance policies. However, the safety of these policies has been a long-standing issue. One promising paradigm to guarantee safety is a shield, which shields…

We present a novel formal system for proving quantitative-leakage properties of programs. Based on a theory of Quantitative Information Flow (QIF) that models information leakage as a noisy communication channel, it uses "gain-functions"…

Spoiler-Duplicator games are used in finite model theory to examine the expressive power of logics. Their strategies have recently been reformulated as coKleisli maps of game comonads over relational structures, providing new results in…

In the setting of Petri nets, we prove that {\em causal-net bisimilarity} \cite{G15,Gor22,Gor25a}, which is a refinement of history-preserving bisimilarity \cite{RT88,vGG89,DDM89}, and the novel {\em hereditary} causal-net bisimilarity,…

We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations -- which axiomatise the usual notion of sets-with-relations -- provide a clean…

Containers are used to carve out a class of strictly positive data types in terms of shapes and positions. They can be interpreted via a fully-faithful functor into endofunctors on Set. Monadic containers are those containers whose…

Fixpoints are ubiquitous in computer science and when dealing with quantitative semantics and verification one often considers least fixpoints of (higher-dimensional) functions over the non-negative reals. We show how to approximate the…

We address the decision problem for a fragment of real analysis involving differentiable functions with continuous first derivatives. The proposed theory, besides the operators of Tarski's theory of reals, includes predicates for…

In this report we define an encoding of Levys call-by-push-value lambda-calculus (CBPV) in the pi-calculus, and prove that our encoding is both sound and complete. We present informal (by-hand) proofs of soundness, completeness, and all…

The present dissertation introduces the research project on HOLMS (\textbf{HOL} Light Library for \textbf{M}odal \textbf{S}ystems), a growing modular framework for modal reasoning within the HOL Light proof assistant. To provide an…

Termination analysis of C programs is a challenging task. On the one hand, the analysis needs to be precise enough to draw meaningful conclusions. On the other hand, relevant programs in practice are large and require substantial…

This paper presents a proof-theoretic analysis of the modal $\mu$-calculus. More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal $\mu$-calculus, using methods from linear logic and its exponential modalities.…

Realizability interprets propositions as specifications for computational entities in programming languages. Specifically, syntactic realizability is a powerful machinery that handles realizability as a syntactic translation of propositions…

Modern verification tools for deep neural networks (DNNs) increasingly rely on abstraction to scale to realistic architectures. In parallel, proof production is becoming a critical requirement for increasing the reliability of DNN…

Partial Combinatory Algebras (PCAs) provide a foundational model of the untyped $\lambda$-calculus and serve as the basis for many notions of computability, such as realizability theory. However, PCAs support a very limited notion of…

Viewing formal mathematical proofs as logical terms provides a powerful and elegant basis for analyzing how human experts tend to structure proofs and how proofs can be structured by automated methods. We pursue this approach by (1)…

In a quest to thoroughly understand the first-order transduction hierarchy of hereditary graph classes, some questions in particular stand out; such as, what properties hold for graph classes that are first-order transductions of planar…

We develop and investigate a general theory of representations of second-order functionals, based on a notion of a right comodule for a monad on the category of containers. We show how the notion of comodule representability naturally…