[Identified a problem in the paper.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080429140758] hunk ./VirtualMachine.agda 12
+open import Logic
+
+------------------------------------------------------------------------
+-- Virtual machine
hunk ./VirtualMachine.agda 80
+------------------------------------------------------------------------
+-- Compiler
+
hunk ./VirtualMachine.agda 95
--- Statement of compiler correctness.
+------------------------------------------------------------------------
+-- Statement of compiler correctness
+
+-- Reflexive transitive closure of the transition relation. Indicates
+-- the reachable states.
hunk ./VirtualMachine.agda 104
+-- x ⟶ means that x is not stuck.
+
+_⟶ : State -> Set
+x ⟶ = ∃₀ \y -> x ⟶ y
+
+-- x ◁ P means that at least one state in P will be reached.
+
+-- Note that the definition used in the paper is incorrect. If, for
+-- instance, _⟶_ contains a transition to some stuck state s from all
+-- other states, then s ◁ P (as defined in the paper, i.e. without
+-- "x ⟶") is trivially satisfied for any s and P.
+
hunk ./VirtualMachine.agda 117
+  -- P will be reached because we are already there.
hunk ./VirtualMachine.agda 119
-  via      : (forall {y} -> x ⟶ y -> y ◁ P) -> x ◁ P
+  -- P will be reached because
+  --   ⑴ we can take a step, and
+  --   ⑵ no matter which step we take we will reach P.
+  via : x ⟶ -> (forall {y} -> x ⟶ y -> y ◁ P) -> x ◁ P
+
+-- Conjunction of the previous two definitions.
hunk ./VirtualMachine.agda 129
+-- The states that must be reachable and reached.
+
hunk ./VirtualMachine.agda 137
+-- Compiler correctness.
+