I have added a fair bit of detail to the section “Quantum Programming Language” (here):

First a fairly comprehensive declaration of the (pseudo-)code sugaring of modal dependent linear TT that makes it a quantum programming language,

then followed by more examples (more basic examples and then the quantum bit flip code in addition the the teleportation protocol).

]]>starting a section (here) which develops the actual programming (pseudo-)code for quantum circuits which is obtained by using the various monadic effects constructed in dLTT as discussed in the previous sections.

]]>Oh, I see. Yes.

]]>Sounds interesting.

We have been talking about it, meanwhile it’s recorded as this Prop. at *quantum reader monad*.

Sounds interesting. Always good to see how something important may be recovered naturally.

]]>I don’t expect that I’ll be digging into the claimed relation to natural language formalization anytime soon.

On the dependent typing: The Oxford community has come ever so close to incorporating this, but maybe falling short (as far as I oversee the literature): Namely the category of (co)algebras over their “classical structures” Frobenius monad is that of dependent linear types, and the corresponding monadic functor is the dependent product-functor. That’s the way to recover dependent linear types if one didn’t start with them. Lem 5.61 in Heunen&Vicary’s book is beginning to see this, minus any monadic language.

]]>Given the subsumption of traditional quantum information formalisms within dLHoTT, I wonder if there’s something to be done regarding categorical compositional distributional semantics. Seemed odd to me not to embrace that part of natural language which is evidently dependently typed.

]]>Oh, now I see which typo you meant. Luckily the organizers mixed up the time zone. Am fixing it now…

]]>Thanks, I think I had spotted these and fixed. Hopefully. Latest version here. Going live now. Will fully polish up the overlay on the last slides later.

]]>On 77/112 you have product as left adjoint to context extension as left adjoint to coproduct. Surely the other way.

]]>Thanks. Will fix this in a moment…

]]>Full-blow -> full-blown

]]>I have been preparing slides for a brief presentation of these ideas, tomorrow at QTML22.

An early and incomplete version of the slides is now here.

All comments are welcome. Hope to finalize these slides tomorrow morning.

]]>added also the Kleisli map which is the “Bell state measurement”.

]]>Am starting a write-up (here) of how (programming languages for) quantum circuits “with classical control and/by measurement” have a rather natural and elegant formulation within the linear homotopy type theory of Riley 2022.

Aspects of this have a resemblance to some constructions considered in/with “Quipper”, but maybe it helps clarify some issues there, such as that of “dynamic lifting”.

The entry is currently written without TOC and without Idea-section etc, but rather as a single top-level section that could be `!include`

-ed into relevant entries (such as at *quantum circuit* and at *dependent linear type theory*). But for the moment I haven’t included it anywhere yet, and maybe I’ll eventually change my mind about it.