Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
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
yiyunliu pushed to master at yiyunliu/eta-expand-confluence 2025-04-08 01:04:12 -04:00
00f581bcc7 Work on diamond
yiyunliu created branch master in yiyunliu/eta-expand-confluence 2025-04-07 23:37:01 -04:00
yiyunliu pushed to master at yiyunliu/eta-expand-confluence 2025-04-07 23:37:01 -04:00
5cf82dae12 Add syntax spec
yiyunliu created repository yiyunliu/eta-expand-confluence 2025-04-07 23:36:36 -04:00