What are the differences between logical relations and simulations? I'm a beginner working on methods proving program equivalence. I've read a few papers about defining logical relations or simulations to prove two programs are equivalent. But I am quite confused about these two techniques.

I only know logical relations are inductively defined while simulations are based on coinduction. Why are they defined in such ways? What are their pros and cons respectively? Which one should I choose in different situations?
I have an answer to this question which is possibly novel.  In fact, I am still thinking through it for the last 6 months or so, and it hasn't been written about in papers yet.

The general thesis is that relational reasoning principles like "logical relations", "simulations", and even "invariants" are manifestations of data abstraction or information hiding.  Wherever there is information hiding, these principles crop up.

The first people to discover it were automata theorists.  Automata have hidden state.  So you need relational reasoning to talk about their equivalence.  Automata theorists struggled with homomorphisms for a while, gave up, and came up with a notion called "relational covering", which is a form of simulation relations.

Milner picked up the idea in a little-known but very fundamental paper called "An algebraic notion of simulation between programs" in 1971.  Hoare knew it and used it in coming up with "Proof of correctness of data representations" in 1972 (but used abstraction functions instead of relations because he thought they were "simpler").  He later retracted the simplicity claim and went back to using relations in "Data refinement refined".  Reynolds used relational reasoning in "Craft of Programming", Chapter 5 (1981).  He thought relations were more natural and general than abstraction functions.  If you go back and read this chapter, you will find relational parametricity ideas lurking around, waiting to be discovered.  Sure enough, two years later, Reynolds published "Types, abstraction and parametric polymorphism" (1983).

It looks like all these ideas have nothing to do with types, but they really do.  Stateful languages and models have built-in data abstraction.  You don't need to define an "abstract data type" to get information hiding.  You just declare a local variable and hide it.  We can teach it to first year students in Java classes in the first few weeks.  No sweat.

Functional languages and models, on the other hand, have to get their information hiding via types.  Functional models don't have built-in data abstraction.  We have to add it on explicitly, using $\forall$ or $\exists$.  So, if you translate a stateful language into a functional language, you will notice all the local state getting translated into type variables.  For an explicit description of how this works, see my paper "Objects and classes in Algol-like languages", but the ideas really come from Reynolds 1981 ("The Essence of Algol"). We are just understanding those classic ideas better now.

Take two machines $M$ and $M'$ that you want to prove equivalent.  Milner 1971 says, define a relation between the states of $M$ and $M'$ and show that the two machines preserve the relation.  Reynolds parametricity says, think of the states of the machines as belonging to types $X$ and $X'$.  Define a relation $R$ between them.  If the machines are of type $F(X)$ and $F(X')$, parameterized by the types of their states, then check that the two machines are related by the relation $F(R)$.  

So, simulations and relational parametricity are essentially the same idea.  It is not merely a superficial resemblance.  The former is made for stateful languages where there is built-in data abstraction.  The latter is made for stateless languages where data abstraction is obtained via type variables.  

What about logical relations then?  On the surface, logical relations appear to be a more general idea.  Whereas parametricity talks about how to relate type variables within the same model, logical relations appear to relate types across different models.  (Dave Clarke wrote a brilliant exposition of this earlier.)  But my feeling is (and it still needs to be demonstrated) that this is an instance of some form of higher-type parametricity which hasn't yet been formulated.  Stay tuned for more progress on that front.



[Note added] The connection between logical relations and simulations is discussed in our recent paper Logical relations and parametricty: A Reynolds programme for Category Theory and Programming Languages.