Abstract. There are a number of applied lambda-calculi in which terms and types are annotated with parameters denoting either regions or locations in machine memory. Such calculi have been designed to have safe memory-management operations. Bunched polymorphism provides natural type-theoretic mechanisms for capturing the disjointness conditions implicit in many of these operations. The bunched type theory is accompanied by a quite general method for constructing models. We illustrate this by extending the Basic Disjointness Model of αλ with regions. We show how additive and multiplicative polymorphic quantifiers are interpreted. A locations model is a special case. The model is refined and used to provide a denotational semantics for a language with explicit allocation and deallocation of regions.
Revised version to appear in SPACE 2006, Charleston, South Carolina, 2006.
Abstract. We describe a polymorphic extension of the substructural lambda calculus alphalambda associated with the logic of bunched implications. This extension is particularly novel in that both variables and type variables are treated substructurally, being maintained through a system of zoned, bunched contexts. Polymorphic universal quantifiers are introduced in both additive and multiplicative forms, and then metatheoretic properties, including subject-reduction and normalization, are established. A sound interpretation in a class of indexed category models is defined and the construction of a generic model is outlined, yielding completeness. A concrete realization of the categorical models is given using pairs of partial equivalence relations on the natural numbers. Polymorphic existential quantifiers are presented, together with some metatheory. Finally, potential applications to closures and memory-management are discussed.
Proc. CSL 05, Lecture Notes in Computer Science 3634, 36-50, 2005.
Abstract. Theorem proving, or algorithmic proof-search, is an essential enabling technology throughout the computational sciences. We explain the mathematical basis of proof-search as the combination of reductive logic together with a control régime. Then we present a games semantics for reductive logic and show how it may be used to model two important examples of control, namely backtracking and uniform proof.
Proc. ETAPS 05 Workshop on Games for Logic and Programming Languages, Edinburgh, April, 2005.
HP Labs Technical Report HPL-2004-170R1, A Calculus and Logic of Resources and Processes. Joint work with Chris Tofts.
Abstract. Recent advances in logics for reasoning about resources provide a new approach to compositional reasoning in interacting systems. We present a calculus of resources and processes, based on a development of Milner's synchronous calculus of communication systems, SCCS, that uses an explicit model of resource. Our calculus models the co- evolution of resources and processes with synchronization constrained by the availability of resources. We provide a logical characterization, analogous to Hennessy-Milner logic's characterization of bisimulation in CCS, of bisimulation between resource processes which is compositional in the concurrent and local structure of systems.
Submitted to a journal.
Oxford Logic Guides, 45, Oxford University Press, 2004.
Errata and Remarks.
Last updated 18 January, 2005: added Section 3.3.1, on the duality of the monoids and comonoids. Submitted to a journal.
Abstract. It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. In previous work, summarized briefly herein, we have provided a class of models called classical categories which is sound and complete and avoids this collapse by interpreting cut-reduction by a poset-enrichment. Examples of classical categories include boolean lattices and the category of sets and relations, where both conjunction and disjunction are modelled by the set-theoretic product.
In this article, which is self-contained, we present an improved axiomatization of classical categories, together with a deep exploration of their structural theory. Observing that the collapse already happens in the absence of negation, we start with negation-free models called Dummett categories. Examples include, besides the classical categories above, the category of sets and relations, where both conjunction and disjunction are modelled by the disjoint union. We prove that Dummett categories are MIX, and that the partial order can be derived from hom-semilattices which have a straightforward proof-theoretic definition. Moreover, we show that the Geometry-of-Interaction construction can be extended from multiplicative linear logic to classical logic, by applying it to obtain a classical category from a Dummett category.
Along the way, we gain detailed insights into the changes that proofs undergo during cut-elimination in the presence of weakening and contraction.
Abstract. It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. We introduce sound and complete models that avoid this collapse by interpreting cut-reduction by a partial order between morphisms. We provide concrete examples of such models by applying the geometry-of-interaction construction to quantaloids with finite biproducts, and show hoe these models illuminate cut-reduction in the presence of weakening and contraction. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination.
Abstract. The logic of bunched implications, BI, provides a logical analysis of a basic notion of resource rich enough, for example, to form the logical basis for ``pointer logic'' and ``separation logic'' semantics for programs which manipulate mutable data structures. We develop a theory of semantic tableaux for BI, so providing an elegant basis for efficient theorem proving tools for BI. It is based on the use of an algebra of labels for BI's tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For BI with inconsistency, bottom, the challenge consists in dealing with BI's Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method TBI with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. Then, from these results, we can define a new resource semantics of BI, based on partially defined monoids, and prove that this semantics is complete. Such a semantics, based on partiality, is closely related to the semantics of BI's (intuitionistic) pointer and separation logics. Returning to the tableaux calculus, we propose a new version with liberalized rules for which the countermodels are closely related to the topological Kripke semantics of BI. As consequences of the relationships between semantics of BI and resource tableaux, we prove two strong new results for propositional BI: its decidability and the finite model property with respect to topological semantics.
Last updated 31 March, 2005.
Abstract. Since its earliest presentations, mathematical logic has been formulated as a formalization of deductive reasoning: given a collection of hypotheses, a conclusion is derived. However, the advent of computational logic has emphasized the significance of reductive reasoning: given a putative conclusion, what are sufficient premisses ? Whilst deductive systems typically have a well-developed semantics of proofs, reductive systems are typically well-understood only operationally. Typically, a deductive system can be read as a corresponding reductive system. The process of calculating a proof of a given putative conclusion, for which non-deterministic choices between premisses must be resolved, is called proof-search and is an essential enabling technology throughout the computational sciences. We suggest that the reductive view of logic is (at least) as fundamental as the deductive view and discuss some of the problems which must be addressed in order to provide a semantics of proof-searches of comparable value to the corresponding semantics of proofs. Just as the semantics of proofs is intimately related to the model theory of the underlying logic, so too should be the semantics of reductions and of proof-search. We discuss how to solve the problem of providing a semantics for proof-searches in intuitionistic logic which adequately models both not only the logical but also, via an embedding of intuitionistic reductive logic into classical reductive logic, the operational aspects, i.e., control of proof-search, of the reductive system.
Abstract. It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. Starting from a convenient formulation of the well-known categorical semantics of linear classical sequent proofs, we give models of weakening and contraction that do not collapse. Cut-reduction is interpreted by a partial order between morphisms. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination. We show soundness and completeness via initial models built from proof nets, and describe models built from sets and relations.
Last updated 7 March, 2005.
Errata and remarks applicable to this paper are available here.
Errata and remarks applicable to this paper are available here.
Theoretical Computer Science 232 (2000).
Erratum: In Proposition 4, `DCC' should be `bicartesian DCC'.