Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-10 16:22:46 -04:00
e278c6eaef Define salgo_dom
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-10 15:35:48 -04:00
4cbd2ac0fd Save
yiyunliu created branch cleanup in yiyunliu/sp-eta-postpone 2025-03-10 14:31:30 -04:00
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-10 14:31:30 -04:00
849d19708e Add new definition of algo_dom
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-03-06 20:42:49 -05:00
437c97455e Finish the soundness and completeness proof of the subtyping algorithm
fe52d78ec5 Start the soundness proof for check_sub
6f154cc9c6 Add stub for check_sub
96b3139726 Prove termination
Compare 4 commits »
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-06 20:42:24 -05:00
437c97455e Finish the soundness and completeness proof of the subtyping algorithm
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-06 19:21:03 -05:00
fe52d78ec5 Start the soundness proof for check_sub
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-06 16:20:38 -05:00
6f154cc9c6 Add stub for check_sub
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-06 15:40:02 -05:00
96b3139726 Prove termination
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-03-05 00:22:12 -05:00
b29d567ef0 Add termination
c4f01d7dfc Update the correctness proof of the computable function
c1ff0ae145 Add check_equal_conf case
c05bd10016 Turn off auto equations generation because it produces poor lemmas
68cc482479 Fix the correctness proof
Compare 24 commits »
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-05 00:18:33 -05:00
b29d567ef0 Add termination
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 23:48:57 -05:00
c4f01d7dfc Update the correctness proof of the computable function
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 23:22:52 -05:00
c1ff0ae145 Add check_equal_conf case
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 22:44:04 -05:00
c05bd10016 Turn off auto equations generation because it produces poor lemmas
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 22:30:32 -05:00
68cc482479 Fix the correctness proof
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 22:28:25 -05:00
a23be7f9b5 Simplify the definition of algo_dom
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 22:20:24 -05:00
5087b8c6ce Add new definition of eq_view
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 21:48:08 -05:00
dcd4465310 Finish the proof of completeness for the algorithm
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 00:40:14 -05:00
b9b6899764 Half way done with check_equal_complete
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-04 00:27:53 -05:00
0060d3fb86 Factor out the rewriting lemmas