Related papers: Name-free combinators for concurrency
This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation on terms obtained by…
We present two rewriting systems that define labelled explicit substitution lambda-calculi. Our work is motivated by the close correspondence between Levy's labelled lambda-calculus and paths in proof-nets, which played an important role in…
In this paper, we describe our participation in the RuTermEval competition devoted to extracting nested terms. We apply the Binder model, which was previously successfully applied to the recognition of nested named entities, to extract…
We introduce a new nameless representation of lambda terms inspired by ordered logic. At a lambda abstraction, number and relative position of all occurrences of the bound variable are stored, and application carries the additional…
Locks are a classic data structure for concurrent programming. We introduce a type system to ensure that names of the asynchronous pi-calculus are used as locks. Our calculus also features a construct to deallocate a lock once we know that…
We prove that the equational theory of the positive calculus of relations with transitive closure (PCoR*) is EXPSPACE-complete. Here, PCoR* terms consist of the following standard operators on binary relations: identity, empty,…
Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are "reasonably…
We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition…
We prove a free analogue of Brillinger's formula (sometimes called "law of total cumulance") which expresses classical cumulants in terms of conditioned cumulants. As expected, the formula is obtained by replacing the lattice of set…
In semantics and in programming practice, algebraic concepts such as monads or, essentially equivalently, (large) Lawvere theories are a well-established tool for modelling generic side-effects. An important issue in this context are…
It is well-known in the field of programming languages that dealing with variable names and binders may lead to conflicts such as undesired captures when implementing interpreters or compilers. This situation has been overcome by resorting…
We investigate an extension of nominal many-sorted signatures in which abstraction has a form of instantiation, called generalised concretion, as elimination operator (similarly to lambda-calculi). Expressions are then classified using a…
Combinatorial categories satisfy a stronger form of Yoneda Lemma, namely, the isomorphism type of an object can be recovered by counting the number of homomorphisms from all other objects into it. In this work, we show that this property…
We introduce labelled sequent calculi for the basic normal non-distributive modal logic L and 31 of its axiomatic extensions, where the labels are atomic formulas of a first order language which is interpreted on the canonical extensions of…
We obtain a criterion on the commutativity of polynomials in the enveloping algebra of a Lie algebra in terms of an involution condition with respect to the Berezin bracket. As an application, it is shown that the commutativity requirement…
In this paper we introduce a typed, concurrent $\lambda$-calculus with references featuring explicit substitutions for variables and references. Alongside usual safety properties, we recover strong normalization. The proof is based on a…
Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations, and explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all…
Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders,…
Using a new approach based on automatic sequences, logic, and a decision procedure, we reprove some old theorems about circularly squarefree words and unbordered conjugates in a new and simpler way. Furthermore, we prove three new results…
We consider anti-unification for simply typed lambda terms in associative, commutative, and associative-commutative theories and develop a sound and complete algorithm which takes two lambda terms and computes their generalizations in the…