How should I think about proof nets? In his answer to this question, Stephane Gimenez pointed me to a polynomial-time normalization algorithm for proofs in linear logic. The proof in Girard's paper uses proof nets, which are an aspect of linear logic I don't actually know very much about. 

Now, I've tried to read papers on proof nets before (such as Pierre-Louis Curien's notes on them), but I have not really understood them.  So my question is: how should I think about them? By "how to think about them", I mean both the informal intuition behind them (e.g., how they behave computationally, or how they are related to  sequents), and also which theorems about them I should prove for myself to really get them. 

In answering this question, you can assume (1) I know the proof theory of linear logic well (including things like how the cut-elimination proof goes, and in focalized form too), (2) their categorical semantics in terms of coherence spaces or via Day convolution, and (3) the very basic rudiments of the GoI construction.
Proof nets are interesting essentially for three reasons:

1) IDENTITY OF PROOFS. They provide an answer to the problem "when are two proofs the same"? In sequent calculus you may have many different proofs of the same proposition which differ only because sequent calculus forces an order among deduction rules even when this is not necessary. Of course, one can add an equivalence relation on sequent calculus proofs, but then one has to show that cut-elimination behaves properly on equivalence classes, and also it is necessary to turn to rewriting modulo, which is quite more technical than plain rewriting. Proof nets solve the problem of dealing with equivalence classes by providing a syntax where every equivalence class is collapsed on a single object. This situation is anyway a bit idealistic, as for many reasons proof nets are often extended with some form of equivalence.

2) NO COMMUTATIVE CUT-ELIMINATION STEPS. Cut-elimination on proof nets takes a quite different flavor than on sequent calculi because commutative cut-elimination steps disappear. The reason is that in proof nets the deduction rules are connected only by their causal relation. Commutative cases are generated by the fact that one rule can be hidden by another causally unrelated rule. This cannot happen in proof nets, where causally unrelated rules are far apart. Since most cases of cut-elimination are commutative one gets a striking simplification of cut-elimination. This has been particularly useful for studying lambda calculi with explicit substitutions (because exponentials = explicit substitutions). Again, this situation is idealized since some presentations of proof nets require commutative steps. However, their number is much smaller than in sequent calculus

3) CORRECTNESS CRITERIA. Proof nets can be defined by translation of sequent calculus proofs, but usually a system of proof nets is not accepted as such unless it is provided with a correctness criterion, i.e. a set of graph-theoretical principles characterizing the set of graphs obtained by translating a sequent calculus proof. The reason for requiring a correctness criterion is that the free graphical language generated by the set of proof net constructors (called links) contains "too many graphs", in the sense that some graphs do not correspond to any proof. The relevance of the correctness criteria approach is usually completely misunderstood. It is important because it gives non-inductive definitions of what is a proof, providing shockingly different perspectives on the nature of deductions. The fact that the characterization is non-inductive is usually criticized, while it is exactly what is interesting. Of course, it is not easily amenable to formalization, but, again, this is its strength: proof nets provide insights that are not available through the usual inductive perspective on proofs and terms. A fundamental theorem for proof nets is the sequentialization theorem, which says that any graph satisfying the correctness criterion can be inductively decomposed as a sequent calculus proof (translating back to the correct graph).

Let me conclude that it is not precise to say that proof nets are a classical and linear version of natural deduction. The point is that they solve (or attempt to solve) the problem of the identity of proofs and that natural deduction succesfully solve the same problem for minimal intuitionistic logic. But proof nets can be done also for intuitionistic systems and for non-linear systems. Actually, they work better for intuitionistic systems than for classical systems.