Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing (Artifact)

• README.md
• algebra
  • multiset.v
• base_logic
  • adequacy.v
  • aprop.v
  • cgraph.v
  • linpred.v
  • miniprot.v
  • proofmode.v
  • uforests.v
  • wp.v
  • wp_prim.v
• examples
  • assert.v
  • basics.v
  • compare.v
  • list_rev.v
  • llist.v
  • prots.v
  • sort.v
  • sort_br_del.v
  • sort_fg.v
  • tour.v
• lang
  • lang.v
  • metatheory.v
  • notation.v
• logrel
  • contexts.v
  • examples
    • compute_service.v
    • pair.v
    • rec_subtyping.v
  • model.v
  • operators.v
  • session_types.v
  • session_typing_rules.v
  • subtyping.v
  • subtyping_rules.v
  • telescopes.v
  • term_types.v
  • term_typing_judgment.v
  • term_typing_rules.v
• prelude
  • prelude.v
• session_logic
  • imp.v
  • proofmode.v
  • sessions.v
  • sub.v
  • tele_imp.v

This is an archived artifact for the paper Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing by Jules Jacobs, Jonas Kastberg Hinrichsen, and Robbert Krebbers. The most recent version of the Coq code is available at https://github.com/julesjacobs/dlf-actris.

This artifact website is bidirectionally hyperlinked with the PDF of the paper:

• Definitions, theorems, and examples in the Coq code are hyperlinked to the corresponding location in the paper.
• Definitions, theorems, and examples in the paper are hyperlinked to the corresponding location in the Coq code.