Agda formalization for operational semantics of a simple imperative language, type-based information flow security, Hoare logic, verification conditions, and separation logic.
- IMP: syntax of the IMP language; evaluation of expressions and substitution lemma.
- OperationalSemantics: small-step and big-step semantics for IMP; determinism, program equivalence, equivalence between the two semantics.
- Security: security type system for IMP; non-interference, anti-monotonicity, confinement lemma.
- Types: type system for IMP; preservation, progress, type soundness.
- HoareLogic: Hoare logic; syntax, weakest preconditions, completeness and soundness.
- SeparationLogic: separation logic; frame lemmas.