Not signed in (Sign In)

Start a new discussion

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).
    • 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?

  1. 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

  2. adding category:logic

    Valeria de Paiva

    diff, v28, current

    • CommentRowNumber19.
    • CommentAuthorvaleriadepaiva
    • CommentTimeNov 6th 2020
    @Mike I think the paper you wanted to remember is Jacobs'
    • 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

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)