There exists a translation, T, applicable to both propositions and proofs with the property that:
If $P$ is a classical proof of $\phi$ then $P^T$ is an intuitionistic proof of $\phi^T$.
(Trivially, any intuitionistic proof is also a perfectly good classical one.)
The details of some versions of the translation of the proof can be found in computer science texts under the name "CPS translation", though with different notation. Surprisingly this translation has an alter-ego as one of the stages when compiling certain programming languages.
Update: Adding (1) more detail and (2) something on the CPS translation.
(1) These translations don't allow you to completely remove double-negation elimination from classical proofs. But they do allow you to pull all of the double negation eliminations all the way out of the body of the proof to the very last line. So starting with a classical proof of $\phi$ we can translate it into an intuitionistic proof of $\neg\neg\phi$ and then we can tack one double negation elimination step onto the end to turn this back into a classical proof of $\phi$.
(2) According to the Curry-Howard isomorphism, a proof $P$ of a theorem $\phi$ can be interpreted as a program $P$ that produces a result of type $\phi$. When we convert a program to "continuation passing style", instead of just accepting a result of type $\phi$ back from our program, we instead write a program that accepts an extra argument (known as a continuation) that tells the program what it should do with its result. Ie. instead of writing a program of type $\phi$ we write a program of type $(\phi\rightarrow k)\rightarrow k$. The continuation is the extra argument of type $\phi\rightarrow k$ and we now get a final result of type $k$. The CPS translation takes an already existing program of type $\phi$ and converts it to one of type $(\phi\rightarrow k)\rightarrow k$. It's a bit fiddly but you can get a translation by following your nose, so to speak. Every function that your program calls also has to be modified so that it too uses the continuation and you thread the continuation all the way through the code.
But by the Curry-Howard isomorphism, this means you're translating a proof of the proposition $\phi$ into a proof of $(\phi\rightarrow k)\rightarrow k$. This is basically a version of the Godel-Gentzen translation as described in Constructivism in Mathematics: an Introduction Studies in Logic and the Foundations of Mathematics (by A. S. Troelstra and D. van Dalen.) A nice result of this is that you can now interpret classical proofs as computer programs.
I think it is a pretty amazing fact that you can take some esoteric mathematics comparing two systems of logic and turn it directly into code that can be used in a compiler.