Session types are behavioral types that specify protocols of message-passing concurrent systems. Typing not only delimits the range of possible messages that can be exchanged but also the order in which the exchange must happen. Session types enjoy a strong theoretical foundation, established by a Curry-Howard correspondence between the session-typed pi-calculus and linear logic. Desirable language properties, such as deadlock freedom and termination, immediately hold true for languages building on this foundation, by virtue of cut elimination of the underlying logic. However, these results only generalize to such languages, if cut reductions are assumed to inform transitions. Yet existing session-type languages typically define transitions explicitly by operational semantics. Then termination must be proved by other means, for example by a logical relations argument.

This paper develops a logical relation for termination for intuitionistic linear logic session types (ILLST) and proves that well-typed ILLST programs are terminating (fundamental theorem). The logical relation is semantic and does not require terms to be well-typed. All results have been mechanized in the Coq proof assistant, amounting to the first mechanization of a logical relation for termination of session types. The paper introduces ILLST, its logical relation, and a novel rooted tree dynamics.