  We generalise Levy's call-by-push-value (CBPV) to dependent type theory, to
gain a better understanding of how to combine dependent types with effects. We
define a dependently typed extension of CBPV, dCBPV-, and show that it has a
very natural small-step operational semantics, which satisfies subject
reduction and (depending on the effects present) determinism and strong
normalization, and an elegant categorical semantics, which - surprisingly - is
no more complicated than the simply typed semantics.
  We have full and faithful translations from a dependently typed version of
Moggi's monadic metalanguage and of a call-by-name (CBN) dependent type theory
into dCBPV- which give rise to the expected operational behaviour. However, it
turns out that dCBPV- does not suffice to encode call-by-value (CBV) dependent
type theory or the strong (dependent) elimination rules for positive
connectives in CBN-dependent type theory.
  To mend this problem, we discuss a second, more expressive system dCBPV+,
which additionally has a principle of Kleisli extension for dependent
functions. We obtain the desired CBV- and CBN-translations of dependent type
theory into dCBPV+. It too has a natural categorical semantics and operational
semantics. However, depending on the effects we consider, we may lose
uniqueness of typing, as the type of a computation may become more specified as
certain effects are executed. This idea can be neatly formalized using a notion
of subtyping.
  We hope that the theoretical framework of this paper on the one hand provides
at least a partial answer to the fundamental type theoretic question of how one
can understand the relationship between computational effects and dependent
types. On the other hand, we hope it can contribute a small-step towards the
ultimate goal of an elegant fully fledged language for certified effectful
programming.
