On bunched typing
The work reported in this paper arose from an attempt by the author to reconcile two substructural type systems, where the contraction rule is restricted: Reynold's Syntactic Control of Inference (SCI) and Girard's Linear Logic (LL). In SCI, contraction is understood as allowing shared access to storage, whereas in LL contraction is understood as duplicating a piece of data, rather than sharing. So limiting contraction in the first system gives control over sharing, whereas limiting contraction in the second one gives control over the number of uses of a datum. The natural question arises whether the conceptual discrepancy between LL and SCI has type-theoretic significance. A hint of a possible way forward was contained in the curious property of some SCI models of having two kinds of closed structures that coexist in the same category. In this paper the author studies a typed \(\lambda\)-calculus (called the \(\alpha\lambda\)-calculus after its binders) corresponding to a category that admits two closed structures. A typing context \(\Gamma\) in a type judgement \(\Gamma \vdash M : B\) is usually represented as a set or a sequence of associations \(x:A\) pairing identifiers with types. In {bunched typing} the contexts are trees built from two combining operations `,' and `;' which allows one to form nested contexts \(\Gamma, \Delta\) and \(\Gamma;\Delta\). In the \(\alpha\lambda\)-calculus we have two arrow introduction rules corresponding to an additive arrow \(A\to B\) and to a multiplicative arrow \(A\to\!*\;B\). The introduction rule for the additive arrow admits in the premise the context \(\Gamma; x:A\), whereas the introduction rule for the multiplicative arrow admits the context \(\Gamma, x:A\). The structural rules of weakening and contraction are allowed for `;', but not for `,'. The author shows that the \(\alpha\lambda\)-calculus is incompatible with an interpretation where a multiplicative function uses its argument once, but perfectly compatible with a reading based on sharing of resources. Many variants of the original basic system are also provided and analysed. Basic properties of the \(\alpha\lambda\)-calculus, such as substitution and reduction, are studied and categorical semantics are provided.
- Effect algebras, presheaves, non-locality and contextuality
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- On the semantics of parsing actions
- Bunched sequential information
- A simple nominal type theory
- Two cotensors in one: presentations of algebraic theories for local state and fresh names
- Strong update, disposal, and encapsulation in bunched typing
- Bunching for regions and locations
- A logic of separating modalities
- A calculus for hardware description
- Bunched polymorphism
- Temporal BI: proof system, semantics and translations
- Resource interpretations, bunched implications and the -calculus. (Preliminary version)
- scientific article; zbMATH DE number 814797 (Why is no real title available?)
- Kripke resource models of a dependently-typed bunched -calculus. (Extended abstract)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Classical control, quantum circuits and linear logic in enriched category theory
- Abstract syntax: substitution and binders
- Bunched Fuzz: sensitivity for vector metrics
- Towards logical foundations for probabilistic computation
- The quantum monadology
- Entanglement of sections: the pushout of entangled and parameterized quantum information
This page was built for publication: On bunched typing
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4461769)
