一句话：建立多态会话π演算与线性System F之间互逆且完全抽象的编码，并由函数理论导出会话类型结果。
本文利用会话类型的逻辑基础，研究何种类型规则能够精确刻画Λ演算行为。基于线性逻辑相继演算与自然演绎可靠性和完备性的证明论内容，作者首次给出多态会话π演算与线性System F之间的相互可逆、完全抽象的过程即函数与函数即过程编码。由此可将Λ演算理论迁移到会话演算：一方面通过System F中的代数表示刻画归纳与余归纳会话类型；另一方面将结果扩展到支持值传递与进程传递，并证明强规范化。
This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.