AuthorsJ. E. Hannay, S. -. Y. Katsumata and D. T. Sannella
TitleSemantic and Syntactic Approaches to Simulation Relations
AfilliationSoftware Engineering, Software Engineering
StatusPublished
Publication TypeProceedings, refereed
Year of Publication2003
Conference NameMathematical Foundations of Computer Science. Proceedings of MFCS, 28th International Symposium on Mathematical Foundations of Computer Science, Bratislava, Slovak Republic, LNCS volume 2747
Pagination68-91
Date PublishedAugust 25 - 29
PublisherSpringer-Verlag
Abstract

Simulation relations are tools for establishing the correctness of data refinement steps. In the simply-typed lambda calculus, logical relations are the standard choice for simulation relations, but they suffer from certain shortcomings; these are resolved by use of the weaker notion of pre-logical relations instead. Developed from a syntactic setting, abstraction barrier-observing simulation relations serve the same purpose, and also handle polymorphic operations. Meanwhile, second-order pre-logical relations directly generalise pre-logical relations to polymorphic lambda calculus (System F). We compile the main refinement-pertinent results of these various notions of simulation relation, and try to raise some issues for aiding their comparison and reconciliation.

Notes

Invited paper.

Citation KeySE.5.Hannay.2003.c