Skip to content

Latest commit

 

History

History
12 lines (9 loc) · 868 Bytes

README.md

File metadata and controls

12 lines (9 loc) · 868 Bytes
Raw

Formal Methods in Agda

Agda formalization for operational semantics of a simple imperative language, type-based information flow security, Hoare logic, verification conditions, and separation logic.

Files structure

  • 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.