What is the analog of a topos in quantum logic? If I'm studying classical mechanics, we might start by viewing propositions as true/false valued questions on points of phase space. 
Then, if I'm interested in a proposition-oriented view of things, I might flip things around and ask what points of phase space correspond to propositions, and observe a Boolean algebra of subsets of phase space. Then I might think about things that aren't propositions (like "x-coordinate of the 7th particle") which are clearly functions on phase space and I start turning the mathematical crank, and eventually decide that I ought to interpret classical mechanics in terms of the topos of sheaves on phase space. (with the discrete topology -- or maybe I consider the usual topology with interesting consequences)
If I want to carry out this procedure quantum physics, I somewhat get the idea that I should associate propositions with projection operators in a C*-algebra -- but where to go from here is unclear. I've only managed to find material talking about the very special case where we consider working with orthogonal projections -- and nothing on what higher structure should be built on top of this.
Just because it sounds natural, I imagine the answer to my question ought to be something like "The category of Hilbert-space representations of the C*-algebra", but I'm having difficulty seeing how one would go about interpreting quantum mechanics in this category.
Can anyone elaborate on how the interpretation would go or point me at references or give the right answer to my question?
(I hope this is the right place -- I'm asking here since physics.stackexchange.com didn't appear to have people knowledgeable about category theory)
 A: Apart from the Döring-Isham approach, there is another approach also, based on $\dagger$-Frobenius monoids. I think that the paper to look at is
J. Vicary, Categorical formulation of finite−dimensional quantum algebras, Comm. Math. Phys. 304, 765-796, arXiv:0805.0432.
This approach recovers the toposes of Döring and Isham by Theorem 4.6 of that paper, and is more general, so it might be used to connect Döring-Isham toposes to other works on categorical foundations of quantum physics (Page 791) or to obtain categorical counterparts to these toposes for the classical theory (Page 793-794).
So it looks like there are a number of different competing approaches, and the jury is out on which if any of these is "best".
A: Take a look at A topos for algebraic quantum theory by Heunen, Landsman, and Spitters. John Baez gives a nice bit of introductory commentary on this paper in TWF Week 257 (starting about halfway through where he discusses the papers of Döring and Isham, which are also relevant).
A: While the other two answers referred to very interesting connections of topos theory and quantum physics I think the following is going more into the direction the OP was imagining: In non-commutative topology one considers quantales, which are, roughly, an axiomatization of what you get when you replace open sets with projection operators - in particular intersection of open sets becomes composition of operators and does no longer have to be commutative. Here a few approaches to this idea are listed. One short definition is: A quantale is a monoid object in the monoidal category of lattices.
One can define sheaves over quantales (e.g. as done by Miraglia and Solitro in this article, or by Mulvey and Nawaz in this nicely written paper) and the categories of such sheaves would be the analogon to the notion of Grothendieck topos (but: to my knowledge no Giraud type characterization of such categories is known, let alone an elementary one). One can interpret logic in such categories, as e.g. done by Coniglio here for the Miraglia/Solitro setting.
In some ways such categories of sheaves over quantales connect back to actual topos theory as for example seen in the last corollary of the above Mulvey/Nawaz paper and more impressively in this article by Pedro Resende.

Edit: After having looked into the article pointed out by Urs Schreiber I would like to add a comment on what the authors see as drawbacks of quantum logic. They write that, on the logical side, quantum logic is not distributive and thus "difficult to interpret as a logical structure", that no satisfactory implication operator has been found "so that there is no deductive system in quantum logic" and that no satisfactory first order quantum logic has been found. 
I cannot judge what would be satisfactory, but Coniglio's interpretation linked to above has an implication operator and first order quantifiers. In any case, deduction systems can be built without implication operators being present inside the language, one just has to devise rules which say when one can infer a formula from a set of hypotheses (this is done in many nonclassical logics). The non-distributivity presents undeniable and annoying technical difficulties, the difficulty to interpret a non-distributive system "as a logical structure" on the other hand may be a matter of reading it in an appropriate way, see the next point.
The authors also see a physical drawback: They see the law of excluded middle $x \vee x^\bot = 1$, valid in quantum logic, as not reflecting the probabilistic spirit of quantum physics, because there it is not the case that either a proposition $x$ or its complement $x^\bot$ are true - they both may have intermediate "degrees of truth". I think an answer to this is that the interpretation of $\vee$ should not be that one of its arguments is true, but rather that its arguments together span the space of all possibilities. Non-distributivity then makes some sense also.
In a similar vein many things in intuitionistic logic make more sense if one interprets it as talking not about the truth of assertions but about whether they are known or provable (and an observer-centered perspective on quantum physics seems very appropriate). So the choice of an underlying logic is the choice of a point of view. Maybe one can see the two topos approaches and the quantale approach as talking about quantum physics from different perspectives - one could even consider creating a bigger formal language containing the connectives from both interpretations and allowing to relate the several points of view (giving a formal semantics for this language might be quite a challenge, though).
Disclaimers: 1. My background in the things discussed above lies in categorical and non-classical logic - my knowledge of quantum physics is quite superficial. 2. Although I jumped to the defense of quantales here, I really like both topos approaches...
