Appendix for "Extending Separation Logic with Fixpoints and Postponed Substitution", Élodie-Jane Sims, TCS Vol. 351, Issue 2

Not everything is typed yet...

We changed some notations,
if there is somewhere a γ(P) it stands for [[P]]
if there is somewhere a Γρ(P) it stands for [[P]]ρ
if there is somewher P[E/x] it stands for the connective of postponned substitution

• Definitions of Var(E), Var(P), FV(E), FV(P), FVv(P), v-closed, P{[z/y]} (ps.gz, pdf)
• Th. 4: Stack Extension Theorem

  If nodep(z,ρ) z ∉ FV(P) FVv(P) ∈ dom(ρ) [[P]]ρ exists Then nodep(z,[[P]]ρ)

  Proofs (ps.gz,pdf)
• Th. 5: Variable Renaming Theorem for BIμν

  If P is v-closed z ∉ Var(P) y ∉ FV(P) Then P ≡ P{[z/y]}

  and more generaly Th. 6:

  If nodep(z,ρ) FVv(P) ∈ dom(&rho) z ∉ Var(P) Then [[P{[z/y]}]]ρ° = {s,h | s°,h ∈ [[P]]ρ }

  Proofs (ps.gz,pdf)
• Th. 7,8: Unfolding theorems :

  μ Xv. P ≡ P{(μ Xv.P)/Xv}

  ν Xv. P ≡ P{(ν Xv.P)/Xv}

  (ps.gz,pdf)
• Proofs of the wlp (not typed yet...)
• Proofs of the sp (ps.gz,pdf)
• Th. 9: A v-variable substitution result

  If [[Y]] exists [[P]] [ρ | Xv → [[Y]] ] exists then [[P]] [ρ | Xv → [[Y]] ] = [[ P{(Y)/Xv} ]] ρ

  (ps.gz,pdf)
• Th. 10: A v-variables substitution result generalized

  If [[Y]]ρ exists [[P]] [ρ | Xv → [[Y]]ρ] or [[P{(Y)/Xv}]]ρ exists then [[P]] [ρ | Xv → [[Y]]ρ] = [[P{(Y)/Xv}]]ρ

  (ps.gz,pdf)
• Th. 11: μ and ν coincide

  μ Xv. P ≡ ¬ ν Xv. ¬ P{¬Xv/Xv}

  ν Xv. P ≡ ¬ μ Xv. ¬ P{¬Xv/Xv}

  (ps.gz,pdf)
• Proofs of the wlp (not typed yet...)
• Some simplification on [/] (ps.gz,pdf)
• Upper-continuous result (ps.gz,pdf)

---

Contact: Elodie-JaneSimspolytechniqueedu Last modified: April 2010

Back