Normal forms for intuitionistic formulas?
There are two main ways you could take this.

If you are interested in provability, then what you want is the Gödel-Tarski embedding of intuitionistic logic into classical S4 modal logic.  The  idea is that you can interpret the box modality of modal logic as a &quot;provability&quot; modality, and then stick a box in front of each connective. Then you can put the formula into whatever variant of modal CNF you need.
See Mints' paper The Gödel-Tarski Translations of Intuitionistic Propositional Formulas.

If you are interested in retaining the ability to translate intuitionistic proofs, then one popular idea is to use Tarski's &quot;high school identities&quot; to put intuitionistic formulas into a normal form related to the exponential polynomials. This gives a normal form for types, whose translation preserves the beta-eta equivalence of proofs of that type.
See Danko Ilik's The exp-log normal form of types.


Both of these papers are about the propositional case. I don't know what happens with first-order quantifiers.