Skip to content
Snippets Groups Projects

Amin/logrel

Amin/logrel
amin/logrel into master
1 unresolved thread
Merged Amin Timany requested to merge amin/logrel into master
1 unresolved thread

Add logical relations from IPM paper to iris-examples. This closes #2 (closed).

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Ralf Jung
    Ralf Jung @jung
    Owner

    Thanks, this is great!

    Could you rebase onto current master and add a section to the README explaining this case study and referencing the paper?

  • Amin Timany added 4 commits

    added 4 commits

    Compare with previous version

    Toggle commit list
  • Amin Timany resolved all discussions

    resolved all discussions

  • Amin Timany
    Amin Timany @amintimany
    Author Developer

    Done!

  • Amin Timany
    Amin Timany @amintimany
    Author Developer

    @jung If you have no objection we can merge this!

  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • README.md
    30 30
    31 31 * [barrier](theories/barrier): The implementation and proof of a barrier as
    32 32 described in "Higher-Order Ghost State" <http://doi.acm.org/10.1145/2818638>.
    33 * [logrel](theories/logrel): the following logical relations from the paper <http://doi.acm.org/10.1145/3093333.3009855>:
    34 * STLC
    35 * Unary logical relations proving type safety
    36 * F_mu (System F with recursive types)
    37 * Unary logical relations proving type safety
    38 * F_mu_ref (System F with recursive types and references)
    39 * Unary logical relations proving type safety
    40 * Binary logical relations for proving contextual refinements
    41 * F_mu_ref_conc (System F with recursive types, references and concurrency)
    42 * Unary logical relations proving type safety
    43 * Binary logical relations for proving contextual refinements
    44 * Proof of refinement for a pair of fine-grained/coarse-grained concurrent counter implementations
    45 * Proof of refinement for a pair of fine-grained/coarse-grained concurrent stack implementations
  • Ralf Jung mentioned in commit 5d574803

    mentioned in commit 5d574803

  • Ralf Jung merged

    merged

  • Ralf Jung mentioned in commit 7c6793f3

    mentioned in commit 7c6793f3

    • Please register or sign in to reply