Session types provide a static guarantee that concurrent programs respect communication protocols. Recently Caires, et al., have developed a correspondence between the propositions of linear logic and session typed pi-calculus processes. We relate the cut-elimination semantics of this approach to an operational semantics for session-typed concurrency in a functional language. We begin by presenting a variant of Wadler’s minimal session-typed functional language, GV. We give a small-step operational semantics for GV. We develop a suitable notion of deadlock for our functional setting, based on existing approaches for capturing deadlock in pi-calculus, and show that all well-typed GV programs are deadlock-free, deterministic and terminating.