My Keynote Presentation at the recent ESRC Public Policy Seminar on the Economics of Information Security is summarized in the ESRC Report.
A Logical and Computational Theory of Located Resource. Joint work with Matthew Collinson and Brian Monahan. Submitted to a journal. Available as an HP Labs Technical Report: HPL-2008-74.
Abstract. Experience of practical systems modelling suggests that the key conceptual components of a model of a system are processes, resources, locations, and environment. In recent work, we have given a process-theoretic account of this view in which resources as well as processes are first-class citizens. This process calculus, SCRP, captures the structural aspects of the semantics of the Demos2k modelling tool. Demos2k represents environment stochastically using a wide range of probability distributions and queue-like data structures. Associated with SCRP is a (bunched) modal logic, MBI, which combines the usual additive connectives of Hennessy-Milner logic with their multiplicative counterparts. In this paper, we complete our conceptual framework by adding to SCRP and MBI an account of a notion of location that is simple yet sufficiently expressive to capture naturally a wide range of forms of location, both spatial and logical. We also provide a sketch of an extension of the Demos2k tool to incorporate this notion of location.
Modelling the Human and Technological Costs and Benefits of USB Memory Stick Security. Joint work with Adam Beautement et al. Available from Proc. WEIS 2008. Preprint of a chapter in an associated forthcoming Springer book.
Abstract. Organizations deploy systems technologies in order to support their operations and achieve their business objectives. In so doing, they encounter tensions between the confidentiality, integrity, and availability of information, and must make investments in information security measures to address these concerns. We discuss how a macroeconomics-inspired model, analogous to models of interest rate policy used by central banks, can be used to understand trade-offs between investments against threats to confidentiality and availability. We investigate how such a model might be formulated by constructing a process model, based on empirically obtained data, of the use of USB memory sticks by employees of a financial management company.
Some recent HP Labs Technical Reports on topics related to services sciences and other topics. Some of these papers have been published elsewhere (conferences, journals, etc.).
Located Demos2k: A Tool for Executing Processes Relative to Distributed Resources. Joint work with Matthew Collinson and Brian Monahan. Submitted. Available as an HP Labs Technical Report: HPL-2008-76.
Abstract. We describe the background to, and the current state of the development of, Located Demos2k, an executable modelling language which reconstructs the Demos2k language starting from an explicit model of location. The version of Located Demos2k described herein is the first useful stage in its development, and provides convenient a point of departure of discussing its further development.
Algebra and Logic for Access Control. Joint work with Matthew Collinson. Submitted to a journal. Available as an HP Labs Technical Report: HPL-2008-75.
Abstract. The access control problem in computer security is fundamentally concerned with the ability of system entitites to see, make use of, or alter various system resources. As such, many access control situations are essentially problems of concurrency. We give an account of fundamental situations in access-control in distributed systems using a resource-based process calculus and a hybrid of Hennessy-Milner and resource logic. This yields a consistent account of operational behaviour and logical reasoning for access control, that includes an analysis of co-signing, roles and chains-of-trust.
Bunched Polymorphism. Joint work with Matthew Collinson and Edmund Robinson. To appear: Mathematical Structures in Computer Science, 2009. Preprint.
Abstract. We describe a polymorphic, typed lambda calculus with substructural features. This calculus extends the first-order substructural lambda calculus alphalambda associated with bunched logic. A particular novelty of our new calculus is the substructural treatment of second-order variables. This is accomplished through the use of bunches of type variables in typing contexts. Both additive and multiplicative forms of polymorphic abstraction are then supported. The calculus has sensible proof-theoretic properties and a straightforward categorical semantics using indexed categories. We produce a model for additive polymorphism with first-order bunching based on partial equivalence relations. We consider additive and multiplicative existential quantifiers separately from the universal quantifiers.
Algebra and Logic for Resource-based Systems Modelling. Joint work with Matthew Collinson. Submitted to a journal. Preprint.
Abstract. Modelling is one of the fundamental tools of science and engineering. Very often, models are required to be executable, as a simulation, on a computer. In this paper, we present some contributions to the process-theoretic and logical foundations of discrete-event modelling with resources and processes. We present a process calculus with an explicit representation of resources in which processes and resources co-evolve. The calculus is closely connected to a logic that may be used as a specification language for properties of models. The logic is strong enough to allow requirements that a system have certain structure; for example, that it is a parallel composite of subsystems. This work consolidates, extends, and improves upon aspects of the earlier works. An extended example, consisting of a semantics for a simple parallel programming language, indicates a connection with separating logics for concurrency.
A Games Model of Bunched Implications. Proc. CSL '07, LNCS 4646: 573-588. Joint work with Guy McCusker.
Abstract. A game semantics of the implicational fragment of the (-*,->)-fragment of the logic of bunched implications, BI, is presented. To date, categorical models of BI have been restricted to two kinds: functor category models; and the category Cat itself. The game model is not of this kind. Rather, it is based on Hyland-Ong-Nickau-style games and embodies a careful analysis of the notions of resource sharing and separation inherent in BI. he key to distinguishing between the additive and multiplicative connectives of BI is a semantic notion of separation. The main result of the paper is that the model is fully complete: every finite, total strategy in the model is the denotation of a term of the alphalambda-calculus, the term language for the fragment of BI under consideration.
Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic. Joint work with Chris Tofts.
Here is a preprint of ENTCS 172, 545-587, 2007. ENTCS 172 is entitled 'Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin'.
Abstract. We describe a programme of research in resource semantics, concurrency theory, bunched logic, and stochastic processes, as applied to mathematical systems modelling. Motivated by a desire for structurally and semantically rigorous discrete event modelling tools, applicable to enterprise-scale as well as component-scale systems, we introduce a new approach to compositional reasoning based on a development of SCCS with 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 simple denotational semantics as a parametrization of Abramsky's synchronization trees semantics for SCCS. We also 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. We discuss applications to ideas such as location and access control.
Formal Aspects of Computing, 18(4): 495-517, 2006.
Preprint here.
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.
Abstract. There are a number of applied lambda-calculi in which terms and types are annotated with parameters denoting either locations or locations in machine memory. Such calculi have been designed with safe memory-management operations in mind.
It is difficult to construct directly denotational models for existing calculi of this kind. We approach the problem differently, by starting from a class of mathematical models that describe some of the essential semantic properties intended in these calculi. In particular, disjointness conditions between regions (or locations) are implicit in many of the memory-management operations.
Bunched polymorphism provides natural type-theoretic mechanisms for capturing the disjointness conditions in such models. We illustrate this by adding regions to the basic disjointness model of $\alphalambda$, the lambda-calculus associated to the logic of bunched implications. We show how both additive and multiplicative polymorphic quantifiers arise naturally in our models. A locations model is a special case. In order to relate this enterprise back to previous work on memory-management, we provide an example in which the model is refined and used to provide a denotational semantics for a language with explicit allocation and disposal of regions.
In: Proc. MFPS 2006, S. Brookes and M. Mislove (editors), Electronic Notes in Theoretical Computer Science, 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.
Oxford Logic Guides, 45, Oxford University Press, 2004.
Errata and Remarks.
Mathematical Structures in Computer Science (2007) 17, 957-1027.
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) 5-53. Erratum: p. 32, side-condition of Resolution rule, replace index i by k and insert ``i ≤ k ≤ n,'' after the comma. Erratum also applies to the corresponding occurrence of the Resolution rule in the preprint (above, p. 26).
Erratum: In Proposition 4, ``DCC'' should be ``bicartesian DCC''.