We define a type system for concurrent communication combining session types [HVK98] and correspondence assertions [CM98,GJ01]. The {\it dependent session types} calculus that we obtain is more expressive than the union of its subsystems. While session types allow us to describe the input/output synchronization between processes, and correspondence assertions allow us to ensure that certain code has been executed before other code, enforcing a communication protocol, dependent session types allow us not only to ensure that two processes communicated, but to guarantee the integrity of the information being exchanged. The resulting type system augments session types with effects and thus yields types which may depend on messages read/written prior within the same session. We prove that evaluation preserves typability and that well-typed processes are safe. This is joint work with Eduardo Bonelli and Elsa Gunter. Keywords: Pi-calculus, type systems, dependent types, session types, correspondence assertions. [CM98] Edmund Clarke and Will Marrero. Using formal methods for analyzing security. Information Survivability Workshop. 1998. [GJ01] Andrew Gordon and Alan Jeffrey. Typing correspondence assertions for communication protocols. In Seventeenth Conference on the Mathematical Foundations of Programming Semantics (MFPS 2001)}, number 45 in ENTCS. Elsevier, 2001. [HVK98] Kohei Honda, Vasco Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Proc. of ESOP'98, LNCS. Springer-Verlag, 1998.