The term Kripke logical relations may refer to either of two closely related of the logical relations technique:
This type of relation was introduced in [Plotkin 1973, 1980] to reason about definability in the simply-typed -calculus.
In more recent years, such Kripke logical relations have proven to be very useful for reasoning about programming languages with effects.
Logical relations of varying arity were introduced by [Jung and Tiuryn 1993], again with a view to characterising definability in the simply-typed -calculus.
In this setting, it is the arity of the relation that varies. The arities are often given by sets (often finite). Then, a logical relation is just a subset of -indexed tuples of the interpretation of a type . For example, if , we obtain the usual binary logical relations.
The variation in the arities usually happens by setting up a small category of sets , and functions between them. If we are given and a relation , we can define a relation
by letting .
This set up subsumes the relations that vary over a Kripke world: take a category all of whose objects have the same cardinality (the arity), and all of whose morphisms are bijections, such that the category is isomorphic to the Kripke frame.
Plotkin, G. D. 1973. ‘Lambda Definability and Logical Relations’. Memorandum SAI-RM-4. University of Edinburgh. [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}
}
Plotkin, Gordon D. 1980. ‘Lambda-Definability in the Full Type Hierarchy’. In To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, edited by J. P. Seldin and J. R. Hindley, 363–73. New York: Academic Press. [pdf]
@incollection{plotkin_lambda-definability_1980,
address = {New York},
title = {Lambda-{Definability} in the {Full} {Type} {Hierarchy}},
url = {https://homepages.inf.ed.ac.uk/gdp/publications/Lambda_Definability.pdf},
booktitle = {To {H}. {B}. {Curry}: {Essays} in {Combinatory} {Logic}, {Lambda} {Calculus}, and {Formalism}},
publisher = {Academic Press},
author = {Plotkin, Gordon D.},
editor = {Seldin, J. P. and Hindley, J. R.},
year = {1980},
pages = {363--373}
}
Jung, Achim, and Jerzy Tiuryn. 1993. ‘A New Characterization of Lambda Definability’. In Typed Lambda Calculi and Applications, edited by Marc Bezem and Jan Friso Groote, 664:245–57. Lecture Notes in Computer Science. Berlin/Heidelberg: Springer-Verlag. https://doi.org/10.1007/BFb0037110.
@inproceedings{jung_1993,
address = {Berlin/Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {A new characterization of lambda definability},
volume = {664},
doi = {10.1007/BFb0037110},
booktitle = {Typed {Lambda} {Calculi} and {Applications}},
publisher = {Springer-Verlag},
author = {Jung, Achim and Tiuryn, Jerzy},
editor = {Bezem, Marc and Groote, Jan Friso},
year = {1993},
pages = {245--257}
}