The famous asynchronous computability theorem (ACT) relates the existence of an asynchronous wait-free shared memory protocol for solving a task with the existence of a simplicial map from a subdivision of the simplicial complex representing the inputs to the simplicial complex representing the allowable outputs. The original theorem relies on a correspondence between protocols and simplicial maps in round-structured models of computation that induce a compact topology. This correspondence, however, is far from obvious for computation models that induce a non-compact topology, and indeed previous attempts to extend the ACT have failed. This paper shows that in every non-compact model, protocols solving tasks correspond to simplicial maps that need to be continuous. It first proves a generalized ACT for sub-IIS models, some of which are non-compact, and applies it to the set agreement task. Then it proves that in general models too, protocols are simplicial maps that need to be continuous, hence showing that the topological approach is universal. Finally, it shows that the approach used in ACT that equates protocols and simplicial complexes actually works for every compact model. Our study combines, for the first time, combinatorial and point-set topological aspects of the executions admitted by the computation model.

Joint work with Hagit Attiya and Armando Castañeda.

Lawvere’s (hyper-)doctrines are a categorical tool that allows the analysis of both the syntax and the semantics of logical theories using the same mathematical structure. In this talk, we explore a possible interpretation of Henkin’s Theorem for first-order logic (“Every consistent theory has a model”) via bounded implicational existential doctrines. To achieve this goal, at first we study the meaning in the framework of doctrines of “adding a constant to a language” and “adding an axiom to a theory”. Then, starting from a consistent doctrine, we use these construction to build a rich doctrine - in which every valid formula of the kind ∃xφ(x) there exists a witness constant c such that φ© holds. Finally, we show that a rich doctrine admits a model, i.e. a morphism towards the subset doctrine. Henkin’s Theorem for doctrines follows from these results, and our proof is modelled on the main lines of the original one.

We will present a very general syntax that aims to export tools and techniques found in linear logic (intersection types, Taylor and Böhm approximations, geometry of interaction…) in a systematic way in other languages or calculus. That being still a work in progress, details will be given in a restriction of this syntax, in which we present an axiomatic definition of “approximation system”, based on a notion of fibration, aiming to capture this phenomenon as generally as possible. In this talk, we will explore the immediate consequences of the definition, introduce several concrete instances of it, and obtain well-known theorems as direct applications of the general framework.