• README.md
• cgraphs
  • bi.v
  • cgraph.v
  • genericinv.v
  • mapexcl.v
  • multiset.v
  • seplogic.v
  • uforests.v
  • upred.v
  • util.v
• dlfactris
  • 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
    • 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
• lambdabar
  • compiler.v
  • definitions.v
  • invariant.v
  • langdef.v
  • langtools.v
  • letmacro.v
  • rtypesystem.v
  • sessions.v
  • theorems.v
• locks
  • lambdalock
    • definitions.v
    • invariant.v
    • langdef.v
    • langtools.v
    • letmacro.v
    • rtypesystem.v
    • theorems.v
  • lambdalockpp
    • definitions.v
    • invariant.v
    • langdef.v
    • langtools.v
    • letmacro.v
    • rtypesystem.v
    • theorems.v
• miniactris
  • base.v
  • imp.v
  • send_close.v
  • session.v
  • sub.v
  • sym_close.v
• multiparty
  • binary.v
  • definitions.v
  • globaltypes.v
  • invariant.v
  • langdef.v
  • mutil.v
  • progress.v
  • rtypesystem.v
  • theorems.v
  • ycombinator.v
• sessiontypes
  • invariant.v
  • langdef.v
  • progress.v
  • rtypesystem.v
  • safety.v
  • ycombinator.v

Guarantees by Construction

This directory contains the formalization of the PhD thesis Guarantees by Construction by Jules Jacobs.

The formalization is based on artifacts associated with papers that were co-authored with Robbert Krebbers, Stephanie Balzer, and Jonas Kastberg Hinrichsen.