Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 120
    • Issues 120
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 16
    • Merge Requests 16
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • Iris
  • Issues

  • Open 120
  • Closed 266
  • All 386
New issue
  • Priority Created date Last updated Milestone due date Due date Popularity Label priority Manual
  • Address the STS encodings lack of usefulness
    #286 · opened Jan 30, 2020 by Jonas Kastberg   A-coq C-enhancement T-algebra
    • 1
    • 5
    updated Jan 30, 2020
  • Documentation for installation on OS X
    #280 · opened Dec 16, 2019 by Jules Jacobs   A-docs C-enhancement
    • 1
    • 8
    updated Feb 06, 2020
  • Write `wp_` lemmas for array operations in a more `iApply`/`wp_apply` friendly way
    #278 · opened Dec 09, 2019 by Ralf Jung   A-coq C-bug T-heap_lang
    • 4
    updated Dec 12, 2019
  • Find a way to reduce usage of O/R/U suffixes
    #277 · opened Dec 02, 2019 by Ralf Jung   A-coq C-enhancement T-algebra
    • 0
    updated Dec 02, 2019
  • Create example user library and document library best practices
    #276 · opened Dec 02, 2019 by Robbert Krebbers   A-docs C-enhancement T-style
    • 1
    • 2
    updated Sep 29, 2020
  • use implicit arguments for lemmas in coq_tactics.v   0 of 1 task completed
    #275 · opened Nov 22, 2019 by Paolo G. Giarrusso   A-coq C-enhancement T-proofmode
    • 0
    updated Nov 22, 2019
  • Iris shadows ssreflect new syntax
    #273 · opened Nov 07, 2019 by Paolo G. Giarrusso   A-coq C-bug T-algebra
    • 15
    updated Nov 22, 2019
  • Fix performance regressions in Iris and std++ in Coq 8.10.1 compared to Coq 8.9.0
    #272 · opened Nov 07, 2019 by Robbert Krebbers   A-coq I-performance
    • 14
    updated Feb 12, 2020
  • `iInv`: support tokens that are "framed" around the accessor
    #268 · opened Sep 30, 2019 by Dan Frumin   A-coq C-enhancement T-proofmode
    • 1
    updated Mar 18, 2020
  • Inconsistent order of arguments for `inv_alloc` and `cinv_alloc`.
    #267 · opened Sep 30, 2019 by Dan Frumin   A-coq C-bug T-base_logic T-style
    • 2
    updated Nov 01, 2019
  • Investigate use of "Filtered Unification"
    #264 · opened Aug 31, 2019 by Ralf Jung   A-coq C-project
    • 0
    updated Nov 01, 2019
  • `big_op*_forall` that relate traversals over different structures
    #262 · opened Aug 28, 2019 by Dmitry Khalanskiy   A-coq C-enhancement Good First Issue T-algebra
    • 6
    updated Jan 21, 2020
  • Provide smart `bi` constructor for BIs that are not step-indexed
    #261 · opened Aug 21, 2019 by Robbert Krebbers   A-coq C-enhancement T-bi
    • 1
    • 0
    updated Nov 01, 2019
  • "Exponentiation" for separating conjunctions
    #252 · opened Jul 09, 2019 by Dmitry Khalanskiy   A-coq C-enhancement Good First Issue T-bi
    • 3
    updated Nov 01, 2019
  • Simplification machinery for RA operations
    #251 · opened Jun 24, 2019 by Ralf Jung   A-coq C-project T-algebra
    • 1
    • 1
    updated Apr 06, 2020
  • Add a general lattice RA to Iris
    #244 · opened Jun 12, 2019 by Ralf Jung   A-theory C-project T-algebra
    • 1
    • 9
    updated Dec 10, 2020
  • Avoid type-level aliases for overloading of canonical structures
    #243 · opened Jun 11, 2019 by Robbert Krebbers   A-coq C-enhancement T-algebra
    • 0
    updated Nov 01, 2019
  • "Flattened" introduction patterns for intuitionistic conjunction elimination.
    #241 · opened May 27, 2019 by Dan Frumin   A-coq C-project T-proofmode
    • 2
    updated Nov 01, 2019
  • Documentation for the algebra folder
    #235 · opened Mar 30, 2019 by Robbert Krebbers   A-docs C-enhancement T-algebra
    • 2
    • 1
    updated Nov 01, 2019
  • "expression validity" in WP
    #228 · opened Feb 19, 2019 by Jonas Kastberg   A-theory C-project T-program_logic
    • 19
    updated Nov 01, 2019
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • 6
  • Next