Skip to content

Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language

License

Notifications You must be signed in to change notification settings

iwilare/formal-methods

Repository files navigation

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.

About

Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language

Topics

Resources

License

Security policy

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages