Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • I iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 0
    • Issues 0
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Jonas Kastberg
  • iris
  • Repository
Switch branch/tag
  • iris-coq
  • theories
  • bi
  • derived_connectives.v
Find file BlameHistoryPermalink
  • Ralf Jung's avatar
    Make uPred itself independent of BI interface and just prove primitive laws (like in master branch) · b56835d0
    Ralf Jung authored May 23, 2018
    The BI interface is then instantiated using these laws.  In particular, this
    shows that the rules we claim to be admissible actually are.
    b56835d0