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