1. 06 Jun, 2018 2 commits
  2. 02 May, 2018 1 commit
    • Dan Frumin's avatar
      Simplify the Treiber stack refinement · bf38948f
      Dan Frumin authored
      The simplification is acheieved by removing the stackUR workaround.
      That RA was used to enusure that the nodes that were parts of the
      stack do not change themselves -- this is crucial for the safety of
      pop and iter operations.
      
      Now this is achieved by using duplicable propositions (∃ q, n ↦ᵢ{q} v)
      to ensure that the node are still alive/not freed.
      bf38948f
  3. 23 Apr, 2018 1 commit
  4. 28 Mar, 2018 1 commit
  5. 04 Jan, 2018 1 commit
  6. 03 Jan, 2018 1 commit
  7. 10 Dec, 2017 1 commit
  8. 29 Nov, 2017 1 commit
  9. 23 Nov, 2017 1 commit
  10. 28 Oct, 2017 1 commit
  11. 23 Oct, 2017 1 commit
  12. 22 Oct, 2017 1 commit
  13. 19 Oct, 2017 1 commit
  14. 28 Sep, 2017 1 commit
  15. 15 Sep, 2017 1 commit
    • Dan Frumin's avatar
      Some more examples · 1188cb70
      Dan Frumin authored
      From "The effects of higher-order state and control on local relational reasoning"
      1188cb70
  16. 13 Sep, 2017 1 commit
  17. 07 Sep, 2017 2 commits
  18. 06 Sep, 2017 1 commit
  19. 05 Sep, 2017 1 commit
  20. 28 Aug, 2017 1 commit
  21. 21 Aug, 2017 1 commit
    • Dan Frumin's avatar
      A common rel_pure_l/r tactic utilizing typeclass search · d7cada37
      Dan Frumin authored
      - The typeclass `PureExec e1 e2` controls pure deterministic
        reductions
      - General tactics rel_pure_l and rel_pure_r that depend on that typeclass
      - The same typeclass can be used for WP tactics and tp tactics, potentially
      d7cada37
  22. 17 Aug, 2017 1 commit
  23. 15 Aug, 2017 1 commit
    • Dan Frumin's avatar
      Bit flipping example · cce140f7
      Dan Frumin authored
      - Add more binary ops to the language
      - An example refinement for module types
      cce140f7
  24. 14 Aug, 2017 1 commit
  25. 07 Aug, 2017 2 commits
  26. 21 Jul, 2017 1 commit
  27. 14 Jul, 2017 1 commit
  28. 04 Jul, 2017 1 commit
  29. 03 Jul, 2017 1 commit
  30. 18 Apr, 2017 1 commit
  31. 10 Apr, 2017 1 commit
  32. 21 Mar, 2017 1 commit
  33. 01 Mar, 2017 1 commit
  34. 28 Feb, 2017 1 commit
  35. 16 Nov, 2016 1 commit
  36. 05 Jul, 2016 1 commit
  37. 30 May, 2016 1 commit
    • Amin Timany's avatar
      Change congruence lemmas of Fμ,ref,par · a17bf389
      Amin Timany authored
      The case of lam and case expressions that before required the terms to be
      well-typed now require terms to be closed.
      
      Separated definition context and context refinement from soundness_binary file.
      a17bf389