aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* | Add more legible names to variablesYann Herklotz2021-02-121-1/+17
* | Add signed and unsigned divisionYann Herklotz2021-02-122-0/+339
* | Add temporary fixes to get everything to compileYann Herklotz2021-02-129-45/+514
* | Fix state generation for if-conversionYann Herklotz2021-02-034-14/+21
* | Fix scheduling for if-conversionYann Herklotz2021-02-031-14/+90
* | Add predicated values and instructionsYann Herklotz2021-02-027-41/+92
* | Add if conversion passYann Herklotz2021-02-021-3/+65
* | Add if conversion passYann Herklotz2021-02-021-0/+32
* | Add Vrange and predicatesYann Herklotz2021-02-028-66/+95
* | Fix OCaml files for compilationYann Herklotz2021-01-314-92/+94
* | Fix compilation of CoqYann Herklotz2021-01-302-19/+48
* | Fix proofs with better defined equalityYann Herklotz2021-01-302-31/+57
* | Fix definitions of proofs some moreYann Herklotz2021-01-294-106/+162
* | Fix the proof for RTLPargenYann Herklotz2021-01-291-32/+33
* | Fix HTLPargen and RTLPargenYann Herklotz2021-01-292-56/+178
* | Refactoring RTLBlock and RTLParYann Herklotz2021-01-293-297/+205
* | Finish all proofs except executing basic blocksYann Herklotz2021-01-271-1/+4
* | Add more proofs for RTLPargen correctnessYann Herklotz2021-01-273-26/+97
* | Add basic block matching and proofYann Herklotz2021-01-261-3/+78
* | Remove the schedule oracleYann Herklotz2021-01-262-518/+515
* | Add an inductive to enter the basic blockYann Herklotz2021-01-261-3/+3
* | Use basic blocks in context to help proofYann Herklotz2021-01-261-11/+15
* | Add destruction to context match expressionsYann Herklotz2021-01-261-2/+5
* | Remove match on basic blocksYann Herklotz2021-01-231-6/+0
* | Add match_states for RTLPargen proofYann Herklotz2021-01-223-4/+78
* | Fix imports to remove warnings when compilingYann Herklotz2021-01-227-49/+101
* | Update documentationYann Herklotz2021-01-221-0/+0
* | Fix types with new changes in RTLBlockYann Herklotz2021-01-224-91/+133
* | Define RTLPar semanticsYann Herklotz2021-01-222-172/+85
* | Add top-level semantics definitionsYann Herklotz2021-01-221-0/+17
* | Update documentationYann Herklotz2021-01-221-0/+0
* | Add semantics for RTLBlockYann Herklotz2021-01-222-12/+68
* | Merge branch 'master' into developYann Herklotz2021-01-225-84/+172
|\ \
| * | Add change log and rename READMEYann Herklotz2021-01-223-84/+169
| * | Add documentation repository as submoduleYann Herklotz2021-01-222-0/+3
* | | Add semantics for RTLBlockInstr and RTLBlockYann Herklotz2021-01-222-22/+72
* | | Share code between RTLBlock and ParYann Herklotz2021-01-214-149/+314
* | | Fix imports in Coq modulesYann Herklotz2021-01-217-116/+162
* | | Improve expression equality proofYann Herklotz2021-01-211-57/+17
|/ /
* | Remove github pages from repositoryYann Herklotz2021-01-202-30/+1
* | Delete documents folder and move to separate repositoryYann Herklotz2021-01-20123-529786/+0
* | Fix links on main pageYann Herklotz2021-01-151-1/+1
* | More tweaks to the CSSYann Herklotz2021-01-153-5/+5
* | Increase font sizeYann Herklotz2021-01-151-9/+9
* | Actually update cssYann Herklotz2021-01-151-94/+174
* | Fix website build by adding correct pathYann Herklotz2021-01-151-1/+1
* | Update websiteYann Herklotz2021-01-154-6/+6
* | Fix inconsistencies in websiteYann Herklotz2021-01-152-7/+4
* | Translate from RTLBlock to RTLParYann Herklotz2021-01-131-201/+39
* | Correct translation of scheduling with oracle checkYann Herklotz2021-01-131-4/+53