Two programs are equivalent up to uses of closed instantations (or CIU equivalent) whenever they behave identically
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.
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},
}
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},
}