CIU equivalence

Two programs are equivalent up to uses of closed instantations (or CIU equivalent) whenever they behave identically

after closing them (substituting for all their free variables), and
in all possible operational settings - e.g. in all possible states of memory, starting from any stack, etc.

CIU equivalence often coincides with contextual equivalence, even in the presence of recursive datatypes, mutable states, and even OO features.

It is closely related to applicative bisimilarity, as applied to functional and OO languages.

References

The notion of CIU equivalence first appeared in the following ICALP 1989 paper. The journal version appeared in 1991 in JFP.

Mason, Ian, and Carolyn Talcott. ‘Programming, Transforming, and Proving with Function Abstractions and Memories’. In Automata, Languages and Programming, edited by Giorgio Ausiello, Mariangiola Dezani-Ciancaglini, and Simonetta Ronchi Della Rocca, 372:574–88. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg, 1989. https://doi.org/10.1007/BFb0035784.

@inproceedings{mason_1989,
	location = {Berlin, Heidelberg},
	title = {Programming, transforming, and proving with function abstractions and memories},
	volume = {372},
	doi = {10.1007/BFb0035784},
	series = {Lecture Notes in Computer Science},
	pages = {574--588},
	booktitle = {Automata, Languages and Programming},
	publisher = {Springer Berlin Heidelberg},
	author = {Mason, Ian and Talcott, Carolyn},
	editor = {Ausiello, Giorgio and Dezani-Ciancaglini, Mariangiola and Della Rocca, Simonetta Ronchi},
	date = {1989},
}

Mason, Ian, and Carolyn Talcott. ‘Equivalence in Functional Languages with Effects’. Journal of Functional Programming 1, no. 3 (1991): 287–327. https://doi.org/10.1017/S0956796800000125.

@article{mason_1991,
	title = {Equivalence in functional languages with effects},
	volume = {1},
	doi = {10.1017/S0956796800000125},
	pages = {287--327},
	number = {3},
	journaltitle = {Journal of Functional Programming},
	author = {Mason, Ian and Talcott, Carolyn},
	date = {1991},
}

A tutorial presentation on how CIU equivalence can be used to characterise contextual equivalence, in a language with recursion, polymorphism, and existential types, is given by Andy Pitts in
A method for reasoning operationally about a language with existential types and recursion is presented in

Pitts, A. M. ‘Typed Operational Reasoning’. In Advanced Topics in Types and Programming Languages, edited by B. C. Pierce, 245–89. The MIT Press, 2005. pdf

@incollection{pitts_typed_2005,
	title = {Typed Operational Reasoning},
	pages = {245--289},
	booktitle = {Advanced Topics in Types and Programming Languages},
	publisher = {The {MIT} Press},
	author = {Pitts, A. M.},
	editor = {Pierce, B. C.},
	date = {2005},
}