[TYPES] terminology for different kinds of proof terms?

[Joe Wells]

I am seeking pointers to definitions of terminology for different
kinds of proof terms.

At the most basic level, I understand the phrase "proof term" to refer
to syntactic objects that are added to the judgements in derivations
of a rule system for some logic.  Often, these are λ-terms or
variations on λ-terms.  Generally, a proof term captures some of the
structure of the derivation, although sometimes quite a bit of the
structure is lost.  I am aware of a terminological distinction between
"Curry style" where pure λ-terms are used and "Church style" where
type are inserted in the λ-terms.  Are there any other interesting
terminological distinctions?

I think I need to define some new terminology, but I would prefer to
reuse existing terminology if possible and if not at least avoid
conflicts.

Thanks for any pointers!

-- 
Joe Wells