Intermediate languages are a paradigm to separate concerns in
software verification systems when bridging the gap between
programming languages and the logics understood by
theorem provers. While such intermediate languages traditionally
only offer rather simple type systems, this paper argues that it is both
advantageous and feasible to integrate richer type systems with
features like (higher-ranked) polymorphism and quantification over
types. As a concrete solution, the paper presents the type system of
Boogie 2, an intermediate verification language that is used in
several program verifiers.
The paper gives two encodings of types and formulae in
simply typed logic such that SMT solvers and other theorem
provers can be used to discharge verification
conditions.