计算机科学中的逻辑

We introduce a meta-model based on formal languages, dubbed formal choreographic languages, to study message-passing systems. Our framework allows us to generalise standard constructions from the literature and to compare them. In…

In this paper we propose a new approach to realizability interpretations for nonstandard arithmetic. We deal with nonstandard analysis in the context of (semi)intuitionistic realizability, focusing on the Lightstone-Robinson construction of…

We consider relational semantics (R-models) for the Lambek calculus extended with intersection and explicit constants for zero and unit. For its variant without constants and a restriction which disallows empty antecedents, Andreka and…

Pomset logic and BV are both logics that extend multiplicative linear logic (with Mix) with a third connective that is self-dual and non-commutative. Whereas pomset logic originates from the study of coherence spaces and proof nets, BV…

Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the…

Semi-unification is the combination of first-order unification and first-order matching. The undecidability of semi-unification has been proven by Kfoury, Tiuryn, and Urzyczyn in the 1990s by Turing reduction from Turing machine immortality…

We generalize several propositional preprocessing techniques to higher-order logic, building on existing first-order generalizations. These techniques eliminate literals, clauses, or predicate symbols from the problem, with the aim of…

We study the expressive power and complexity of second-order revised Krom logic (SO-KROM$^{r}$). On ordered finite structures, we show that its existential fragment $\Sigma^1_1$-KROM$^r$ equals $\Sigma^1_1$-KROM, and captures NL. On all…

This paper introduces the exponential substitution calculus (ESC), a new presentation of cut elimination for IMELL, based on proof terms and building on the idea that exponentials can be seen as explicit substitutions. The idea in itself is…

The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential…

Causal reversibility blends reversibility and causality for concurrent systems. It indicates that an action can be undone provided that all of its consequences have been undone already, thus making it possible to bring the system back to a…

Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e., the absence of deadlock. Distributed algorithms often…

We consider a first-order logic for the integers with addition. This logic extends classical first-order logic by modulo-counting, threshold-counting and exact-counting quantifiers, all applied to tuples of variables (here, residues are…

Milner (1984) defined an operational semantics for regular expressions as finite-state processes. In order to axiomatize bisimilarity of regular expressions under this process semantics, he adapted Salomaa's proof system that is complete…

This paper connects the classes of weighted alternating finite automata (WAFA), weighted finite tree automata (WFTA), and polynomial automata (PA). First, we investigate the use of trees in the run semantics for weighted alternating…

Hyperproperties are system properties that relate multiple computation paths in a system and are commonly used to, e.g., define information-flow policies. In this paper, we study a novel class of hyperproperties that allow reasoning about…

We provide time lower bounds for sequential and parallel algorithms deciding bisimulation on labeled transition systems that use partition refinement. For sequential algorithms this is $\Omega((m \mkern1mu {+} \mkern1mu n ) \mkern-1mu \log…

We look in detail at the structural liveness problem (SLP) for subclasses of Petri nets, namely immediate observation nets (IO nets) and their generalized variant called branching immediate multi-observation nets (BIMO nets), that were…

We study the learnability of symbolic finite state automata (SFA), a model shown useful in many applications in software verification. The state-of-the-art literature on this topic follows the query learning paradigm, and so far all…

We apply program verification technology to the problem of specifying and verifying automatic differentiation (AD) algorithms. We focus on define-by-run, a style of AD where the program that must be differentiated is executed and monitored…