---

B Proofs for typing

• Basic properties
• Subject reduction for the chemical semantics (Theorem 1.1)
  • Case 1.
  • Case 2.
• Subject reduction for the rewriting semantics (Theorem 1.2)
  • Basic cases.
  • Inductive cases.
  • Basic cases for class reduction.
  • Basic cases for processes.
  • Inductive cases for classes.
  • Inductive cases for processes.
• Safety (Theorem 2)
  • No free variables.
  • No runtime failure.
  • No class rewriting failure.

---