Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 151
    • Issues 151
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 9
    • Merge requests 9
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #29
Closed
Open
Created Aug 16, 2016 by Jeehoon Kang@jeehoon.kang😴Contributor1 of 2 tasks completed1/2 tasks

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
Time tracking