The </strong>K</strong> Combinator as a Semantically Transparent
Tagging Mechanism
The K Combinator as a Semantically Transparent Tagging Mechanism
The K combinator provides a semantically transparent
tagging mechanism which is useful in various aspects of mechanizing
higher order logic. Our examples include numerals, normalization
procedures, named hypotheses in goal-directed proof, and rewriting
directives.
gzipped Postscript
PDF