The following graph gives an overview of the development. Click on the nodes to jump to the corresponding file. A description of each file is below.

Prerequisites

• HeapF SLF's functor for building a separation logic, given a definition of values
• LibFmap extra lemmas and tactics for SLF's finite maps
• ExtraTactics miscellaneous general tactics

Main development

• Basics definitions of the programming langauge, the separation logic (via HeapF), the syntax and semantics of staged formulae (flow), entailment and equivalence and basic properties
• ShiftFree definition of what it means for a staged formula to be shift-free and associated tactics, as well as a typeclass version for use in rewriting
• Satisfies introduction and elimination lemmas for the constructs of staged logic
• Propriety Proper instances for rewriting
• Reduction lemmas for shift/reset reduction
• Norm lemmas for normalisation and simplification, to be used for rewriting
• Biab definition of biabduction
• Entl entailment lemmas, for meta-operations or finishing proofs
• GEnt generalised entailment
• Logic entry point which re-exports all the previous modules
• Automation tactics for working with staged logic
• Examples case studies

Inessential

• Tests
• Triples, Ent, ExamplesEnt, ReductionOld deprecated