一句话：为 K、T、K4、GL、S4 的必要性片段提出双上下文自然演绎与模态 λ 演算，并建立元理论与范畴语义。
论文针对模态逻辑必要性片段（K、T、K4、GL、S4），提出了一类双上下文自然演绎系统及相应的模态 λ 演算。系统区分模态假设与直觉主义假设两个区域，并说明其源于相应的 sequent 演算。作者研究这些演算的元理论，给出合流且强规范化的归约概念，证明其可证性与通常的 Hilbert 系统一致。最后建立范畴语义，将模态解释为保持乘积的函子，从而为双上下文模态演算提供语义基础。
We present natural deduction systems and associated modal lambda calculi for the necessity fragments of the normal modal logics K, T, K4, GL and S4. These systems are in the dual-context style: they feature two distinct zones of assumptions, one of which can be thought as modal, and the other as intuitionistic. We show that these calculi have their roots in in sequent calculi. We then investigate their metatheory, equip them with a confluent and strongly normalizing notion of reduction, and show that they coincide with the usual Hilbert systems up to provability. Finally, we investigate a categorical semantics which interprets the modality as a product-preserving functor. Comment: Full version of article previously presented at LICS 2017 (see arXiv:1602.04860v4 or doi: 10.1109/LICS.2017.8005089)