equivalence-of-cast-calculi

Inventory

Where to find the definitions?

• The D abstract machine
• The S(C) abstract machine
• Cast ADT
• Lazy D hypercoercions(Including theorems about it)
• List-based Cast ADT

Where to find the theorems?

• Lemma 4.6 (applyCast Preserves Bisimulation)
• Lemma 4.7 (Weak Bisimulation between S(C) and D)
• Corollary 4.8 (Correctness of S(C))
• Lemma 4.9 (Strong Bisimulation Among S(·))
• Proposition 4.10 (Equivalence of Two Lazy D Cast ADTs)
• Proposition 4.11 (L Properties)
• Lemma 4.12 (L is Correct wrt. D)
• Theorem 4.13 (S(C) is Correct wrt. D)