When I do research, I come across a lot of terms I don't know. This folder serves as a place for me to store such terms. TODO: - [x] sequent calculus - [x] cut elimination - [x] Linear Logic's proof-nets - [ ] read this https://github.com/andreypopp/type-systems - [ ] compact closed category - [ ] polycategory - [ ] tensor fragment of quantum theory (referred to as multiplicative quantum mechanics) - [x] curry-howard iesomorphism, or propositions-as-types or, proofs-as-programs - [ ] lambda term beta reducing via cut elimination (brush up on lambda calculus perhaps) - [ ] lattice of closed subspaces of a hilbert space as the fundamental object of quantum mechanics (paper by birkhoff and von neuman). lattice is not distributive and the meet does not have a right adjoint, hence implication is problematic. what does any of this mean? - [x] gentzen-style logical calculus is not available, no conventional idea of deduction because of aforementioned thing - [ ] abramsky and coecke explicitly categorical account AC04 of strongly compact closed categories with biproducts. - [ ] tensor structure - [ ] kelly laplaza coherence theorem - [ ] arrows in a category - [ ] finite dimensional complex hilbert space H - [ ] equivalence classes of unit vectors in H - [ ] Algorithm W