Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
7
 Projects Packages Public activity Starred repositories
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-04-28 17:33:52 -04:00
fe88b519a9 Change woodpecker branch name
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-04-28 17:33:09 -04:00
d7207c6532 Add ci
yiyunliu pushed to master at yiyunliu/info-page 2025-04-20 22:00:43 -04:00
8f5425ac42 Add README.md
c252582a4e Add update about mastodon
Compare 2 commits »
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-04-19 17:46:01 -04:00
0e04a7076b Prove PairEta
8e083aad4b Add renaming_comp
2b92845e3e Add E_AppEta
43daff1b27 Fix soundness
d9282fb815 Finish preservation
Compare 8 commits »
yiyunliu pushed to ext-rep at yiyunliu/sp-eta-postpone 2025-04-19 00:24:14 -04:00
0e04a7076b Prove PairEta
yiyunliu pushed to ext-rep at yiyunliu/sp-eta-postpone 2025-04-19 00:07:49 -04:00
8e083aad4b Add renaming_comp
yiyunliu pushed to ext-rep at yiyunliu/sp-eta-postpone 2025-04-18 16:38:33 -04:00
2b92845e3e Add E_AppEta
yiyunliu pushed to ext-rep at yiyunliu/sp-eta-postpone 2025-04-18 15:46:07 -04:00
43daff1b27 Fix soundness
yiyunliu pushed to ext-rep at yiyunliu/sp-eta-postpone 2025-04-18 15:46:02 -04:00
d9282fb815 Finish preservation
yiyunliu pushed to ext-rep at yiyunliu/sp-eta-postpone 2025-04-18 14:14:43 -04:00
87b84794b4 Fix structural rules
yiyunliu pushed to ext-rep at yiyunliu/sp-eta-postpone 2025-04-17 16:42:55 -04:00
7c985fa58e Minor
yiyunliu created branch ext-rep in yiyunliu/sp-eta-postpone 2025-04-17 15:23:01 -04:00
yiyunliu pushed to ext-rep at yiyunliu/sp-eta-postpone 2025-04-17 15:23:01 -04:00
e1fc6b609d Add the extensional representation of pair&abs equality rules
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-04-17 15:16:05 -04:00
a367591e9a Add extensional version of pair equality rules
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-04-17 15:07:28 -04:00
ef8feb63c3 Redefine semantic context well-formedness as an inductive
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-04-16 23:57:07 -04:00
4b2bbeea6f Add SE_FunExt
yiyunliu pushed to master at yiyunliu/eta-expand-confluence 2025-04-13 21:46:26 -04:00
5dbde6d45f Add alternative direct commutativity proof
yiyunliu pushed to master at yiyunliu/eta-expand-confluence 2025-04-13 21:00:22 -04:00
593f50ebaa Attempt to directly show commutation of parallel betaeta
yiyunliu pushed to master at yiyunliu/eta-expand-confluence 2025-04-08 22:25:24 -04:00
21bb2944a3 Restructure proof to use hindley rosen
yiyunliu pushed to master at yiyunliu/eta-expand-confluence 2025-04-08 16:53:53 -04:00
9d3c3726dd The proof is miserable