一句话：统一刻画 System F 的一类可实现性语义，证明正类型完备性及闭实现子的参数性条件。
本文研究 System F 的可实现性语义中的完备性与参数性。作者考虑由 λ-项集合上的闭包算子定义的一大类可实现性语义，该类涵盖用于正规化定理的多数语义，如 Tait 饱和集与 Girard 可归约候选。文章给出正类型的完备性定理，该结果蕴含文献中已有结论；并证明闭实现子满足参数性条件，这些条件可表述为对逻辑关系的不变性或双自然性。由此推出，对于正类型，闭正规 λ-项的可类型性、可实现性与参数性三者等价。
We investigate completeness and parametricity for a general class of realizability semantics for System F defined in terms of closure operators over sets of $\lambda$-terms. This class includes most semantics used for normalization theorems, as those arising from Tait's saturated sets and Girard's reducibility candidates. We establish a completeness result for positive types which subsumes those existing in the literature, and we show that closed realizers satisfy parametricity conditions expressed either as invariance with respect to logical relations or as dinaturality. Our results imply that, for positive types, typability, realizability and parametricity are equivalent properties of closed normal $\lambda$-terms.
@article{paperbot747,
title = {On completeness and parametricity in the realizability semantics of System F},
author = {Paolo Pistone},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 4},
year = {2019},
doi = {10.23638/lmcs-15(4:6)2019}
}