It is a commonplace that even such seemingly simple structures as sequent calculus proofs in classical propositional logic present semantic dilemmas. One often says that there is no genuinely symmetric Curry-Howard Isomorphism for classical proof. I shall start by outlining a proof-net based view as to the shape of a semantics for classical proof. It seems there is more room for manoeuvre than in the case of constructive proof so I shall try to say something about possible variants on the notion.
I shall then talk about abstract interpretations. Those with which I shall be concerned are like the relational model for linear logic. In particular they collapse the binary connectives. One way to see such interpretations is as a mathematically civilized way of describing combinatorial structure on proofs of the kind considered at various stages by such researchers as Statman, Buss, Carbone. The analysis is less sensitive than that suggested by experience with Linear Logic, but still provides much information. I shall consider two leading examples one based on the notion of Frobenius object and one based on traced categories with biproduct.