ROOT

chapter Quantitative_Separation_Logic

session Quantitative_Separation_Logic = HOL +
  sessions
    Separation_Algebra "HOL-Library"

  theories
    Quantitative_Separation_Connectives
    Assertions_With_State
    Sep_Heap_Instance

    HPGCL \<comment> \<open>The deeply embedded heap-manipulating probabilistic guarded command language.\<close>

    QSL_For_Potentials

    QSL_For_Probabilities

    QSL_For_Expectations

    QSL

    (* HPGCL_Expected_Running_Time *) \<comment> \<open>Experimental, a ert calculus for hpGCL\<close>

    (* Sized_Separation_Algebra *) \<comment> \<open>A separation algebra with a size operation\<close>

    (* QSL_For_Experimental_Domains *) \<comment> \<open>Experimental, try to instantiate enat option as quantale\<close>

  document_files
    "root.bib"