[TYPES] terminology for different kinds of proof terms?

[Carl Eastlund]

On Tue, 25 Jan 2005 20:18:20 -0800 (PST), Joe Wells <jbw at macs.hw.ac.uk> wrote:
> [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
> 
> 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 can't help you on the terminology front, but I have a question about
your description of proof terms.  As I understood it, the purpose of
proof terms was in fact to capture the entire structure of the
derivation, and that none was lost.  Are some proof terms used
otherwise?  Can someone shed some light on this?

--Carl