  In the theory of programming languages, type inference is the process of
inferring the type of an expression automatically, often making use of
information from the context in which the expression appears. Such mechanisms
turn out to be extremely useful in the practice of interactive theorem proving,
whereby users interact with a computational proof assistant to construct formal
axiomatic derivations of mathematical theorems. This article explains some of
the mechanisms for type inference used by the Mathematical Components project,
which is working towards a verification of the Feit-Thompson theorem.
