Paolo Pistone - On completeness and parametricity in the realizability semantics of System F

lmcs:4293 - Logical Methods in Computer Science, October 29, 2019, Volume 15, Issue 4 - https://doi.org/10.23638/LMCS-15(4:6)2019
On completeness and parametricity in the realizability semantics of System FArticle

Authors: Paolo Pistone

    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.


    Volume: Volume 15, Issue 4
    Published on: October 29, 2019
    Accepted on: July 13, 2019
    Submitted on: February 17, 2018
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,03B15, 03B70, 03F03, 03F05,F.4.1

    Consultation statistics

    This page has been seen 1855 times.
    This article's PDF has been downloaded 368 times.