Lambda Prolog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a polymorphic higher-order logic using the ML-style polymorphism of Lambda Prolog. The terms of the metalanguage (Lambda Prolog) can be used to express the statement of a lemma, and metalanguage type-checking can directly type-check the lemma. But to allow polymorphic lemmas requires either more general polymorphism at the meta-level or a less concise encoding of the object logic. We discuss both the Terzo and Teyjus implementations of Lambda Prolog as well as related systems such as Elf.

A shorter version of this paper is to appear in 16th International Conference on Logic Programming, November 1999.