  We present the design, implementation, and foundation of a verifier for
higher-order functional programs with generics and recursive data types. Our
system supports proving safety and termination using preconditions,
postconditions and assertions. It supports writing proof hints using assertions
and recursive calls. To formalize the soundness of the system we introduce
System FR, a calculus supporting System F polymorphism, dependent refinement
types, and recursive types (including recursion through contravariant positions
of function types). Through the use of sized types, System FR supports
reasoning about termination of lazy data structures such as streams. We
formalize a reducibility argument using the Coq proof assistant and prove the
soundness of a type-checker with respect to call-by-value semantics, ensuring
type safety and normalization for typeable programs. Our program verifier is
implemented as an alternative verification-condition generator for the
Stainless tool, which relies on existing SMT-based solver backend for
automation. We demonstrate the efficiency of our approach by verifying a
collection of higher-order functional programs comprising around 14000 lines of
polymorphic higher-order Scala code, including graph search algorithms, basic
number theory, monad laws, functional data structures, and assignments from
popular Functional Programming MOOCs.
