This paper presents a statical analysis approach to ensure the type safety of BDD client code and libraries and the correctness of BDDs high-level properties and semantics. The core of the approach is BDDL, a calculus that extends the lambda calculus with support for BDD operations. BDDL uses a type system based on refinement types to statically check BDD manipulation and can prevent incorrect operations on BDDs at compile-time.