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

Discussion Tag Cloud

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: !-modality

Bottom of Page

1 to 27 of 27

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeFeb 4th 2014
    • (edited Feb 4th 2014)

    collected some references on the interpretation of the !-modality as the Fock space construction at !-modality.

    Cross-linked briefly with he stub entries_Fock space_ and second quantization.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeNov 10th 2017

    I de-stubbified !-modality with some discussion of the various ways to interpret it categorically.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeDec 22nd 2017

    I added to !-modality some comments about term calculi.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeApr 17th 2018

    Added Hyland-Schalk reference

    diff, v18, current

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 7th 2019

    It seems that !-modality doesn’t render as a link on some pages, e.g., at Fock space. Is there a problem starting with ’!’ ?

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJul 7th 2019

    Thanks for the alert. I am fixing it in the entries. “exponential modality” is a better link word, anyway.

    But of course there remains a bug which would be good to fix in any case. So I have moved the non-rendering “!-modality”-link to the Sandbox.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 7th 2019

    OK, have changed a number of links.

    • CommentRowNumber8.
    • CommentAuthorRichard Williamson
    • CommentTimeJul 7th 2019
    • (edited Jul 7th 2019)

    I’m currently on holiday, and unfortunately will not be able to look at the bug for at least a week. Would it be possible to create a single thread ’Bugs and feature requests’ where all bugs and feature requests are registered (and maybe a note could be added to the HowTo to this effect)? It is then much less likely that I will forget about or overlook something. To keep it easy to get an overview, maybe discussion can be avoided in that thread, and instead when registering the bug one can link to a thread where one can discuss it?

  9. Other Kleisli article

    Ammar Husain

    diff, v20, current

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 12th 2019

    Added an example: the Chu construction of any cartesian monoidal category has an idempotent !-modality, namely the coreflection into the original category.

    diff, v22, current

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeNov 13th 2019

    I have a vague memory of reading a paper that decomposed the !-modality into two separate modalities, one that allows only contraction and another that allows only weakening. Does anyone know a reference doing something like that?

    • CommentRowNumber12.
    • CommentAuthormaxsnew
    • CommentTimeNov 13th 2019
    • (edited Nov 13th 2019)

    This paper does something like that, though for the closely related “tensor logic” rather than linear I think.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeNov 13th 2019

    Thanks. I don’t think that’s the paper I was half-remembering, but it’s useful to have.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeNov 13th 2019

    Added the missing nullary condition for a Seely !-modality.

    diff, v24, current

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeNov 13th 2019

    Generalized the example to lift any linear-nonlinear adjunction to a Chu construction.

    diff, v25, current

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeNov 20th 2019

    Added some citations for construction of cofree !-modalities

    diff, v26, current

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeNov 21st 2019

    Clarified relationship between the various definitions.

    diff, v27, current

  18. adding category:logic

    Valeria de Paiva

    diff, v28, current

    • CommentRowNumber19.
    • CommentAuthorvaleriadepaiva
    • CommentTimeNov 7th 2020
    @Mike I think the paper you wanted to remember is Jacobs' https://www.sciencedirect.com/science/article/pii/0168007294900205
    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    Added these pointers:

    A quantum programming language based on this linear/non-linear type theory adunction is QWIRE:

    • Jennifer Paykin, Robert Rand, Steve Zdancewic, QWIRE: a core language for quantum circuits, POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesJanuary 2017 Pages 846–858 (doi:10.1145/3009837.3009894)

    applied to verified programming after implementation in Coq:

    • Robert Rand, Jennifer Paykin, Steve Zdancewic, QWIRE Practice: Formal Verification of Quantum Circuits in Coq, EPTCS 266, 2018, pp. 119-132 (arXiv:1803.00699)

    and using ambient homotopy type theory:

    • Jennifer Paykin, Steve Zdancewic, A HoTT Quantum Equational Theory (arXiv:1904.04371)

    diff, v29, current

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    also pointer to:

    diff, v30, current

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeNov 8th 2022
    • (edited Nov 8th 2022)

    added cross-links by !include-ing the logic symbols – table

    added pointer to:

    • Daniel Mihályi, Valerie Novitzká, Section 2.2 of: What about Linear Logic in Computer Science?, Acta Polytechnica Hungarica 10 4 (2013) 147-160 [pdf]

    diff, v33, current

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2022
    • (edited Nov 10th 2022)

    I have fixed and completed this bibitem:

    • Nick Benton, A mixed linear and non-linear logic: Proofs, terms and models, in Computer Science Logic. CSL 1994, Lecture Notes in Computer Science 933 [doi:10.1007/BFb0022251, pdf]

    here and in a couple of other entries.

    (It also appears at linear-non-linear logic and still needs to be reformatted there, but that entry is suffering from some bug which prevents it from being edited. I have contacted the technical team about it.)

    diff, v34, current

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2022

    also polished up this bibitem:

    diff, v34, current

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2022

    I have recovered this reference here via the WaybackMachine:

    Unfortunately, the pdf is just a tad larger than the upload limit for the nLab server. I have tried to compress it a little, but couldn’t quite bring it below the threshold.

    So for the time being the pdf is sitting in my Dropbox.

    diff, v34, current

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeNov 11th 2022

    added a section (here) on the realization of the exponential modality in linear homotopy type theory.

    diff, v35, current

    • CommentRowNumber27.
    • CommentAuthorJ-B Vienney
    • CommentTimeNov 11th 2022

    Added dereliction rule

    diff, v36, current

1 to 27 of 27

  1.