  In various provers and deductive verification tools, logical transformations
are used extensively in order to reduce a proof task into a number of simpler
tasks. Logical transformations are often part of the trusted base of such
tools. In this paper, we develop a framework to improve confidence in their
results. We follow a modular and skeptical approach: transformations are
instrumented independently of each other and produce certificates that are
checked by a third-party tool. Logical transformations are considered in a
higher-order logic, with type polymorphism and built-in theories such as
equality and integer arithmetic. We develop a language of proof certificates
for them and use it to implement the full chain of certificate generation and
certificate verification.
