A lambda encoding is some way of representing data as functions (lambda abstractions).  Some motivations for this for computer-checked proofs and type theory.