A formulation of the logic underlying quantum theory (and quantum systems), posed by Isham et al., that supersedes the older (non-distributive) quantum logic formulation associated with von Neumann, came about early this century and late last century. It is a logic on a bi-Heyting lattice, which means you have all the structure of (distributive) intuitionist logic, but also all the dual connectives.
It's actually easy to fully characterize [bi-/dual-]Heyting lattices and Boolean lattices and the logics based on them. Let $A ⊢ B$ (or equivalently $B ⊣ A$) denote the "inference" relation (that statement $A$ infers statement $B$, i.e. that $B$ can be inferred from $A$). It's a pre-order relation by virtue of the properties
$$A ⊢ A,\quad \left(\begin{aligned}A ⊢ B\\B ⊢ C\end{aligned}\right) ⇒ A ⊢ C.$$
The corresponding equivalence relation
$$A ⊣⊢ B ⇔ \left(\begin{aligned}A ⊢ B\\A ⊣ B\end{aligned}\right),$$
then gives you equivalence classes $[A] = \{ B: A ⊣⊢ B \}$ that are, then, partially ordered by $[A] ≤ [B]$ if and only if $A ⊢ B$, and the ordering forms a bi-Heyting lattice.
Associated with it are connectives that may be succinctly (and precisely) characterized by the following properties
$$\begin{array}{lcl}
C ⊢& A ∧ B &⇔ \left(\begin{aligned}C ⊢ A\\C ⊢ B\end{aligned}\right),\\
C ⊢& ⊤ &⇔\text{ always},\\
C ⊢& A ⊃ B &⇔ C ∧ A ⊢ B,\\
C ⊢& ¬A &⇔ C ∧ A ⊢ ⊥,
\end{array}$$
and
$$\begin{array}{cll}
A ∨ B &⊢ D &⇔ \left(\begin{aligned}A ⊢ D\\B ⊢ D\end{aligned}\right),\\
⊥ &⊢ D &⇔\text{ always},\\
A ⊂ B &⊢ D &⇔ A ⊢ B ∨ D,\\
⨽B &⊢ D &⇔ ⊤ ⊢ B ∧ D.
\end{array}$$
The connective $A ⊃ B$, also written as $A → B$, is the conditional "if $A$ then $B$" connective, while the dual $A ⊂ B$, which could also be written as $A - B$, is the actual Boolean connective (meant in the sense that Boole, himself, used it in his "Laws of Thought" book) "$A$ unless $B$" or "$A$ except $B$". I've also seen it written as $A ← B$. The stronger "is false" negation, associated with Heyting lattices, is $¬A ⊣⊢ A ⊃ ⊥$, while the weaker "isn't true" negation that Boole used $⨽B ⊣⊢ ⊤ ⊂ B$ is a kind of dual. I've also seen it written as $\sim B$. The inference $¬C ⊢ ⨽C$ is valid, while the converse $¬C ⊣ ⨽C$ is valid, as a rule, if and only if the logic is ... Boolean.
There is a presentation-mode PDF on this newer Isham-based quantum logic framework Contexts, Bi-Heyting Algebras and a New Logic for Quantum Systems and ArXiv pre-print Topos-Based Logic for Quantum Systems and Bi-Heyting Algebras, both by Döring, that discuss this in depth.
The logics are, as lattices, complete, which means that they have arbitrary least upper bounds (join) $∨$ and greatest lower bounds (meet) $∧$ on an arbitrary number of arguments of arbitrary cardinality, not just a finite number of arguments; and they are both distributive, including infinitely distributive. It's for that reason that you have the full set of connectives and their duals.
Everything is defined in the setting of topos theory, which (as per my best understanding) have some kind of "internal language" associated with them similar to that of a Curry-Howard representation for intuitionistic logics. I'm not entirely sure about that, since I haven't (yet) studied topos theory in any great depth. I see no references anywhere on doing Curry-Howard for bi-Heyting logics, but I do see this PDF Topos Internal Language, which might be useful for connecting the dots.
