vellvm/ctrees

Issues

• [CTL] Coinduction lemma

  #30 opened a year ago by elefthei
  0

• [CTL] Make low-level definitions opaque

  #29 opened 2 years ago by elefthei
  0

• Idea: Branching Temporal Logic -> ctrees

  #16 opened 2 years ago by elefthei
  1

• Performance issue

  #27 opened 2 years ago by YaZko
  0

• __upto_bind_eq_ssim is broken

  #26 opened 2 years ago by nchappe
  0

• Prove *complete* simulations for the constant and state schedulers

  #25 opened 2 years ago by nchappe
  0

• Recovering the companion's "symmetric" tactic in the heterogeneous branch

  #20 opened 2 years ago by YaZko
  1

• Proper instance for heterogeneous ssim

  #24 opened 2 years ago by nchappe
  0

• Trade off in representations

  #23 opened 2 years ago by YaZko
  0

• On a canonical representation for stuck

  #22 opened 2 years ago by YaZko
  0

• On specifiying the relation `L` fed to (bi)simulations

  #21 opened 2 years ago by YaZko
  0

• Meta-theory for refinements/simulations

  #6 opened 2 years ago by YaZko
  1

• Use the fin from ExtLib

  #15 opened 3 years ago by elefthei
  2

• Posing definitions rather than notations for the main relations

  #1 opened 3 years ago by YaZko
  1

• Non-finite internal branching

  #3 opened 3 years ago by YaZko
  1

• Messed up reduction behavior of bind

  #10 opened 3 years ago by YaZko
  2

• Universe inconsistency with ITree.Events.StateFacts

  #8 opened 3 years ago by elefthei
  1

• Allowing for an heterogeneous relation on labels

  #4 opened 3 years ago by YaZko
  4

• Limiting the use of [JMeq_eq]

  #5 opened 3 years ago by YaZko
  0

• Swiss army knife for inversion

  #2 opened 3 years ago by YaZko
  0