aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Gible.v
Commit message (Expand)AuthorAgeFilesLines
* Annonimize submissiondev/asplosYann Herklotz2023-08-101-1/+1
* Add SMTCoq solver as dependencyYann Herklotz2023-06-211-2/+2
* Prove more admitted theoremsYann Herklotz2023-05-291-0/+10
* Finish abstr_seq_reverse_correct_foldYann Herklotz2023-05-211-0/+11
* Prepare work on evaluability of instructionsYann Herklotz2023-05-191-12/+99
* Change nat to positive in Sat proofYann Herklotz2023-04-271-5/+5
* Finish sem_update_instr finallyYann Herklotz2023-02-121-0/+34
* Work on implementing abstract predicatesYann Herklotz2022-07-191-0/+2
* Add work on abstract predicatesYann Herklotz2022-07-141-0/+3
* Working on scheduling proofYann Herklotz2022-07-041-0/+13
* Update build files for documentationYann Herklotz2022-06-241-3/+3
* Rearrange definitions and create IfConversion templateYann Herklotz2022-06-061-0/+12
* Finish CondElim proof and fix Gible semanticsYann Herklotz2022-06-061-23/+54
* Fix many more lemmasYann Herklotz2022-06-051-0/+10
* Working towards ElimCond proofYann Herklotz2022-06-031-0/+5
* Work on CondElim proofYann Herklotz2022-06-031-0/+20
* Update the Gible semantics with correct terminationYann Herklotz2022-05-311-9/+10
* Rewrite a lot fixing scheduling of GibleYann Herklotz2022-05-271-27/+22
* Translate the base languagesYann Herklotz2022-05-251-0/+595
generated by cgit (git 2.34.1) at 2024-06-26 01:12:41 +0000