index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
backends
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2023-06-19
Further simplify the proofs in Diverge.lean
Son Ho
1
-122
/
+151
2023-06-19
Make progress on making the proofs in Diverge more systematic
Son Ho
1
-8
/
+252
2023-06-18
Make minor modifications
Son Ho
2
-3
/
+3
2023-06-14
Make minor modifications
Son Ho
2
-6
/
+26
2023-06-13
Find sufficient validity criteria for Diverge.lean
Son Ho
1
-41
/
+309
2023-06-09
Start working on extrinsic proofs of termination
Son Ho
4
-7
/
+232
2023-06-09
Reorganize a bit the Lean library
Son Ho
4
-22
/
+36
2023-06-06
Remove the sorries from Primitives.lean
Son Ho
2
-65
/
+120
2023-06-04
Add a comment
Son Ho
1
-3
/
+7
2023-06-04
Update the HOL4 proofs for the last *release* version of HOL4
Son Ho
3
-145
/
+137
2023-06-04
Start setting up the Nix derivation for HOL4
Son Ho
2
-1
/
+9
2023-06-04
Simplify a proof
Son Ho
1
-12
/
+6
2023-06-04
Remove some obsolete files from the HOL4 backend
Son Ho
4
-3302
/
+0
2023-06-04
Finish the proofs of the hashmap
Son Ho
5
-9
/
+98
2023-06-04
Make progress on the proofs of the hash map
Son Ho
5
-2
/
+180
2023-06-04
Make good progress on the proofs of the hashmap in HOL4
Son Ho
6
-18
/
+155
2023-06-04
Make the theorems used by the progress tactic persistent
Son Ho
8
-186
/
+285
2023-06-04
Commit saveThmsLib.sig
Son Ho
1
-0
/
+46
2023-06-04
Improve the parsing for divDefLib
Son Ho
1
-1
/
+91
2023-06-04
Fix some minor issues
Son Ho
2
-41
/
+49
2023-06-04
Make progress on the HOL4 backend
Son Ho
2
-42
/
+298
2023-06-04
Make progress on extracting the HOL4 files
Son Ho
2
-2
/
+216
2023-06-04
Make the unfolding theorems collection from evalLib persistent
Son Ho
9
-242
/
+222
2023-06-04
Make minor modifications
Son Ho
1
-5
/
+11
2023-06-04
Start working on saveThmsLib
Son Ho
1
-0
/
+190
2023-06-04
Commit evalLib
Son Ho
2
-0
/
+170
2023-06-04
Update the definitions of mk_vec and vec_insert_back
Son Ho
2
-21
/
+71
2023-06-04
Cleanup a bit the HOL4 backend and implement eval_conv
Son Ho
14
-56
/
+238
2023-06-04
Make good progress on generating code for HOL4
Son Ho
3
-123
/
+736
2023-06-04
Make a minor modification
Son Ho
1
-3
/
+5
2023-06-04
Introduce fix_exec, an executable version of fix
Son Ho
5
-13
/
+90
2023-06-04
Make minor modifications
Son Ho
2
-8
/
+35
2023-06-04
Make minor modifications to divDefLib
Son Ho
2
-60
/
+65
2023-06-04
Fix minor issues
Son Ho
3
-12
/
+508
2023-06-04
Fix minor issues
Son Ho
2
-6
/
+17
2023-06-04
Do more cleanup
Son Ho
2
-1222
/
+0
2023-06-04
Cleanup the files of the HOL4 backend
Son Ho
16
-3080
/
+2938
2023-06-04
Reimplement DefineDiv with the new fixed point operator
Son Ho
3
-2
/
+1249
2023-06-04
Write some tests for divDefProto2Script.sml
Son Ho
2
-84
/
+214
2023-06-04
Update divDefProto2Script.sml
Son Ho
1
-55
/
+16
2023-06-04
Write a prototype definition using the general fixed-point combinator
Son Ho
2
-510
/
+417
2023-06-04
Start working on more general fixed-point combinators
Son Ho
3
-0
/
+904
2023-06-04
Cleanup divDefProtoScript
Son Ho
2
-523
/
+12
2023-06-04
Improve the performance of dependent rewrites by using nets
Son Ho
2
-58
/
+120
2023-06-04
Make more proofs about the hashmap proto
Son Ho
5
-4
/
+225
2023-06-04
Update the hashmap proofs and fix some tactics
Son Ho
5
-46
/
+300
2023-06-04
Start working on a version of divDefLib which uses fixed point combinators
Son Ho
2
-0
/
+983
2023-06-04
Cleanup a bit and reorganize
Son Ho
6
-90
/
+577
2023-06-04
Make minor modifications
Son Ho
1
-0
/
+26
2023-06-04
Fix minor bugs in divDefLib.sml
Son Ho
1
-28
/
+134
[next]