Commits · 0294692b0896bc6538790b369d601ab38b6ae4c4 · FP / Stacked Borrows Coq

08 Jul, 2019 1 commit
- split refl_step; WIP: pure steps refl · 0294692b
  Hai Dang authored Jul 08, 2019
  
  0294692b
07 Jul, 2019 28 commits
- add rule for proj · cbbe8be3
  Hai Dang authored Jul 08, 2019
  
  cbbe8be3
- fix function results; add lemma for var · a063d2d6
  Hai Dang authored Jul 08, 2019
  
  a063d2d6
- fancy expression induction · cad19e71
  Ralf Jung authored Jul 08, 2019
  
  cad19e71
- stub out all cases, and comment · 15332a78
  Ralf Jung authored Jul 07, 2019
  
  15332a78
- functions take and return results; breaking simple.v and refl.v · 28168cc9
  Hai Dang authored Jul 07, 2019
  
  28168cc9
- Merge branch 'master' of gitlab.mpi-sws.org:FP/stacked-borrows · 92a15853
  Ralf Jung authored Jul 07, 2019
  
  92a15853
- substitution stuff · 1e25cde7
  Ralf Jung authored Jul 07, 2019
  
  1e25cde7
- fix index for values · 94b59314
  Hai Dang authored Jul 07, 2019
  
  94b59314
- simple write local · 46dc5239
  Hai Dang authored Jul 07, 2019
  
  46dc5239
- write locals · dd880389
  Hai Dang authored Jul 07, 2019
  
  dd880389
- towards refl induction · 4be2ffb7
  Ralf Jung authored Jul 07, 2019
  
  4be2ffb7
- program WF · 7d18706e
  Ralf Jung authored Jul 07, 2019
  
  7d18706e
- well-formedness · f9c9f0a8
  Ralf Jung authored Jul 07, 2019
  
  f9c9f0a8
- per-fun refl is enough · 80572367
  Ralf Jung authored Jul 07, 2019
  
  80572367
- tie some global things together · 85a73e08
  Ralf Jung authored Jul 07, 2019
  
  85a73e08
- tweak simple rules · 0bca5190
  Ralf Jung authored Jul 07, 2019
  
  0bca5190
- Merge branch 'master' of gitlab.mpi-sws.org:FP/stacked-borrows · bcb97508
  Ralf Jung authored Jul 07, 2019
  
  bcb97508
- show that vrel etc are persistent · 8f14a12f
  Ralf Jung authored Jul 07, 2019
  
  8f14a12f
- WIP: sim_local_funs_insert · aec339fd
  Hai Dang authored Jul 07, 2019
  
  aec339fd
- Merge branch 'master' of gitlab.mpi-sws.org:FP/stacked-borrows · 41993800
  Hai Dang authored Jul 07, 2019
  
  41993800
- add viewshift · b5203edd
  Hai Dang authored Jul 07, 2019
  
  b5203edd
- ex1: better names · 63dfd1ef
  Ralf Jung authored Jul 07, 2019
  
  63dfd1ef
- some global glue · 40ee246b
  Ralf Jung authored Jul 07, 2019
  
  40ee246b
- add funs_lookup assumption to example proof · 7f4bd80f
  Ralf Jung authored Jul 07, 2019
  
  7f4bd80f
- fix syntactic condition on lookup of function tables · 78a6143e
  Hai Dang authored Jul 07, 2019
  
  78a6143e
- give a name to our decidability assumotion and show that it holds classically · 8814e3ea
  Ralf Jung authored Jul 07, 2019
  
  8814e3ea
- fix end_call_sat · f77ae9f0
  Hai Dang authored Jul 07, 2019
  
  f77ae9f0
- fix step_over_call · 59e4404f
  Hai Dang authored Jul 07, 2019
  
  59e4404f
06 Jul, 2019 11 commits
- fix step_over_call and program · ccfc5429
  Hai Dang authored Jul 07, 2019
  
  ccfc5429
- connect things a bit · 4f730067
  Ralf Jung authored Jul 07, 2019
  
  4f730067
- Merge branch 'master' of gitlab.mpi-sws.org:FP/stacked-borrows · eaf2676c
  Ralf Jung authored Jul 07, 2019
  
  eaf2676c
- step over call · e2e3e1d9
  Ralf Jung authored Jul 07, 2019
  
  e2e3e1d9
- fix local inv · 07045249
  Hai Dang authored Jul 07, 2019
  
  07045249
- fix call statement, remove unused lemmas, WIP fixing local var inv · e2ea498c
  Hai Dang authored Jul 07, 2019
  
  e2ea498c
- state a local retag lemma · 42fe994a
  Ralf Jung authored Jul 07, 2019
  
  42fe994a
- simple rule for writes, and some res automation · 5d7ad1d1
  Ralf Jung authored Jul 06, 2019
  
  5d7ad1d1
- let-lemmas for simple sim · dd28723e
  Ralf Jung authored Jul 06, 2019
  
  dd28723e
- make tactics work for simple sim · aaa597f0
  Ralf Jung authored Jul 06, 2019
  
  aaa597f0
- simplified sim relation that does not track the entire physical state, just the call id stacks · 8abdd6bc
  Ralf Jung authored Jul 06, 2019
  
  8abdd6bc