计算机科学中的逻辑

We present fully abstract encodings of the call-by-name and call-by-value $\lambda$-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the $\lambda$-calculus side --…

Quantum based systems are a relatively new research area for that different modelling languages including process calculi are currently under development. Encodings are often used to compare process calculi. Quality criteria are used then…

A classic result by Stockmeyer gives a non-elementary lower bound to the emptiness problem for star-free generalized regular expressions. This result is intimately connected to the satisfiability problem for interval temporal logic, notably…

We introduce a call-by-name lambda-calculus $\lambda Jn$ with generalized applications which is equipped with distant reduction. This allows to unblock $\beta$-redexes without resorting to the standard permutative conversions of generalized…

The pebbling comonad, introduced by Abramsky, Dawar and Wang, provides a categorical interpretation for the k-pebble games from finite model theory. The coKleisli category of the pebbling comonad specifies equivalences under different…

This paper presents a case study for the application of semiring semantics for fixed-point formulae to the analysis of strategies in B\"uchi games. Semiring semantics generalizes the classical Boolean semantics by permitting multiple truth…

We study the extent to which it is possible to approximate the optimal value of a Unique Games instance in Fixed-Point Logic with Counting (FPC). Formally, we prove lower bounds against the accuracy of FPC-interpretations that map Unique…

Inspired by a width invariant on permutations defined by Guillemot and Marx, Bonnet, Kim, Thomass\'e, and Watrigant introduced the twin-width of graphs, which is a parameter describing its structural complexity. This invariant has been…

When translating a term calculus into a graphical formalism many inessential details are abstracted away. In the case of $\lambda$-calculus translated to proof-nets, these inessential details are captured by a notion of equivalence on…

Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable interest in internalizing aspects of these presheaf models,…

Game comonads, introduced by Abramsky, Dawar and Wang and developed by Abramsky and Shah, give an interesting categorical semantics to some Spoiler-Duplicator games that are common in finite model theory. In particular they expose…

We extend the notion of compositional associative rewriting as recently studied in the rule algebra framework literature to the setting of rewriting rules with conditions. Our methodology is category-theoretical in nature, where the…

Session types are formal specifications of communication protocols, allowing protocol implementations to be verified by typechecking. Up to now, session type disciplines have assumed that the communication medium is reliable, with no loss…

We describe a general approach to deriving linear-time logics for a wide variety of state-based, quantitative systems, by modelling the latter as coalgebras whose type incorporates both branching and linear behaviour. Concretely, we define…

Preservation theorems provide a direct correspondence between the syntactic structure of first-order sentences and the closure properties of their respective classes of models. A line of work has explored preservation theorems relativised…

We robustify PCTL and PCTL*, the most important specification languages for probabilistic systems, and show that robustness does not increase the complexity of their model-checking problems.

In [1] the concept of CHTW-systems as a multidimensional representation of Petri nets was proposed based on the assumption of multidimensional distribution of tokens (resources) in positions (branes) and, accordingly, multidimensional…

Data dependencies are integrity constraints that the data of interest must obey. During the 1980s, Janos Makowsky made a number of contributions to the study of data dependencies; in particular, he was the first researcher to characterize…

In the last few years there have been rapid developments in SMT solving for finite fields. These include new decision procedures, new implementations of SMT theory solvers, and new software verifiers that rely on SMT solving for finite…

To advance formal verification of stochastic systems against temporal logic requirements for handling unknown dynamics, researchers have been designing data-driven approaches inspired by breakthroughs in the underlying machine learning…