Post #1506862

@chrisamaphone @cbaberle The logical relation with a monoid thing reminded me of Dal Lago's and Hofmann's quantitative realisability [1] and Aloïs Brunel's PhD work extending it to biorthogonality/forcing [2,3], which was a precursor to Brunel et al.'s coeffect/graded calculus. It is probably more remote (they do not investigate linear parametricity results to my knowledge, and definitely do not look at ordered logic) but Aloïs's PhD work is amazing and I thought you might like to hear about it (I suspect that one might not easily stumble upon it). [1] https://www.sciencedirect.com/science/article/pii/S0304397510007164 [2] https://theses.hal.science/tel-01162997 [3] http://arxiv.org/abs/1201.4307