Precise Reasoning with Structured Time, Structured Heaps, and Collective Operations

Program analysis by optimizing for clarity.

Coq Proof

Definition and modelization

IMP

• IMP language (Figure 3)
• IMP Relational big-step semantic (Figure 4)
  • Expression Evaluation
  • Loop Evaluation
  • Statement Evaluation
• IMP functonal semantics (Figure 5)
  • Expression Evaluation
  • Loop Evaluation
  • Statement Evaluation

FUN

• FUN language (Figure 6)
• FUN value representation for Option Monad (Figure 7)
• FUN small step semantics

IMP to FUN transformation

• Expression Transformation
• Statement Transformation
• Equivalence

Theorems

• IMP is deterministic

  • Expression Deterministic
  • Proposition 3.3

• Adequacy between big-step semantics and functional semantics.

  • Expression Adequacy
  • Statement Adequacy (1st half)
  • Statement Adequacy (2nd half)
  • Proposition 3.9

• Soundness of the IMP to FUN transformation

  • Expression Soundness
  • Statement Soundness
  • Theorem 3.14