Semantic and Syntactic Approaches to Simulation Relations

Jo Hannay, Shin-ya Katsumata, Donald Sannella

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationMathematical Foundations of Computer Science 2003 Book Subtitle
Subtitle of host publication28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25-29, 2003. Proceedings
EditorsBranislav Rovan, Peter Vojtás
Place of PublicationBerlin, Heidelberg
PublisherSpringer
Pages68-91
Number of pages24
ISBN (Electronic)978-3-540-45138-9
ISBN (Print)978-3-540-40671-6
DOIs
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume2747
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Semantic and Syntactic Approaches to Simulation Relations'. Together they form a unique fingerprint.

Cite this