Skip to content

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
    • Help
    • Support
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project
    • Project
    • Details
    • Activity
    • Releases
    • Cycle Analytics
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Charts
  • Issues 76
    • Issues 76
    • List
    • Boards
    • Labels
    • Milestones
  • Merge Requests 5
    • Merge Requests 5
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Charts
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Charts
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Iris
  • Iris
  • Issues
  • #29

Closed
Open
Opened Aug 16, 2016 by Jeehoon Kang@jeehoon.kang😴1 of 2 tasks completed1/2 tasks
  • Report abuse
  • New issue
Report abuse New issue

Bring back Logically Atomic Triples (Coq + docs)

  • Implement logically atomic triples in Coq.
  • Do a LaTeX write-up of logically atomic triples (either in The Iris Documentation, or referenced from there).

Original description

  • May I ask if the POPL 2015 paper's appendix is still in the repository (http://plv.mpi-sws.org/iris/appendix.pdf)?
  • Do you have a plan to merge the appendix of POPL 2015 paper and that of ICFP 2016? It would be definitely helpful to readers like me.

@jung wrote

The POPL 2015 appendix has been split into two parts:

  • The Iris Documentation is describing Iris in general, from the model through the base logic to the most important derived constructions. The version matching Iris 2.0 can be found on the website. It should have more derived constructions than it does, like STSs... however, we are currently in the process of redesigning how constructions like STSs describe their interface to the world, so now would be a bad time to update the documentation :/

  • The details of logically atomic triples. These triples have not been ported to later versions of Iris, which is why they don't show up in the current appendix. Unfortunately, since pretty much all examples involve logically atomic triples, those are now all outdated as well. (On paper, that is.)

What, specifically, are you missing from the POPL 2015 appendix?

Edited Jul 13, 2018 by Ralf Jung
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
3
Labels
A-theory C-project T-logical-atomicity
Assign labels
  • View project labels
Reference: iris/iris#29