_CoqProject · b56835d0dcec6691d330c8b0d1bc40369f417c34 · Abel Nieto / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

6 years ago
b56835d0
Make uPred itself independent of BI interface and just prove primitive laws (like in master branch) · b56835d0
Ralf Jung authored 6 years ago
```
The BI interface is then instantiated using these laws.  In particular, this
shows that the rules we claim to be admissible actually are.
```
b56835d0

History
Make uPred itself independent of BI interface and just prove primitive laws (like in master branch)
Ralf Jung authored 6 years ago
```
The BI interface is then instantiated using these laws.  In particular, this
shows that the rules we claim to be admissible actually are.
```