<p><a href="https://doi.org/10.1145/1538788.1538814" rel="nofollow noreferrer">Leroy</a> uses simulation relations as a means of showing compiler correctness; the basic idea is that a simulation relation is an asymmetric binary relation between states in two different small step semantics such that initial states are related, and the relation is preserved under a single step in the first semantics by a finite sequence of steps (or sometimes none) in the second. This can be augmented with notions of trace inclusion, and then determinism proofs allow trace equivalence to be shown from the existence of a simulation.</p>
<p><a href="http://adam.chlipala.net/frap/" rel="nofollow noreferrer">Chlipala</a> covers this in his text (which is where I first learned about it), but there are no citations, and I'm not sure whether the method is due to Leroy or if it has earlier origins.</p>

CC BY-SA 4.0
2020-07-27T11:49:38.607Z
I have not had time to check in detail, but at a guess: this comes from Robin Milner, in particular his [17]. Milner has numerous publication that study various notions of equivalence.
Martin Berger
CC BY-SA 4.0
2020-07-27T12:53:08.170Z
@MartinBerger Thanks! (Can't upvote comments since this is a fresh account.) I found "An algebraic notion of simulation between programs" (1971) which applies simulation to programs within the same semantics which seems to be the earliest notion of this.
denotational
CC BY-SA 4.0
2020-07-27T13:27:39.517Z
@p0llard Milner's notion of simulation is quite natural, and I imagine (but don't know) that several other authors independently stumbled on it, maybe without naming it. E.g. Milner's coinductive notion of *bisimulation*  turns out also to have been invented independently multiple times: in philosophical logic (more precisely modal logic), in set theory (more precisely in the study of non-well-founded sets) and in model theory (Ehrenfeucht-Fraïsse games). See [On the Origins of Bisimulation and Coinduction](http://www.cs.unibo.it/~sangio/DOC_public/history_bis_coind.pdf).
Martin Berger
CC BY-SA 4.0
2020-07-29T10:47:08.563Z
My memory may be playing tricks on me again but I do seem to remember that Milner's (typically bi-) simulations are unnecessarily strong for ordinary compiler correctness. This changes only when compilers are expected to preserve non-trace properties such as non-interference. A decent reference on the classical compiler correctness literature should be in Müller-Olm's thesis (LNCS 1283). As an aside, Leroy unfortunately confuses the rest of the world by swapping names of his simulations compared to just about every precursor.
Kai
CC BY-SA 4.0
2020-07-29T12:57:45.733Z
@Kai > "Müller-Olm's thesis (LNCS 1283)" Wow, this is a great resource, thanks for pointing it out to me!
denotational
<reference-request><semantics><compilers><operational-semantics>
Origin of simulation relations for compiler correctness
denotational
# Origin of simulation relations for compiler correctness

(Asked by: username_0 on 2020-07-27)

[Leroy](https://doi.org/10.1145/1538788.1538814) uses simulation relations as a means of showing compiler correctness; the basic idea is that a simulation relation is an asymmetric binary relation between states in two different small step semantics such that initial states are related, and the relation is preserved under a single step in the first semantics by a finite sequence of steps (or sometimes none) in the second. This can be augmented with notions of trace inclusion, and then determinism proofs allow trace equivalence to be shown from the existence of a simulation.

[Chlipala](http://adam.chlipala.net/frap/) covers this in his text (which is where I first learned about it), but there are no citations, and I'm not sure whether the method is due to Leroy or if it has earlier origins.

**Tags:** reference-request, semantics, compilers, operational-semantics
> **Comments:**
> **username_1**: I have not had time to check in detail, but at a guess: this comes from Robin Milner, in particular his [17]. Milner has numerous publication that study various notions of equivalence.  
> **username_0**: @MartinBerger Thanks! (Can't upvote comments since this is a fresh account.) I found "An algebraic notion of simulation between programs" (1971) which applies simulation to programs within the same semantics which seems to be the earliest notion of this.  
> **username_1**: @p0llard Milner's notion of simulation is quite natural, and I imagine (but don't know) that several other authors independently stumbled on it, maybe without naming it. E.g. Milner's coinductive notion of *bisimulation*  turns out also to have been invented independently multiple times: in philosophical logic (more precisely modal logic), in set theory (more precisely in the study of non-well-founded sets) and in model theory (Ehrenfeucht-Fraïsse games). See [On the Origins of Bisimulation and Coinduction](http://www.cs.unibo.it/~sangio/DOC_public/history_bis_coind.pdf).  
> **username_2**: My memory may be playing tricks on me again but I do seem to remember that Milner's (typically bi-) simulations are unnecessarily strong for ordinary compiler correctness. This changes only when compilers are expected to preserve non-trace properties such as non-interference. A decent reference on the classical compiler correctness literature should be in Müller-Olm's thesis (LNCS 1283). As an aside, Leroy unfortunately confuses the rest of the world by swapping names of his simulations compared to just about every precursor.  
> **username_0**: @Kai > "Müller-Olm's thesis (LNCS 1283)" Wow, this is a great resource, thanks for pointing it out to me!  

---

## 0 answers

