We propose a semantic foundation for logics for reasoning in settings that possess a distinction between equality of variables, a coarser equivalence of variables, and a notion of conditional independence between variables. We show that such relations can be modelled naturally in atomic sheaf toposes. Equivalence of variables is modelled by an intrinsic relation of atomic equivalence that is possessed by every atomic sheaf. We identify additional structure on the category generating the atomic topos (primarily, the existence of a system of independent pullbacks) that allows conditional independence to be interpreted in the topos. We then study the logic of equivalence and conditional independence that is induced by the internal logic of the topos. This atomic sheaf logic is a classical logic that validates a number of fundamental reasoning principles relating equivalence and conditional independence. As a concrete example of this abstract framework, we use the atomic topos over the category of surjections between finite nonempty sets as our main running example. In this category, the interpretations of equivalence and conditional independence coincide with those given by the multiteam semantics of independence logic, in which the role of equivalence is taken by the relation of mutual inclusion. A major difference from independence logic is that, in atomic sheaf logic, the multiteam semantics of the equivalence and conditional independence relations is embedded within a classical surrounding logic. At the end of the paper, we briefly outline two other instances of our framework, to demonstrate its versatility. The first of these is a category of probability sheaves, in which atomic equivalence is equality-in-distribution, and the conditional independence relation is the usual probabilistic one. Our other example is the Schanuel topos (equivalent to nominal sets) where equivalence is orbit equality and conditional independence amounts to a relative form of separatedness.

The article investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability , are satisfied by the modalities, then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe’s method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store, and input/output.

The "generic operational metatheory" of Johann, Simpson and Voigtländer (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on ground-type effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.

The paper investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability , are satisfied by the modalities then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe’s method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store and input/output.

I introduce the notion of probability sheaf, which is a mathematical structure capturing the relationship between probabilistic concepts (such as random variable) and sample spaces. Various probability-theoretic notions can be (re)formulated in terms of category-theoretic structure on the category of probability sheaves. As a main example, I consider the Giry monad, which, in its original formulation, constructs spaces of probability measures. I show that the Giry monad generalises to the category of probability sheaves, where it turns out to have a simple, purely category-theoretic definition.

The paper explores properties of the Łukasiewicz μ-calculus, or Łμ for short, an extension of Łukasiewicz logic with scalar multiplication and least and greatest fixed-point operators (for monotone formulas). We observe that Łμ terms, with n variables, define monotone piece-wise linear functions fr om [0, 1]n to [0, 1]. Two effective procedures for calculating the output of Łμ terms on rational inputs are presented. We then consider the Łukasiewicz modal μ-calculus, which is obtained by adding box and diamond modalities to Łμ. Alternatively, it can be viewed as a generalization of Kozen’s modal μ-calculus adapted to probabilistic nondeterministic transition systems (PNTS’s). We show how properties expressible in the well-known logic PCTL can be encoded as Łukasiewicz modal μ-calculus formulas. We also show that the algorithms for computing values of Łukasiewicz μ-calculus terms provide automatic (albeit impractical) methods for verifying Łukasiewicz modal μ-calculus properties of finite rational PNTS’s.

This article introduces the enriched effect calculus, which extends established type theories for computational effects with primitives from linear logic. The new calculus provides a formalism for expressing linear aspects of computational effects; e.g. the linear usage of imperative features such as state and/or continuations. The enriched effect calculus is implemented as an extension of a basic effect calculus without linear primitives, which is closely related to Moggi's computational metalanguage, Filinski's effect PCF and Levy's call-by-push-value. We present syntactic results showing: the fidelity of the behaviour of the linear connectives of the enriched effect calculus; the conservativity of the enriched effect calculus over its non-linear core (the effect calculus); and the non-conservativity of intuitionistic linear logic when considered as an extension of the enriched effect calculus. The second half of the article investigates models for the enriched effect calculus, based on enriched category theory. We give several examples of such models, relating them to models of standard effect calculi (such as those based on monads), and to models of intuitionistic linear logic. We also prove soundness and completeness.

This article formalizes and compares two different styles of reasoning with inductively defined predicates, each style being encapsulated by a corresponding sequent calculus proof system.The first system, LKID, supports traditional proof by induction, with induction rules formulated as rules for introducing inductively defined predicates on the left of sequents.We show LKID to be cut-free complete with respect to a natural class of Henkin models; the eliminability of cut follows as a corollary. The second system, LKIDω, uses infinite (non-well-founded) proofs to represent arguments by infinite descent. In this system, the left-introduction rules for inductively defined predicates are simple case-split rules, and an infinitary, global condition on proof trees is required in order to ensure soundness.We show LKIDω to be cut-free complete with respect to standard models, and again infer the eliminability of cut. The infinitary system LKIDω is unsuitable for formal reasoning. However, it has a natural restriction to proofs given by regular trees, i.e. to those proofs representable by finite graphs, which is so suited. We demonstrate that this restricted ‘cyclic’ proof system, CLKIDω, subsumes LKID, and conjecture that CLKIDω and LKID are in fact equivalent, i.e. that proof by induction is equivalent to regular proof by infinite descent.

We provide a syntactic analysis of contextual preorder and equivalence for a polymorphic programming language with effects. Our approach applies uniformly across a range of {algebraic effects}, and incorporates, as instances: errors, input/output, global state, nondeterminism, probabilistic choice, and combinations thereof. Our approach is to extend Plotkin and Power's structural operational semantics for algebraic effects (FoSSaCS 2001) with a primitive "basic preorder" on ground type computation trees. The basic preorder is used to derive notions of contextual preorder and equivalence on program terms. Under mild assumptions on this relation, we prove fundamental properties of contextual preorder (hence equivalence) including extensionality properties and a characterisation via applicative contexts, and we provide machinery for reasoning about polymorphism using relational parametricity.

I shall present an extension of Moggi's computational metalanguage with primitives from linear logic, the enriched effect-calculus. Illustrative applications to side effects, continuations, nondeterminism and polymorphism will be considered. The talk is based on joint work with Jeff Egger and Rasmus Mogelberg.

This paper compares two different styles of reasoning with inductively defined predicates, each style being encapsulated by a corresponding sequent calculus proof system. The first system supports traditional proof by induction, with induction rules formulated as sequent rules for introducing inductively defined predicates on the left of sequents. We show this system to be cut-free complete with respect to a natural class of Henkin models; the eliminability of cut follows as a corollary. The second system uses infinite (non-well-founded) proofs to represent arguments by infinite descent. In this system, the left rules for inductively defined predicates are simple case-split rules, and an infinitary, global condition on proof trees is required to ensure soundness. We show this system to be cut-free complete with respect to standard models, and again infer the eliminability of cut. The second infinitary system is unsuitable for formal reasoning. However, it has a natural restriction to proofs given by regular trees, i.e. to those proofs representable by finite graphs. This restricted "cyclic" system subsumes the first system for proof by induction. We conjecture that the two systems are in fact equivalent, i.e., that proof by induction is equivalent to regular proof by infinite descent.

According to Strachey, a polymorphic program is parametric if it applies a uniform algorithm independently of the type instantiations at which it is applied. The notion of relational parametricity, introduced by Reynolds, is one possible mathematical formulation of this idea. Relational parametricity provides a powerful tool for establishing data abstraction properties, proving equivalences of datatypes, and establishing equalities of programs. Such properties have been well studied in a pure functional setting. Many programs, however, exhibit computational effects. In this paper, we develop a framework for extending the notion of relational parametricity to languages with effects.

We prove two results for the sequential topology on countable products of sequential topological spaces. First we show that a countable product of topological quotients yields a quotient map between the product spaces. Then we show that the reflection from sequential spaces to its subcategory of monotone ω-convergence spaces preserves countable products. These results are motivated by applications to the modelling of computation on non-discrete spaces.

We propose compactly generated monotone convergence spaces as a well-behaved topological generalisation of directed-complete partial orders (dcpos). The category of such spaces enjoys the usual properties of categories of ‘predomains’ in denotational semantics. Moreover, such properties are retained if one restricts to spaces with a countable pseudobase in the sense of E. Michael, a fact that permits connections to be made with computability theory, realizability semantics and recent work on the closure properties of topological quotients of countably based spaces (qcb spaces). We compare the standard domain-theoretic constructions of products and function spaces on dcpos with their compactly generated counterparts, showing that these agree in important cases, though not in general.

We present a general axiomatic construction of models of FPC, a recursively typed lambda-calculus with call-by-value operational semantics. Our method of construction is to obtain such models as full subcategories of categorical models of intuitionistic set theory. This allows us to obtain a notion of model that encompasses both domain-theoretic and realizability models. We show that the existence of solutions to recursive domain equations, needed for the interpretation of recursive types, depends on the strength of the set theory. The internal set theory of an elementary topos is not strong enough to guarantee their existence. However, solutions to recursive domain equations do exist if models of intuitionistic Zermelo-Fraenkel set theory are used instead We apply this result to interpret FPC, and we provide necessary and sufficient conditions on a model for the interpretation to be computationally adequate, i.e. for the operational and denotational notions of termination to agree.

There are two main approaches to obtaining ‘topological’ cartesian-closed categories. Under one approach, one restricts to a full subcategory of topological spaces that happens to be cartesian closed – for example, the category of sequential spaces. Under the other, one generalises the notion of space – for example, to Scott's notion of equilogical space. In this paper, we show that the two approaches are equivalent for a large class of objects. We first observe that the category of countably based equilogical spaces has, in a precisely defined sense, a largest full subcategory that can be simultaneously viewed as a full subcategory of topological spaces. In fact, this category turns out to be equivalent to the category of all quotient spaces of countably based topological spaces. We show that the category is bicartesian closed with its structure inherited, on the one hand, from the category of sequential spaces, and, on the other, from the category of equilogical spaces. We also show that the category of countably based equilogical spaces has a larger full subcategory that can be simultaneously viewed as a full subcategory of limit spaces. This full subcategory is locally cartesian closed and the embeddings into limit spaces and countably based equilogical spaces preserve this structure. We observe that it seems essential to go beyond the realm of topological spaces to achieve this result.

We propose a notion of interval object in a category with finite products, providing a universal property for closed and bounded real line segments. The universal property gives rise to an analogue of primitive recursion for defining computable functions on the interval. We use this to define basic arithmetic operations and to verify equations between them. We test the notion in categories of interest. In the category of sets, any closed and bounded interval of real numbers is an interval object. In the category of topological spaces, the interval objects are closed and bounded intervals with the Euclidean topology. We also prove that an interval object exists in and elementary topos with natural numbers object.

We give an axiomatic treatment of fixed-point operators in categories. A notion of iteration operator is defined embodying the equational properties of iteration theories. We prove a general completeness theorem for iteration operators, relying on a new, purely syntactic characterisation of the free iteration theory. We then show how iteration operators arise in axiomatic domain theory. One result derives them from the existence of sufficiently many bifree algebras (exploiting the universal property Freyd introduced in his notion of algebraic compactness). Another result shows that, in the presence of a parameterized natural numbers object and an equational lifting monad, any uniform fixed-point operator is necessarily an iteration operator.

We axiomatize a notion of "classic structure" on a regular category, isolating the essential properties of the category of classes together with its full subcategory of sets. Like the axioms for a topos, our axiomatization is very simple, but has powerful consequences. In particular, we show that our axiomatized categories provide a sound and complete class of models for intuitionistic Zermelo-Fraenkel set theory.

We propose a uniform way of isolating a subcategory of predomains within the category of modest sets determined by a partial combinatory algebra (PCA). Given a divergence on a PCA (which determines a notion of partiality), we identify a candidate category of predomains, the well-complete objects. We show that, whenever a single strong completeness axiom holds, the category satisfies appropriate closure properties. We consider a range of examples of PCAs with associated divergences and show that in each case the axiom does hold. These examples encompass models allowing a ‘parallel’ style of computation (for example, by interleaving), as well as models that seemingly allow only ‘sequential’ computation, such as those based on term-models for the lambda-calculus. Thus, our approach provides a uniform approach to domain theory across a wide class of realizability models. We compare our treatment with previous approaches to domain theory in realizability models. It appears that no other approach applies across such a wide range of models.

We present a sequent calculus for proving that processes in a process algebra satisfy assertions in Hennessy-Milner logic. The main novelty lies in the use of the operational semantics to derive introduction rules (on the left and right of sequents) for the different operators of the process calculus. This gives a generic proof system applicable to any process algebra with an operational semantics specified in the GSOS format. We identify the desirable property of compositionality with cut-elimination, and we prove that this holds for a class of sequents. Further, we show that the proof system enjoys good completeness and /spl omega/-completeness properties relative to its intended model.