Abstract of Paper

Semantic and Syntactic Approaches to Simulation Relations
by Jo Hannay, Shin-ya Katsumata, and Donald Sannella

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.