计算机科学中的逻辑

We investigate the isomorphism problem in the setting of definable sets (equivalent to sets with atoms): given two definable relational structures, are they related by a definable isomorphism? Under mild assumptions on the underlying…

Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstract completion, both for finite and infinite runs. For the…

We introduce two-player games which build words over infinite alphabets, and we study the problem of checking the existence of winning strategies. These games are played by two players, who take turns in choosing valuations for variables…

We present an algebraic account of the Wasserstein distances $W_p$ on complete metric spaces, for $p \geq 1$. This is part of a program of a quantitative algebraic theory of effects in programming languages. In particular, we give axioms,…

The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between B\"ohm trees. It is well known that the lambda-theory H*, arising by taking as observables the head normal…

This paper presents two decidability results on the validity checking problem for entailments of symbolic heaps in separation logic with Presburger arithmetic and arrays. The first result is for a system with arrays and existential…

This paper introduces a new family of models of intensional Martin-L\"of type theory. We use constructive ordered algebra in toposes. Identity types in the models are given by a notion of Moore path. By considering a particular gros topos,…

In the first part of this paper, we define two resource aware typing systems for the {\lambda}{\mu}-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial…

We investigate completeness and parametricity for a general class of realizability semantics for System F defined in terms of closure operators over sets of $\lambda$-terms. This class includes most semantics used for normalization…

We present the first polynomial time algorithm to learn nontrivial classes of languages of infinite trees. Specifically, our algorithm uses membership and equivalence queries to learn classes of $\omega$-tree languages derived from weak…

In the setting of constructive pointfree topology, we introduce a notion of continuous operation between pointfree topologies and the corresponding principle of pointfree continuity. An operation between points of pointfree topologies is…

Event structures are a well-accepted model of concurrency. In a seminal paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge between the theory of domains and the approach to concurrency proposed by Petri. A basic role…

We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian…

Environments and closures are two of the main ingredients of evaluation in lambda-calculus. A closure is a pair consisting of a lambda-term and an environment, whereas an environment is a list of lambda-terms assigned to free variables. In…

Let p/q be a rational number. Numeration in base p/q is defined by a function that evaluates each finite word over A_p={0,1,...,p-1} to some rational number. We let N_p/q denote the image of this evaluation function. In particular, N_p/q…

The purpose of this paper is to provide a construction to model shared-variable systems using higher-dimensional automata which is compositional in the sense that the parallel composition of completely independent systems is modeled by the…

Interpretation methods and their restrictions to polynomials have been deeply used to control the termination and complexity of first-order term rewrite systems. This paper extends interpretation methods to a pure higher order functional…

There are several approaches for using computers in deriving mathematical proofs. For their illustration, we provide an in-depth study of using computer support for proving one complex combinatorial conjecture -- correctness of a strategy…

This paper contributes to the theory of the modal $\mu$-calculus by proving some model-theoretic results. More in particular, we discuss a number of semantic properties pertaining to formulas of the modal $\mu$-calculus. For each of these…

We present FJ&$\lambda$, a new core calculus that extends Featherweight Java (FJ) with interfaces, supporting multiple inheritance in a restricted form, $\lambda$-expressions, and intersection types. Our main goal is to formalise how…