BDD trees provide a hierarchically structured canonical representation for boolean functions, based on ordered binary decision diagrams (OBDD's). We describe algorithms for function application and boolean quantification on BDD trees, allowing them to be used in applications such as symbolic model checking. Experimentally, we find that BDD trees can be greatly more efficient than ordinary OBDD's in verifying tree structured systems using symbolic model checking. In one case, sublinear growth is observed in the size of the transition relation representation. Analytically, we find that for a class of circuits of fixed tree width, BDD trees are asymptotically efficient.