Hoare Logic of a small language in Agda.
- Small-step & big-step operational semantics
- Equivalence between the small-step & big-step operational semantics
- Hoare Logic with embedded assertion logic
- Soundness of Hoare Logic on the small-step semantics
salty-Frankenstein/AgdaHoare
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|