Commits · cpp · MICHELLAND Sébastien / itree-ai · GitLab

Mentions légales du service

Snippets Groups Projects

GitLab upgrade completed. Current version is 17.11.4.

Sep 19, 2023
- CPP submission snapshot · 03057697
  MICHELLAND Sébastien authored 1 year ago
  
  03057697
- Updaet readme · e6398cde
  Yannick Zakowski authored 1 year ago
  
  e6398cde
Sep 18, 2023
- Print assumptions · 43a7536d
  Yannick Zakowski authored 1 year ago
  
  43a7536d
- prove last remaining admits · d984c917
  MICHELLAND Sébastien authored 1 year ago
  
  d984c917
Sep 15, 2023
- better parameter order for syntactic soundness theorems · d30e2711
  MICHELLAND Sébastien authored 1 year ago
  
  d30e2711
Sep 14, 2023
- rename sound_void1 -> sound_unfold · 07a7aa93
  MICHELLAND Sébastien authored 1 year ago
  
  07a7aa93
- complete example + simplified imp notations · 3cb45686
  MICHELLAND Sébastien authored 1 year ago
  
  3cb45686
- extract to ImpArithFail with intervals · 934ea441
  MICHELLAND Sébastien authored 1 year ago
  
  934ea441
Sep 13, 2023
- ImpArithFail now uses intervals · f64d01d5
  MICHELLAND Sébastien authored 1 year ago
  
  f64d01d5
- test cases are now somewhat useable · 942c2539
  MICHELLAND Sébastien authored 1 year ago
  
  942c2539
- repair extraction · df04bc81
  MICHELLAND Sébastien authored 1 year ago
  
  df04bc81
- do not join in failT sequence when first half doesn't fail... · ec79937c
  MICHELLAND Sébastien authored 1 year ago
  ec79937c
Sep 12, 2023
- rename aflow function compile -> unfold · 694563fe
  MICHELLAND Sébastien authored 1 year ago
  
  694563fe
Sep 09, 2023
- some cleanup, including Imp.v · 56e82c0f
  MICHELLAND Sébastien authored 1 year ago
  
  56e82c0f
- BEHOLD, failT support in all its glory! · 773de118
  MICHELLAND Sébastien authored 1 year ago
  
  773de118
- failT basically preserved + noflow no longer needed · 7f0be10a
  MICHELLAND Sébastien authored 1 year ago
  
  7f0be10a
Sep 08, 2023
- break down SoundBisim · e04b8a99
  MICHELLAND Sébastien authored 1 year ago
  
  e04b8a99
- sequence combinator (!) · bd346ea1
  MICHELLAND Sébastien authored 1 year ago
  
  bd346ea1
- prove lattice measure theorems, once and for all · 7c8d28c6
  MICHELLAND Sébastien authored 1 year ago
  
  7c8d28c6
Sep 07, 2023
- nits · 94e4bfc7
  Yannick Zakowski authored 1 year ago
  
  94e4bfc7
- wip · ee9dedc5
  Yannick Zakowski authored 1 year ago
  
  ee9dedc5
- wip · 8748d7fe
  Yannick Zakowski authored 1 year ago
  
  8748d7fe
- Add lemmas needed to exploit ~ y ⊆ x in map widening proof · b10fa881
  MICHELLAND Sébastien authored 1 year ago
  
  b10fa881
Sep 06, 2023
- fix map_measure_le · 1751a87a
  Yannick Zakowski authored 1 year ago
  
  1751a87a
- From one admit to five admits, magic · 6cc354bb
  Yannick Zakowski authored 1 year ago
  
  6cc354bb
- fix admits in latticevec · ffd3b666
  Yannick Zakowski authored 1 year ago
  
  ffd3b666
- use Typeˣ instead of Lattice instances in defs/theorems · 9f648640
  MICHELLAND Sébastien authored 1 year ago
  9f648640
- add AbstractMonad.v from the type_sharp branch · 351b9b5d
  MICHELLAND Sébastien authored 1 year ago
  351b9b5d
- rename Prog -> aflow, 2/2 · 47ed0e13
  MICHELLAND Sébastien authored 1 year ago
  
  47ed0e13
- rename Prog -> aflow, 1/2 · 67e283ef
  MICHELLAND Sébastien authored 1 year ago
  
  67e283ef
Sep 05, 2023
- organize case-related lemmas and prove Asm · df2756c9
  MICHELLAND Sébastien authored 1 year ago
  
  df2756c9
- Imp/ImpArith defined and proven · ca3f6ce5
  MICHELLAND Sébastien authored 1 year ago
  
  ca3f6ce5
- propagate type-heterogeneous fixpoint to Interpretation.v · a142d54c
  MICHELLAND Sébastien authored 1 year ago
  
  a142d54c
- tpye-heterogeneous fixpoint · 2e6da79f
  MICHELLAND Sébastien authored 1 year ago
  2e6da79f
Sep 04, 2023
- propagate cleaner concrete loops to Interpretation.v · 78b218cf
  MICHELLAND Sébastien authored 1 year ago
  78b218cf
- fix incorrectly-designed loop combinator result · 470431ac
  MICHELLAND Sébastien authored 1 year ago
  470431ac
- remove SoundConditionalPath, which does *NOT* work · f535cbb9
  MICHELLAND Sébastien authored 1 year ago
  f535cbb9
Apr 20, 2023
- fix warnings 8.17 · dfb75ef7
  Yannick Zakowski authored 2 years ago
  
  dfb75ef7
- propagate do/while changes + error-carrying interp_fail · d9f786dc
  MICHELLAND Sébastien authored 2 years ago
  
  d9f786dc
Apr 13, 2023
- while: fail-capable and boolean-based while combinator · 1a72cdfb
  MICHELLAND Sébastien authored 2 years ago
  
  1a72cdfb