Quantum lambda calculus, symmetric monoidal closed categories, and TQFTs

The last post was all about stuff that’s already known. I’ll be working in my thesis on describing the syntax of what I’ll call simply-typed quantum lambda calculus. Symmetric monoidal closed categories (SMCCs) are a generalization of CCCs; they have tensor products instead of products. One of the immediate effects is the [...]

CCCs and lambda calculus

I finally got it through my thick skull what the connection is between lambda theories and cartesian closed categories.
The lambda theory of a set has a single type, with no extra terms or axioms. This gives rise to a CCC where the objects are generated by products and exponentials of a distinguished object, the [...]