Forked from
Iris / stdpp
2795 commits behind the upstream repository.
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
| Name | Last commit | Last update |
|---|---|---|
| .. | ||
| base.v | ||
| collections.v | ||
| decidable.v | ||
| fin_collections.v | ||
| fin_maps.v | ||
| list.v | ||
| listset.v | ||
| monads.v | ||
| nmap.v | ||
| numbers.v | ||
| option.v | ||
| orders.v | ||
| pmap.v | ||
| prelude.v | ||
| subset.v | ||
| trs.v | ||