Commits · 340b623ded0d240b3efba20581183cdf0ac6975a · AVA / FloVer

23 Feb, 2017 4 commits
- Add changes to proofs, to obtain proper invariants · 340b623d
  Heiko Becker authored Feb 23, 2017
  
  340b623d
- Merge branch 'new_semantics' into translation · 429cb4d0
  Heiko Becker authored Feb 23, 2017
  
  429cb4d0
- Merge branch 'new_semantics' into translation · 6ad313ba
  Heiko Becker authored Feb 23, 2017
  
  6ad313ba
- Add new evaluation semantics to HOL4, without proofs · ae3c6189
  Heiko Becker authored Feb 23, 2017
  
  ae3c6189
21 Feb, 2017 13 commits
- Move out REAL_TYPE from transScript.sml · 80f0d0c4
  Magnus Myreen authored Feb 21, 2017
  
  80f0d0c4
- Minor modification to iv validation and translation file · 139aea84
  Heiko Becker authored Feb 21, 2017
  
  139aea84
- add negation · 20c18685
  Heiko Becker authored Feb 21, 2017
  
  20c18685
- Prove addition and subtraction equivalent on pair type · 39e3b4ee
  Heiko Becker authored Feb 21, 2017
  
  39e3b4ee
- Merge branch 'translation' of gitlab.mpi-sws.org:hbecker/daisy into translation · 479abb64
  Heiko Becker authored Feb 21, 2017
  
  479abb64
- Fix? submodule · a2b8f5f8
  Heiko Becker authored Feb 21, 2017
  
  a2b8f5f8
- Reconfigure submodule for CakeML · f4892f07
  Heiko Becker authored Feb 21, 2017
  
  f4892f07
- Update cake-ml --> cakeml in Holmakefile · b1baa092
  Magnus Myreen authored Feb 21, 2017
  
  b1baa092
- Update submodule file · e6694dfa
  Heiko Becker authored Feb 21, 2017
  
  e6694dfa
- Merge branch 'translation' of gitlab.mpi-sws.org:hbecker/daisy into translation · c5c810f2
  Heiko Becker authored Feb 21, 2017
  
  c5c810f2
- Update cakeml to latest version of branch · 93ad28eb
  Heiko Becker authored Feb 21, 2017
  
  93ad28eb
- Remove last cheat from transTheory and add realax$< · 2d439e9a
  Magnus Myreen authored Feb 21, 2017
  
  2d439e9a
- Get hol4 dir to build without Holmake --fast · 61374236
  Magnus Myreen authored Feb 21, 2017
  
  61374236
20 Feb, 2017 9 commits
- Prove translation lemmas about inv · 53c5964c
  Magnus Myreen authored Feb 20, 2017
  
  53c5964c
- Move cake-ml submodule to daisy branch · d305a5e5
  Heiko Becker authored Feb 20, 2017
  
  d305a5e5
- Merge branch 'translation' of gitlab.mpi-sws.org:hbecker/daisy into translation · 8c00929e
  Heiko Becker authored Feb 20, 2017
  
  8c00929e
- Fix paths · 48c905ac
  Heiko Becker authored Feb 20, 2017
  
  48c905ac
- Prove lemmas about real_of_int · 9d2c3129
  Magnus Myreen authored Feb 20, 2017
  
  9d2c3129
- CakeML now a submodule, run git submodule init to download · f3e945c0
  Heiko Becker authored Feb 20, 2017
  
  f3e945c0
- Add missing transScript.sml · 5073e8ed
  Magnus Myreen authored Feb 20, 2017
  
  5073e8ed
- Get files to build with Holmake --fast · 1ac6e8a8
  Magnus Myreen authored Feb 20, 2017
  
  1ac6e8a8
- Start on translation · d9c94b1e
  Magnus Myreen authored Feb 20, 2017
  
  d9c94b1e
19 Feb, 2017 1 commit

Rework evaluation semantics to not be arguing about precondition, make this... · df325c1a

Heiko Becker authored Feb 19, 2017

Rework evaluation semantics to not be arguing about precondition, make this explicit in the theorem, that we assume it. Admitted proofs that are obvious

df325c1a

18 Feb, 2017 2 commits
- Show substitution properties for ssa programs · abe26619
  Heiko Becker authored Feb 18, 2017
  
  abe26619
- Prove all necessary properties for new semantics · 3747df48
  Heiko Becker authored Feb 18, 2017
  
  3747df48
17 Feb, 2017 1 commit
- Rework expression and cmd semantics for removing parameters distinction · 3bf112d9
  Heiko Becker authored Feb 17, 2017
  
  3bf112d9
13 Feb, 2017 8 commits
- Same simplification in HOL4 · bd83c45a
  Heiko Becker authored Feb 13, 2017
  
  bd83c45a
- Simplify coq error bound proof · 95dac28a
  Heiko Becker authored Feb 13, 2017
  
  95dac28a
- Add some documentation about env approx relation · 7ab24f19
  Heiko Becker authored Feb 13, 2017
  
  7ab24f19
- Merge remote-tracking branch 'ava_daisy/master' · 2d655ab1
  Heiko Becker authored Feb 13, 2017
  
  2d655ab1
- Merge branch 'letBindings' · 57477218
  Heiko Becker authored Feb 13, 2017
  
  57477218
- Remove not yet used lemmas from ssaPrgs.v to get a clean state before sending next merge request · 752ac724
  Heiko Becker authored Feb 13, 2017
  
  752ac724
- Update development to Coq 8.6 · d3d60c41
  Heiko Becker authored Feb 13, 2017
  
  d3d60c41
- Add ssa soundness checker · 7f633e09
  Heiko Becker authored Feb 13, 2017
  
  7f633e09
08 Feb, 2017 2 commits
- Simplify some coq proofs · 2e65b5a9
  Heiko Becker authored Feb 08, 2017
  
  2e65b5a9
- Show soundness of let Bindings in HOL4 · de4bf712
  Heiko Becker authored Feb 08, 2017
  
  de4bf712