[TYPES] logical relations

[Uday Reddy]

Eijiro Sumii writes:

> HOWEVER, according to my quick "eye grep" of this paper, it does not
> seem to contain the words "logical relations" nor
> "main/basic/fundamental lemma/theorem" anywhere, so I still do not
> know the answer to the "for what reason" part of my question.

Here is my guess as to "for what reason":

The correspondence between type systems and logics has been known
since Curry's time.  Since logical relations are built using that
correspondence (times as conjunction, -> as implication and so on.)
it was appropriate to call them "logical" relations, i.e., families of
relations obtained by treating type constructors as logical connectives.

Claudio Hermida tried to squeeze out this correspondence more formally
and succeeded to a large degree:

@PhDThesis(Hermida-thesis,
        Author = "Hermida, C.",
        Title = "Fibrations, Logical Predicates and Indeterminantes",
        School = "Aarhus University",
        Year = "1993"
        )

Cheers,
Uday