AgdaHoare 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