Separating Network Layers. Joint work Matthew Collinson and Kevin McDonald.
Abstract. Complex systems, be they natural or synthetic, are ubiquitous. In particular, complex networks of devices and services underpin most of society's operations. By their very nature, such systems are difficult to conceptualize and reason about effectively. The concept of layering is widespread in complex systems, but has not been considered conceptually. Noting that graphs are a key formalism in the description of complex systems, we establish a notion of a layered graph. We provide a logical characterization of this notion of layering using a non-associative, non-commutative substructural, separating logic. We provide soundness and completeness results for a class of algebraic models that includes layered graphs, which give a mathematically substantial semantics to this very weak logic. We explain, via examples, applications in information processing and security.
Manuscript available here.
A Proof-theoretic Analysis of the Classical Matrix Method. Joint work with Eike Ritter and Edmund Robinson.
Abstract. The matrix method, due to Bibel and Andrews, is a proof procedure designed for automated theorem-proving. We show that underlying this method is a fully structured combinatorial model of conventional classical proof theory.
Manuscript available here. Submitted to a journal.
Contagion in Cybersecurity Attacks. Joint work with Adrian Baldwin, Iffat Gheyas, Christos Ioannidis, and Julian Williams.
Abstract. We develop and estimate a vector equation system of threats to ten important IP services, using SANS-reported data over the period January 2003 to February 2011. Our results reveal strong evidence of contagion between such attacks, with attacks on ssh and Secure Web Server indicating increased attack activity on other ports. Security managers who ignore such contagious inter-relationships may underestimate the underlying risk to their systems' defence of security attributes, such as sensitivity and criticality, and thus delay appropriate information security investments.
Manuscript available here. Accepted (with minor revisions) for presentation at WEIS 2012, Berlin.
Information Stewardship in the Cloud. Joint work with Simon Shiu. IISP Pulse 7 Winter 2011: 6-8.
Available here.
Enterprise information risk management: Dealing with cloud computing. Joint work with Adrian Baldwin and Simon Shiu. To appear: Privacy and Security for Cloud Computing: Selected Topics, Siani Pearson and George Yee (editors), Springer, Computer Communications and Networks series, 2012.
Abstract. Managing information risk is a complex task that must continually adapt to business and technology changes. We argue that cloud computing presents a more significant step change, and so implies a bigger change for the enterprise risk and security management lifecycle. Specifically, the economies of scale that large providers can achieve are creating an ecosystem of service providers in which the marketplace (rather than consuming enterprises) determines security standards and properties. Moreover, the ability to consume high-level services from different environments is changing the nature of one-size-fits-all security policies.
Manuscript available here.
The TSB-funded Trust Economics project Final Report.
Information Stewardship in Cloud Ecosystems: Towards Models, Economics, and Delivery. Joint work with Adrian Baldwin, Martin Sadler, and Simon Shiu. Preprint.
To appear: Proc. 2011 Third IEEE International Conference on Cloud Computing Technology and Science (CloudCom 2011). Copyright IEEE, 2011.
Abstract. We discuss the concept of information stewardship in cloud-based business ecosystems. The constituent concepts of stewardship --- which we believe will be crucial to the successful development of cloud-based business of all kinds --- extend those of security to encompass concepts such as values, ethics, resilience, and sustainability: all familiar from the stewardship of natural resources. Our view is based on rigorous approaches from mathematical systems modelling and economics, and is informed by concepts from natural resource management and information assurance.
Fixed Costs, Investment Rigidities, and Risk Aversion in Information Security: A Utility-theoretic Approach. Joint work with Christos Ioannidis and Julian Williams. Proc. WEIS 2011, George Mason University, Fairfax, Virginia, 14-15 June, 2011: WEIS 2011.
Proceedings to be published by Springer (Bruce Schneier, editor) 2011. In press.
Abstract. This paper introduces and demonstrates a simple analytically tractable method of mapping utility theory to information security problems and in particular optimal timing for vulnerability management. Our primary focus is on the decision to defer costly deterministic investment, such as the removal of a service or implementation of a security patch, when the costs associated with future security vulnerabilities are uncertain. We outline an investment function with fixed and variable costs that imports a nominal rigidity into the investment decision-making profile. The rigidity introduces a delay in the implementation of security measures, resulting in cyclical investments in information security. We show how such cycles emerge endogenously from the policy-maker's chosen trade-offs between system and security attributes.
Available from the WEIS 2011 site at here.
Information Stewardship: Systems Perspective, Systems Solutions. Slides from my Keynote presentation at Information Security Leaders (2011), Edinburgh, February 2011.
Available here.
The Structure and Dynamics of Systems Security Economics. Joint work with Adam Beautement.
Abstract. Structured systems security economics provides a conceptual framework, inspired by macroeconomic models of trade-offs and mathematical systems models, for analysing the structure of security architectures, their policy constraints, and their interactions with users. In this paper, we explore the dynamics of structured systems security economics by considering the representation and functionality of Actors in the framework. We show how a simple representation of Actors' preferences is sufficient to understand the security dynamics of the system and support utility calculations that inform design and investment decisions. Overall, the framework is intended to facilitate the design and implementation of trustworthy security systems.
Manuscript available here.
Economics of Information Security and Privacy. Co-editor with Tyler Moore and Christos Ioannidis. Springer New York Dordrecht Heidelberg London, 2010. doi: 10.1007/978-1-4419-6967-5.
Papers from WEIS 2009, the Eighth Workshop on the Economics of Information Security, UCL, June 24-25, 2009.
Available from Amazon.
Security Analytics: Bringing Science to Security Management. Joint work with Simon Shiu. IISP Pulse 4 Summer 2010: 12-13.
Available here.
Information Stewardship in the Cloud: A Model-based Approach. Joint work with Martin Sadler, Simon Shiu, and Marco Casassa Mont. To appear, Proc. CloudComp 2010, Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering (LNICST) series, Springer, 2010. Preprint.
Abstract. Managing the information stewardship lifecycle is a challenge. In the context of cloud computing, the stakeholders in cloud ecosystems must also take account of the demands of the information stewardship lifecycles of other participants in the ecosystem. We describe a modelling framework --- incorporating tools from mathematical systems modelling, economics, and policy/user modelling --- suitable for supporting reasoning and decision making in cloud ecosystems, and so provides a basis for developing model-based service level agreements.
Structured Systems Economics for Security Management. Joint work with Adam Beautement. Proc. WEIS 2010, Harvard University. Paper. Presentation.
Abstract. We develop an ontological account of information security architectures that is inspired by economic models of trade-offs between confidentiality, integrity, and availability. Our approach clarifies the nature of the trade-offs by making a clear distinction between declarative and operational concepts in security. We integrate this approach with a semantically justified mathematical systems modelling technology, thus providing a basis for a systematic methodology to support operational decision-making in information security investments and trade-offs.
Information Stewardship in Cloud Computing. Joint work with Martin Sadler. International Journal of Service Science, Management, Engineering, and Technology 1(1), 50-67, 2010. Free sample copy, including this article.
Semantics for Structured Systems Modelling and Simulation. Joint work with Matthew Collinson and Brian Monahan. Proc. Simutools 2010, ACM Digital Library and EU Digital Library. ISBN: 978-963-9799-87-5. Preprint.
Abstract. Simulation modelling is an important tool for exploring and reasoning about the dynamics and properties of complex systems, and many supporting languages are available. Commonly occurring features of these languages are constructs that capture concepts such as process, resource, and location. We describe a mathematical framework that supports a modelling idiom based on these core concepts, and which also adopts stochastic methods for representing the environments within which systems exist. We explain how this framework can be used to give a formal semantics to a simulation modelling language, Core Gnosis, that includes basic constructs for process, resource, and location. We include a brief discussion of a system of logic for reasoning about our models that is compositional with respect to the structure of models. We believe that our mathematical analysis of systems in terms of process, resource, location, and stochastic environment, together with a language that captures these concepts quite directly, leads to an efficient and robust modelling framework within which natural mathematical reasoning about systems is captured in the associated tools.
Decision Support for Systems Security Investment. Joint work with Yolanta Beresnevichiene and Simon Shiu. Proc. Business-driven IT Management (BDIM) 2010. IEEE Xplore, 2010. Preprint
Abstract. Information security managers with fixed budgets must invest in security measures to mitigate increasingly severe threats whilst maintaining the alignment of their systems with their organization's business objectives. The state of the art lacks a systematic methodology to support security investment decision-making. We describe a methodology that integrates methods from multi-attribute utility evaluation and mathematical systems modelling. We illustrate our approach using a case study of a large organization divesting itself of its IT support services, delivering useful results to the organization's security managers. Specifically, by integrating a mathematical model of system behaviour with an account of the utility of available security investment strategies, the case study has enabled them to understand better the trade-offs between the security performance and the operational consequences of their choices.
Economics of Identity and Access Management: Providing Decision Support for Investments. Joint work with Marco Casassa Mont, Yolanta Beresnevichiene, and Simon Shiu. Proc. Business-driven IT Management (BDIM) 2010. IEEE Xplore, 2010. Preprint
Abstract. Identity and Access Management (IAM) is a key enabler of enterprise businesses: it supports automation, security enforcement and compliance. However, most enterprises struggle with their Identity and Access Management strategy. Discussions on IAM primarily focus at the IT operational level, rather than targeting strategic decision makers' issues, at the business level. Organisations are experiencing an increasing number of internal and external threats and risks: there is scarcity of resources and budget to address them all. Decision makers (e.g. CIOs, CISOs) need to prioritise their choices and motivate their requests for investments. This applies for investments in IAM vs. other possible security or business investments that could be made by the organisation. In this context, a range of possible IAM investment options has an effect on multiple strategic outcomes of interest, such as assurance, agility, security, compliance, productivity and empowerment. We have developed a repeatable approach and methodology to help organisations work through this complex problem space and determine an appropriate strategy, by providing them with decision support capabilities. The proposed approach, validated in collaboration with Security & IAM experts, couples economic modeling, enabling decision makers to explore their preferences between the different outcomes, with system modeling & simulations to predict the consequences (likely outcomes) associated with different investment choices and map them against decision makers' preferences to identify the most suitable options. We illustrate how this methodology has been applied in an IAM case study, in a business-driven context with core enterprise services. This work is in progress. We discuss current results and next steps.
Information Security Trade-offs and Optimal Patching Policies. Joint work with Christos Ioannidis and Julian Williams. European Journal of Operational Research, 216(2):434-444, 16 January 2012. doi:10.1016/j.ejor.2011.05.050. Preprint.
Abstract.We develop and simulate a model of the deployment of patches --- which incurs cost --- in the presence of trade-offs between confidentiality and availability. The patching of vulnerabilities is divided into regular and irregular events, for both networks and clients. The computation of the optimal patching policy requires knowledge of the joint processes of arrivals and intensities, system architecture, and the type of organization. We have found that different types of organizations, as characterized by the managers' preferences, exhibit distinct off-cycle patching profiles that are relatively cost-sensitive, and that the frequency of irregular patching depends crucially on the aspect of the system --- e.g., network or clients --- addressed.
Investments and Trade-offs in the Economics of Information Security. Joint work with Christos Ioannidis and Julian Williams. Proc. Financial Cryptography and Data Security 2009, LNCS 5628: 148-162, Springer, 2009. Preprint.
Abstract. We develop and simulate a dynamic model of investment in information security. The model is based on the recognition that both IT managers and users appreciate the trade-off between the fundamental characteristics of information security, namely confidentiality and availability. The model's parameters can be clustered in a manner that allows us to categorize and compare the responses to shocks of various types of organizations. We derive the system's stability conditions and find that they admit a wide choice of parameters. We examine the system's responses to the same shock in confidentiality under different parameter constellations that correspond to various types of organizations. Our analysis illustrates that the response to investments in information security will be uniform in neither size nor time evolution.
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. Journal of Logic and Computation19(b):1207-1244, 2009. Advance Access published on 22 July, 2009. doi:10.1093/logcom/exp021. Preprint. Also available as an HP Labs Technical Report: HPL-2008-74R1.
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. In Managing Information Risk and the Economics of Security. M. Eric Johnson (editor), Springer, 2009: 141-163. Preprint.
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, systems modelling, mathematical logic, and other topics. Some of these papers have been published elsewhere (conferences, journals, etc.).
An Update to Located Demos2k. Joint work with Matthew Collinson and Brian Monahan. Available as an HP Labs Technical Report: HPL-2008-205.
Abstract. We give here a short update concerning Located Demos2k briefly describing the ability to forget and recall resource links, as reported in an earlier Technical Report. We also briefly mention our (purely applicative) implementation in OCaml of a simulator for Located Demos2k. Two appendices contain a substantial example of Located Demos2k, presented in OCaml terms, and the execution trace produced by the implementation.
Located Demos2k: A Tool for Executing Processes Relative to Distributed Resources. Joint work with Matthew Collinson and Brian Monahan. 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. Formal Aspects of Computing22(2), 83-104, 2010. Erratum: Formal Aspects of Computing22(3-4), 483-484, 2010. Available as an HP Labs Technical Report (with erratum incorporated): HPL-2008-75R1. The original publication is available at http://www.springerlink.com.
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. Mathematical Structures in Computer Science 18(6), 1091-1132, 2008. doi: 10.1017/S0960129508007159. 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. Mathematical Structures in Computer Science 19:959-1027, 2009. doi:10.1017/S0960129509990077. Preprint.
Abstract. Mathematical 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.
Errata
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. The original publication is available at http://www.springerlink.com.
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.
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.
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''.