Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: bunched logic

Bottom of Page

1 to 15 of 15

  1.  
    • CommentRowNumber1.
    • CommentAuthorspitters
    • CommentTimeJul 7th 2018

    Connect to monoidal topos

    diff, v5, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeOct 4th 2022

    added pointer to:

    diff, v7, current

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMar 24th 2023

    added publication data to this item:

    diff, v10, current

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeMar 24th 2023

    added publication data to this item:

    diff, v10, current

    • CommentRowNumber5.
    • CommentAuthorGuest
    • CommentTimeMar 24th 2023

    the Mitchell Riley doi link doesn’t seem to work.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMar 24th 2023

    It used to work!

    But I also happened to notice a few hours back that it fails to work for the moment(?) which is why I had added an alternative pdf link (rev 9).

    I think this must be a mistake and suspect it will be rectified. But I don’t know.

    • CommentRowNumber7.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 25th 2023

    Yes. This permalink still works https://digitalcollections.wesleyan.edu/object/ir%3A3269 in the meantime.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2023

    added pointer to:

    diff, v11, current

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2023

    Fixed the hyperlink for this item

    • Bodil Biering, On the logic of bunched implications – and its relation to separation logic, MSc thesis Copenhagen (2004) [pdf]

    and moved it out of the list of original articles

    diff, v12, current

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMar 28th 2023

    re #5:

    I have contacted the “WesScholar” team, and they promptly replied:

    This is a temporary issue with the DOI as we just completed a migration of the digital collections in WesScholar. It will be resolved when the post-migration clean-up is complete.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeMar 29th 2023
    • (edited Mar 29th 2023)

    I have slightly re-worked and then considerably expanded the Idea section (here).

    In particular I have added the following discussion:

    But aspects of the proposal of O’Hearn & Pym (1999) and Pym (2002) have remained unsatisfactory, see Pym (2008), Errata to Pym (2002) and Riley(2022), pp. 19 and Rem. 1.4.1 (p. 64):

    Riley 2022, pp. 19: [Since] context manipulations are not recorded in the terms, typechecking a term can be difficult. First, it is not always obvious when and how the contraction rule has to be applied, and secondly, it is not always obvious how the context has to be split into two pieces to apply ⊸\multimap-ELIM. Besides the challenge of typechecking, the combination of the weakening rule and the rules for the monoidal unit also breaks soundness for the intended semantics.

    The various extensions of the αλ-calculus that have since appeared [BO06; CPR08; SS04; Atk04] do not resolve these issues. It is also not so clear how to add dependent types to this system and how dependency should behave between bunches.

    In reaction to this, Riley (2022) proposes an enhanced form of bunched type theory which is claimed to fix all these problems at least in the case that the second structural connective ⊗\otimes is a multiplicative conjunction in a linear type theory, hence for a form of dependent linear type theory. The key new ingredients in Riley (2022) to make this work are (1.) a classical modality ♮\natural which from any “parameterized linear type” projects out the underlying classical type and (2.) a decoration of bunched contexts by “color palettes” which keep explicit track of the bunching/tree structure. (On the other hand, especially the second point leads to a proliferation of inference rules, but maybe that’s what it takes.)

    diff, v15, current

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeMar 30th 2023

    Once more back to #5: The “WesScholar” team informs me that the link doi:10.14418/wes01.3.139 has been repaired.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeApr 9th 2023

    added (here) another quote from Riley (2022)

    diff, v19, current

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJun 1st 2023

    added pointer to:

    diff, v20, current

  15. Removed semicolon typo in the interpretation of the first sequent on the page (Idea section).

    Baptiste Loreau

    diff, v22, current

1 to 15 of 15

  1.