aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GibleSeq.v
Commit message (Expand)AuthorAgeFilesLines
* Annonimize submissiondev/asplosYann Herklotz2023-08-101-1/+1
* Finish max predicate proofYann Herklotz2023-05-281-1/+78
* Finish abstr_seq_reverse_correct_foldYann Herklotz2023-05-211-0/+18
* Prove abstr_fold_correct top-downYann Herklotz2023-01-291-0/+5
* Clean up proofsYann Herklotz2022-10-111-1/+1
* Working on scheduling proofYann Herklotz2022-07-041-0/+62
* Finish DeadBlocksproofYann Herklotz2022-07-011-0/+49
* Update proofYann Herklotz2022-06-301-5/+10
* Work on if-conversion proofYann Herklotz2022-06-281-0/+63
* Rearrange definitions and create IfConversion templateYann Herklotz2022-06-061-0/+59
* Work on CondElim proofYann Herklotz2022-06-031-1/+1
* Fix GibleSeqgenproof with new semanticsYann Herklotz2022-05-311-0/+9
* Rewrite a lot fixing scheduling of GibleYann Herklotz2022-05-271-13/+6
* Add new block generation for GibleYann Herklotz2022-05-261-0/+1
* Translate the base languagesYann Herklotz2022-05-251-0/+70