• Robbert Krebbers's avatar
    Major revision of the whole development. · 18669b92
    Robbert Krebbers authored
    The main changes are:
    
    * Function calls in the operational semantics
    * Mutually recursive function calls in the axiomatic semantics
    * A general definition of the interpretation of the axiomatic semantics  so as
      to improve reusability (useful for function calls, and also for expressions
      in future versions)
    * Type classes for stack independent, memory independent, and memory extensible
      assertions, and a lot of instances to automatically derive these properties.
    * Many additional lemmas on the memory and more robust tactics to simplify
      goals involving is_free and mem_disjoint
    * Proof of preservation of statements in the smallstep semantics
    
    * Some new tactics: feed, feed destruct, feed inversion, etc...
    * More robust tactic scripts using bullets and structured scripts
    * Truncate most lines at 80 characters
    18669b92
monads.v 710 Bytes