Related papers: A finiteness structure on resource terms
We propose a functional description of rewriting systems on topological vector spaces. We introduce the topological confluence property as an approximation of the confluence property. Using a representation of linear topological rewriting…
A quantitative model of concurrent interaction is introduced. The basic objects are linear combinations of partial order relations, acted upon by a group of permutations that represents potential non-determinism in synchronisation. This…
We extend the recently introduced setting of coherent differentiation for taking into account not only differentiation, but also Taylor expansion in categories which are not necessarily (left)additive. The main idea consists in extending…
We present a technique to study normalizing strategies when termination is asymptotic, that is, it appears as a limit, as opposite to reaching a normal form in a finite number of steps. Asymptotic termination occurs in several settings,…
The topological interpretation of modal logics provides descriptive languages and proof systems for reasoning about points of topological spaces. Recent work has been devoted to model checking of spatial logics on discrete spatial…
Formalisms based on temporal logics interpreted over finite strict linear orders, known in the literature as finite traces, have been used for temporal specification in automated planning, process modelling, (runtime) verification and…
We define a new cost model for the call-by-value lambda-calculus satisfying the invariance thesis. That is, under the proposed cost model, Turing machines and the call-by-value lambda-calculus can simulate each other within a polynomial…
Continuous reducibilities are a proven tool in computable analysis, and have applications in other fields such as constructive mathematics or reverse mathematics. We study the order-theoretic properties of several variants of the two most…
We introduce the notion of finitary computable reducibility on equivalence relations on the natural numbers. This is a weakening of the usual notion of computable reducibility, and we show it to be distinct in several ways. In particular,…
In this paper, we define a realizability semantics for the simply typed $\lambda\mu$-calculus. We show that if a term is typable, then it inhabits the interpretation of its type. This result serves to give characterizations of the…
We first partly develop a mathematical notion of stable consistency intended to reflect the actual consistency property of human beings. Then we give a generalization of the first and second G\"odel incompleteness theorem to stably…
Regular cost functions have been introduced recently as an extension to the notion of regular languages with counting capabilities, which retains strong closure, equivalence, and decidability properties. The specificity of cost functions is…
We extend to singular cardinals the model-theoretical relation $\lambda \stackrel{\kappa}{\Rightarrow} \mu$ introduced in P. Lipparini, The compactness spectrum of abstract logics, large cardinals and combinatorial principles, Boll. Unione…
Resource theories provide a general framework for the characterization of properties of physical systems in quantum mechanics and beyond. Here, we introduce methods for the quantification of resources in general probabilistic theories…
We sketch a tentative proof of P-completeness for the $\beta$-convertibility problem on untyped planar (a.k.a. ordered or non-commutative) $\lambda$-terms.
We address the problem of complementing higher-order patterns without repetitions of existential variables. Differently from the first-order case, the complement of a pattern cannot, in general, be described by a pattern, or even by a…
In this paper, we consider a model of classical linear logic based on coherence spaces endowed with a notion of totality. If we restrict ourselves to total objects, each coherence space can be regarded as a uniform space and each linear map…
A $\lambda$-quiddity of size $n$ is an $n$-tuple of elements from a fixed set, which is a solution to a matrix equation that arises in the study of Coxeter's friezes. The study of these solutions involves in particular the use of a notion…
Many kinds of categorical structure require the existence of finite limits, of colimits of some specified type, and of "exactness" conditions between the finite limits and the specified colimits. Some examples are the notions of regular, or…
I present a model of universal parallel computation called $\Delta$-Nets, and a method to translate $\lambda$-terms into $\Delta$-nets and back. Together, the model and the method constitute an algorithm for optimal parallel…