Logical relations

Please expand.

History

Logical relations appear to have been discovered in the 1970s.

The most famous instance is the report of Plotkin 1973, where they are used as a way of characterising which functions can be expressed in \lambda-calculus.

In the report Plotkin credits the idea of using relations to Mike Gordon. He also points out that the first instance of using something akin to a logical relation for proving the equivalence of programs occurs in Robert Milne's 1973 thesis Milne 1973.

References

The first document to present logical relations as we understand them nowadays is Plotkin's 1973 report, where it is used to prove that certain functions are not definable in the \lambda-calculus:

Plotkin, G. D. ‘Lambda Definability and Logical Relations’. Memorandum. University of Edinburgh, 1973. pdf

@techreport{plotkin_lambda_1973,
	type = {Memorandum},
	title = {Lambda {Definability} and {Logical} {Relations}},
	url = {https://homepages.inf.ed.ac.uk/gdp/publications/logical_relations_1973.pdf},
	number = {SAI-RM-4},
	institution = {University of Edinburgh},
	author = {Plotkin, G. D.},
	year = {1973},
}

The first instance of something akin to a logical relation used for proving equivalence of programs is in

Milne, Robert. ‘The Formal Semantics of Computer Languages and Their Implementations’. University of Cambridge, 1974. link

@phdthesis{milne_1974,
	title = {The {Formal} {Semantics} of {Computer} {Languages} and {Their} {Implementations}},
	url = {https://www.cs.ox.ac.uk/publications/publication3763-abstract.html},
	school = {University of Cambridge},
	author = {Milne, Robert},
	year = {1974},
	note = {Distributed by the Oxford Programming Research Group as Photocopy PRG-X13.},
}