  This work proposes a dependent type theory that combines functions and
session-typed processes (with value dependencies) through a contextual monad,
internalising typed processes in a dependently-typed lambda-calculus. The
proposed framework, by allowing session processes to depend on functions and
vice-versa, enables us to specify and statically verify protocols where the
choice of the next communication action can depend on specific values of
received data. Moreover, the type theoretic nature of the framework endows us
with the ability to internally describe and prove predicates on process
behaviours. Our main results are type soundness of the framework, and a
faithful embedding of the functional layer of the calculus within the
session-typed layer, showcasing the expressiveness of dependent session types.
