Today's standard model for database concurrency control, called serializability theory, represents executions of transactions as partial orders of operations. The theory tells when an execution is serializable, that is, when the set of operations of a transaction execute atomically with respect to those of other transactions. It has been used successfully to prove correctness of most database concurrency control algorithms. Its most serious limitation is its inability to represent nested computations conveniently.This paper presents a more general model that permits nested transactions. In this model, transactions may execute subtransactions, giving rise to tree-structured computations. A serializability theory is developed for this model, which can be used to prove the correctness of concurrency control algorithms for nested transactions and for multilevel database systems.The theory is based on an abstract model of computation that allows arbitrary operations, and parallel and even nondeterministic programs. Axioms are presented that express the basic properties that programs that manage or access data need to satisfy. We use these axioms to derive proof techniques. One new technique—substitution—shows the equivalence of two executions by substituting one subcomputation by another, usually shallower (i.e., less nested), one. Our proof techniques are illustrated by applying them to several well-known concurrency control problems.