OPLSS
Preface
Total and Partial Maps (Maps)
Simple Imperative Programs (Imp)
ImpShort
Hoare Logic, Part I (Hoare)
Introduction
Monads
Free
ITrees
ITreesEquiv
ImpDenotation
ImpEquiv
- Equivalence of Imp programs
- Elementary properties of program equivalences
- Syntactic contexts
- Semantically Characterizing Evaluation
- Universally valid static rewrite rules: an inventory
- Semantic validity of our calculus
- A sound static calculus
- Soundly lifting the calculus
- Proving program equivalences
- Constant folding as a tactic
- Constant folding as a sound optimization
- State algebra