Runners in Action

Runners of algebraic effects, also known as comodels, provide a mathematical model of resource management. We show that they also give rise to a programming concept that models top-level external resources, as well as allows programmers to modularly define their own intermediate “virtual machines”. We capture the core ideas of programming with runners in an equational calculus $$\lambda _{\mathsf {coop}}$$ λ coop , which we equip with a sound and coherent denotational semantics that guarantees the linear use of resources and execution of finalisation code. We accompany $$\lambda _{\mathsf {coop}}$$ λ coop with examples of runners in action, provide a prototype language implementation in OCaml, as well as a Haskell library based on $$\lambda _{\mathsf {coop}}$$ λ coop .

Isomorphic objects in symmetric monoidal closed categories

This paper presents a new and self-contained proof of a result characterizing objects isomorphic in the free symmetric monoidal closed category, i.e., objects isomorphic in every symmetric monoidal closed category. This characterization is given by a finitely axiomatizable and decidable equational calculus, which differs from the calculus that axiomatizes all arithmetical equalities in the language with 1, product and exponentiation by lacking 1c=1 and (a · b)c =ac · bc (the latter calculus characterizes objects isomorphic in the free cartesian closed category). Nevertheless, this calculus is complete for a certain arithmetical interpretation, and its arithmetical completeness plays an essential role in the proof given here of its completeness with respect to symmetric monoidal closed isomorphisms.

Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic

A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1)Feasible interpolation theorems for the following proof systems:(a)resolution(b)a subsystem of LK corresponding to the bounded arithmetic theory (α)(c)linear equational calculus(d)cutting planes.(2)New proofs of the exponential lower bounds (for new formulas)(a)for resolution ([15])(b)for the cutting planes proof system with coefficients written in unary ([4]).(3)An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory (α).In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle.