  The Abella interactive theorem prover has proven to be an effective vehicle
for reasoning about relational specifications. However, the system has a
limitation that arises from the fact that it is based on a simply typed logic:
formalizations that are identical except in the respect that they apply to
different types have to be repeated at each type. We develop an approach that
overcomes this limitation while preserving the logical underpinnings of the
system. In this approach object constructors, formulas and other relevant
logical notions are allowed to be parameterized by types, with the
interpretation that they stand for the (infinite) collection of corresponding
constructs that are obtained by instantiating the type parameters. The proof
structures that we consider for formulas that are schematized in this fashion
are limited to ones whose type instances are valid proofs in the simply typed
logic. We develop schematic proof rules that ensure this property, a task that
is complicated by the fact that type information influences the notion of
unification that plays a key role in the logic. Our ideas, which have been
implemented in an updated version of the system, accommodate schematic
polymorphism both in the core logic of Abella and in the executable
specification logic that it embeds.
