ABSTRACT. The differential λ-calculus studies how the quantitative aspects of programs correspond to differentiation and to Taylor expansion inside models of linear logic. Recent work has generalized the axioms of Taylor expansion so they apply to many models that only feature partial sums. However, that work does not cover the classic web based models of Köthe spaces and finiteness spaces. First, we provide a generic construction of web based models with partial sums. It captures models, ranging from coherence spaces to probabilistic coherence spaces, finiteness spaces and Köthe spaces. Second, we generalize the theory of Taylor expansion to models in which coefficients can be non-positive. We then use our generic web model construction to provide a unified proof that all the aforementioned web based models feature such Taylor expansion.

ABSTRACT. Quantum causal models extend classical causal models to quantum systems. In particular, Quantum Bayesian networks, first introduced in foundational work by Henson, Lal, and Pusey (2014) provide a mathematical formalism to describe causal relations, to analyse correlations, and to predict the probabilities of measurement outcomes, in systems involving both classical and quantum data. Such a framework generalizes Pearl's Bayesian networks—prominent graphical models for classical probabilistic reasoning and inference. Our paper brings compositional principles and a typing discipline into the setting of Quantum Bayesian Networks, with two main contributions. - First, a compositional semantics with a key feature: when all causes are classical, it coincides with the standard semantics of Bayesian networks (which is key to inference algorithms), while in the purely quantum case it reduces to tensor networks. - Second, a typed graphical formalism based on linear logic proof nets, where types ensure well-behaved composition of systems.

ABSTRACT. The purpose of this paper is to invite structural proof theorists to a challenging problem in substructural and fuzzy logics: the consistency of Cantor-Lukasiewicz naive set theory. To this end, we consider two logics: FLew (Full Lambek calculus with exchange and weakening) and its extension \L (Lukasiewicz' infinite-valued logic). The former is equivalently specified as the !-free intuitionistic linear logic with weakening, while the latter is the most important system of mathematical fuzzy logic. For each of them, we consider two extensions: one with simultaneous fixed points of formulas and the other with naive set theory with unrestricted comprehension, so that we end up with four systems: FLew-fix, FLew-set, \L-fix and \L-set. The first two admit an easy proof of consistency by cut elimination, while the third admits a proof by Brouwer's fixed point theorem. The last system \L-set (Cantor-Lukasiewicz set theory) is our main target. Although its consistency is still open, we prove the consistency of a restricted fragment.

ABSTRACT. Asynchronous effects of Ahman and Pretnar complement the conventional synchronous treatment of algebraic computational effects with asynchrony based on decoupling the execution of algebraic operation calls into signalling that an operation's implementation needs to be executed, and into interrupting a running computation with the operation's result, to which the computation can react by installing matching interrupt handlers. Beyond providing asynchrony for algebraic effects, the resulting core calculus also naturally models examples such as pre-emptive multi-threading, (cancellable) remote function calls, multi-party applications, and even a parallel variant of runners of algebraic effects. In this paper, we study the normalisation properties of this calculus. We prove that if one removes general recursion from the original calculus, then the remaining calculus is strongly normalising, including both its sequential and parallel parts. However, this only guarantees termination for very simple asynchronous examples. To improve on this result, we also prove that the sequential fragment of the calculus remains strongly normalising when a controlled amount of interrupt-driven recursive behaviour is reintroduced. Our strong normalisation proofs are structured compositionally as a natural extension of Lindley and Stark's $\top\top$-lifting based approach for proving strong normalisation of effectful languages. All our results are also formalised in Agda.

ABSTRACT. An all-path reachability (APR, for short) predicate is a pair of a source set and a target set, which are subsets of an object set. APR predicates have been defined for abstract reduction systems (ARSs, for short) and then extended to logically constrained term rewrite systems (LCTRSs, for short) as pairs of constrained terms that represent sets of terms modeling configurations, states, etc. An APR predicate is said to be partially (or demonically) valid w.r.t. a rewrite system if every finite maximal reduction sequence of the system starting from any element in the source set includes an element in the target set. Partial validity of APR predicates w.r.t. ARSs is defined by means of two inference rules, which can be considered a proof system to construct (possibly infinite) derivation trees for partial validity. On the other hand, a proof system for LCTRSs consists of four inference rules, and thus there is a gap between the inference rules for ARSs and LCTRSs. In this paper, we revisit the framework for APR analysis and adapt it to verification of not only safety but also liveness properties. To this end, we first reformulate an abstract framework for partial validity w.r.t. ARSs so that there is a one-to-one correspondence between the inference rules for partial validity w.r.t. ARSs and LCTRSs. Secondly, we show how to apply APR analysis to safety verification. Thirdly, to apply APR analysis to liveness verification, we introduce a novel stronger validity of APR predicates, called total validity, which requires not only finite but also infinite execution paths to reach target sets. Finally, for a partially valid APR predicate with a cyclic-proof tree, we show a necessary and sufficient condition for the tree to ensure total validity.

ABSTRACT. We are interested in proving input-output properties of functions that handle infinite data such as streams or non-wellfounded trees. We provide a finitary refinement type system which is (sound and) complete for Scott-open properties defined in a fixpoint-like logic. Working on top of Abramsky's Domain Theory in Logical Form, we build from the well-known fact that the Scott domains interpreting recursive types are spectral spaces. The usual symmetry between Scott-open and compact-saturated sets is reflected in logical polarities: positive formulae allow for least fixpoints and define Scott-open sets, while negative formulae allow for greatest fixpoints and define compact-saturated sets. A realizability implication with the expected (contra)variance on polarities allows for non-trivial input-output properties to be formulated as positive formulae on function types.