1. 26 Aug, 2019 1 commit
  2. 13 Jul, 2019 1 commit
  3. 30 Jun, 2019 1 commit
  4. 18 Jun, 2019 1 commit
  5. 10 May, 2019 2 commits
  6. 09 May, 2019 1 commit
  7. 29 Jan, 2019 1 commit
  8. 28 Nov, 2018 1 commit
  9. 21 Sep, 2017 1 commit
  10. 02 Aug, 2017 1 commit
  11. 05 Jul, 2017 1 commit
  12. 30 May, 2017 1 commit
  13. 15 Mar, 2017 1 commit
  14. 31 Jan, 2017 3 commits
  15. 20 Sep, 2016 1 commit
  16. 14 Sep, 2016 1 commit
  17. 04 May, 2016 1 commit
  18. 07 Apr, 2016 1 commit
  19. 03 Mar, 2016 1 commit
  20. 13 Feb, 2016 1 commit
  21. 11 Feb, 2016 1 commit
  22. 16 Nov, 2015 1 commit
  23. 01 Feb, 2017 1 commit
    • Robbert Krebbers's avatar
      Port to Coq 8.5 beta 2. · 02f213ce
      Robbert Krebbers authored
      The port makes the following notable changes:
      
      * The carrier types of separation algebras and integer environments are no
        longer in Set. Now they have a type at a fixed type level above Set. This
        both works better in 8.5 and makes the formalization more general.
        I have tried putting them at polymorphic type levels, but that increased the
        compilation time by an order of magnitude.
      * I am using a custom f_equal tactic written in Ltac to circumvent bug #4069.
        That bug has been fixed, so this custom tactic can be removed when the next
        beta of 8.5 is out.
      02f213ce
  24. 08 Feb, 2015 1 commit
  25. 23 Dec, 2014 1 commit
    • Robbert Krebbers's avatar
      More lenient pointer equality. · 914f32ee
      Robbert Krebbers authored
      Pointer equality is now defined using absolute object offsets. The treatment
      is similar to CompCert:
      
      * Equality of pointers in the same object is defined provided the object has
        not been deallocated.
      * Equality of pointers in different objects is defined provided both pointers
        have not been deallocated and both are strict (i.e. not end-of-array).
      
      Thus, pointer equality is defined for all pointers that are not-end-of-array
      and have not been deallocated. The following examples have defined behavior:
      
        int x, y;
        printf("%d\n", &x == &y);
        int *p = malloc(sizeof(int)), *q = malloc(sizeof(int));
        printf("%d\n", p == q);
        struct S { int a; int b; } s, *r = &s;
        printf("%d\n", &s.a + 1 == &(r->b));
      
      The following not:
      
        int x, y;
        printf("%d\n", &x + 1 == &y);
      914f32ee
  26. 22 Aug, 2014 1 commit
    • Robbert Krebbers's avatar
      Modify typing judgments to depend on a description of the types of objects in · 7f9c5994
      Robbert Krebbers authored
      memory instead of the whole memory itself.
      
      This has the following advantages:
      * Avoid parametrization in {addresses,pointers,pointer_bits,bits}.v
      * Make {base_values,values}.v independent of the memory, this makes better
        parallelized compilation possible.
      * Allow small memories (e.g. singletons as used in separation logic) with
        addresses to objects in another part to be typed.
      * Some proofs become easier, because the memory environments are preserved
        under many operations (insert, force, lock, unlock).
      
      It also as the following disadvantages:
      * At all kinds of places we now have explicit casts from memories to memory
        environments. This is kind of ugly. Note, we cannot declare memenv_of as a
        Coercion because it is non-uniform.
      * It is a bit inefficient with respect to the interpreter, because memory
        environments are finite functions instead of proper functions, so calling
        memenv_of often (which we do) is not too good.
      7f9c5994
  27. 22 May, 2014 1 commit
    • Robbert Krebbers's avatar
      Various changes. · bb9d75d9
      Robbert Krebbers authored
      * Parametrize refinements with memories. This way, refinements imply typing,
        for example [w1 ⊑{Γ,f@m1↦m2} w2 : τ → (Γ,m1) ⊢ w1 : τ]. This relieves us from
        various hacks.
      * Use addresses instead of index/references pairs for lookup and alter
        operations on memories.
      * Prove various disjointness properties.
      bb9d75d9
  28. 02 May, 2014 2 commits
  29. 21 Aug, 2013 1 commit
  30. 24 Jun, 2013 1 commit
  31. 21 May, 2013 1 commit
  32. 07 May, 2013 1 commit
    • Robbert Krebbers's avatar
      Lots of refactoring. and new results on permutations and list containment. · 361308c7
      Robbert Krebbers authored
      The refactoring includes:
      * Use infix notations for the various list relations
      * More consistent naming
      * Put lemmas on one line whenever possible
      * Change proofs into one-liners when possible
      * Make better use of the "Implicit Types" command
      * Improve the order of the list module by placing all definitions at the start,
        then the proofs, and finally the tactics.
      
      Besides, there is some new machinery for proofs by reflection on lists. It is
      used for a decision procedure for permutations and list containment.
      361308c7
  33. 14 Mar, 2013 1 commit
  34. 19 Feb, 2013 1 commit
    • Robbert Krebbers's avatar
      Support sequence point, add permissions, and update prelude. · 415a4f1c
      Robbert Krebbers authored
      Both the operational and axiomatic semantics are extended with sequence points
      and a permission system based on fractional permissions. In order to achieve
      this, the memory model has been completely revised, and is now built on top
      of an abstract interface for permissions.
      
      Apart from these changed, the library on lists and sets has been heavily
      extended, and minor changed have been made to other parts of the prelude.
      415a4f1c
  35. 01 Feb, 2013 1 commit
  36. 09 Jan, 2013 1 commit