The λΛ‐calculus is a dependent type theory with both linear and intuitionistic dependent function spaces. It can be seen to arise in two ways. Firstly, in logical frameworks, where it is the language of the RLF logical framework and can uniformly represent linear and other relevant logics. Secondly, it is a presentation of the proof‐objects of a structural variation, with Dereliction, of a fragment of BI, the logic of bunched implications. As such, it is also closely related to linear logic. BI is a logic which directly combines linear and intuitionistic implication and, in its predicate version, has both linear and intuitionistic quantifiers. The λΛ‐calculus is the dependent type theory which generalizes both implications and quantifiers. In this paper, we study the categorical semantics of the λΛ‐calculus, gives a theory of ‘Kripke resource models’, i.e. monoid‐indexed sets of functorial Kripke models, in which the monoid gives an account of resource consumption. A class of concrete, set‐theoretic models is given by the category of families of sets parametrized over a small monoidal category, in which the intuitionistic dependent function space is described in the established way, but the linear dependent function space is described using Day's tensor product.

Reynolds has developed a logic for reasoning about mutable data structures in which the pre- and postconditions are written in an intuitionistic logic enriched with a spatial form of conjunction. We investigate the approach from the point of view of the logic BI of bunched implications of O'Hearnand Pym. We begin by giving a model in which the law of the excluded middleholds, thus showing that the approach is compatible with classical logic. The relationship between the intuitionistic and classical versions of the system is established by a translation, analogous to a translation from intuitionistic logic into the modal logic S4. We also consider the question of completeness of the axioms. BI's spatial implication is used to express weakest preconditions for object-component assignments, and an axiom for allocating a cons cell is shown to be complete under an interpretation of triplesthat allows a command to be applied to states with dangling pointers. We make this latter a feature, by incorporating an operation, and axiom, for disposing of memory. Finally, we describe a local character enjoyed by specifications in the logic, and show how this enables a class of frame axioms, which say what parts of the heap don't change, to be inferred automatically.

Bornat has recently described an approach to reasoning about pointers, building on work of Morris. Here we describe a semantics that validates the approach, and use it to help devise axioms for operations that allocate and dispose of memory. 1. INTRODUCTION It is widely acknowledged that pointers cause problems for program-proving formalisms (e.g. [8, 17, 13, 16, 9, 1, 14, 7]), but there is less agreement on precisely what the problems are. So, before describing our own work, we rst discuss where we believe the diculties lie. The rst issue that must be faced is aliasing , where distinct expressions can denote the same l-value. The problem here can be seen by reference to Hoare logic, where assignment is treated using substitution on the object-language level: fP [E=x]g x := E fPg: For this treatment of assignment to be sound it is necessary that dierent identiers are not aliases. With pointers the problem is that aliasing is not an exceptional circumstance: for example, it wi...

We study a framework, RLF, for defining natural deduction presentations of linear and other relevant logics. RLF consists in a language together, in a manner similar to that of LF, with a representation mechanism. The language of RLF, the λλκ-calculus, is a system of first-order linear dependent function types which uses a function κ to describe the degree of sharing of variables between functions and their arguments. The representation mechanism is judgements-as-types, developed for linear and other relevant logics. The λλκ-calculus is a conservative extension of the λΠ-calculus and RLF is a conservative extension of LF.