Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added pointer to:
added publication data to this item:
added publication data to this item:
the Mitchell Riley doi link doesn’t seem to work.
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.
Yes. This permalink still works https://digitalcollections.wesleyan.edu/object/ir%3A3269 in the meantime.
added pointer to:
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.
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.)
Once more back to #5: The “WesScholar” team informs me that the link doi:10.14418/wes01.3.139 has been repaired.
1 to 13 of 13