Authors | J. E. Hannay, S. -. Y. Katsumata and D. T. Sannella |
Title | Semantic and Syntactic Approaches to Simulation Relations |
Afilliation | Software Engineering, Software Engineering |
Status | Published |
Publication Type | Proceedings, refereed |
Year of Publication | 2003 |
Conference Name | Mathematical Foundations of Computer Science. Proceedings of MFCS, 28th International Symposium on Mathematical Foundations of Computer Science, Bratislava, Slovak Republic, LNCS volume 2747 |
Pagination | 68-91 |
Date Published | August 25 - 29 |
Publisher | Springer-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 Key | SE.5.Hannay.2003.c |