[TYPES] terminology for different kinds of proof terms?
jbw at macs.hw.ac.uk
Tue Jan 25 08:55:43 EST 2005
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
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
Thanks for any pointers!
More information about the Types-list