Commits · appendix-1 · Thomas Somers / Iris · GitLab

Snippets Groups Projects

Jul 08, 2014
- update README · d86b955f
  Ralf Jung authored 10 years ago
  
  View commits for tag appendix-1 appendix-1
  
  d86b955f
- add coq README · 79bf9711
  Ralf Jung authored 10 years ago
  
  79bf9711
Jul 06, 2014
- Finished with the formalisation. · c7b1b954
  Filip Sieczkowski authored 10 years ago
  
  c7b1b954
- Finished the proof of Ralf's statement of soundness. · 75cc5c91
  Filip Sieczkowski authored 10 years ago
  
  75cc5c91
- Merge branch 'master' of git.fp.mpi-sws.org:nowbook · f95ee313
  Filip Sieczkowski authored 10 years ago
  
  f95ee313
- Fixed the def'n of wp to include a frame over mask, fixed all the · d96b1624
  Filip Sieczkowski authored 10 years ago
  d96b1624
- add and almost prove the soundness (adequacy) theorem as it appears in the writeup · 23b0e16b
  Ralf Jung authored 10 years ago
  
  23b0e16b
- add makefile to coq-ho · 688d3287
  Ralf Jung authored 10 years ago
  
  688d3287
Jul 05, 2014
- Added "timeless" assertion and the view-shift rule. · 02a753f4
  Filip Sieczkowski authored 10 years ago
  
  02a753f4
- Soundness/adequacy proved. · fc83f26a
  Filip Sieczkowski authored 10 years ago
  
  fc83f26a
Jun 22, 2014
- fix vsOpen, vsClose, vsGhostUpd · afa3f82d
  Ralf Jung authored 10 years ago
  
  afa3f82d
Jun 20, 2014
- update to the current set of axioms · 876e9848
  Ralf Jung authored 10 years ago
  
  876e9848
- get rid of erasures, use exclusive state ownership instead · 97c0889d
  Ralf Jung authored 10 years ago
  
  97c0889d
- Define a monoid for exclusive ownership · 3fe8c615
  Ralf Jung authored 10 years ago
  3fe8c615
- sanitize emacs · 25bcec19
  Ralf Jung authored 10 years ago
  
  25bcec19
Jun 06, 2014
- The lemma about ghost state update. · a1ae9e52
  Filip Sieczkowski authored 11 years ago
  
  a1ae9e52
Jun 05, 2014
- Proved the Hoare triple rules, except the one about timeless props. · 594a1dd0
  Filip Sieczkowski authored 11 years ago
  
  594a1dd0
Jun 04, 2014
- Simplified some def's, proved more lemmas (box, composition of ghosts, · a01925c4
  Filip Sieczkowski authored 11 years ago
  a01925c4
Jun 03, 2014
- Propositions are now uniform predicates over monoid elements (not 0); · 0de5b6a9
  Filip Sieczkowski authored 11 years ago
  0de5b6a9
May 31, 2014
- Hoare triples defined. · 8688ed6e
  Filip Sieczkowski authored 11 years ago
  
  8688ed6e
May 29, 2014
- Fixed definition of erasure, proved some properties of view-shifts · e24ee0af
  Filip Sieczkowski authored 11 years ago
  e24ee0af
May 28, 2014
- Simplified definitions by taking UPreds over option T, where T is a · 5517602d
  Filip Sieczkowski authored 11 years ago
  5517602d
- Notations, erasure and view-shift definitions. · ddaf548e
  Filip Sieczkowski authored 11 years ago
  
  ddaf548e
- Internal equality, invariants & ownership. Fixed the visibility of R.res · 368a2f5c
  Filip Sieczkowski authored 11 years ago
  368a2f5c
- Finished preparing the iris setup. The basic rules for BI-logic and · cea1110f
  Filip Sieczkowski authored 11 years ago
  cea1110f
- Added a library for solving recursive domain equations. · 3d69aaa0
  Filip Sieczkowski authored 11 years ago
  
  3d69aaa0