Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
7
 Projects Packages Public activity Starred repositories
yiyunliu pushed to logrel at yiyunliu/sp-eta-postpone 2025-02-04 22:14:39 -05:00
38a0416b2c Add a constant to avoid kripke LR
yiyunliu created branch logrel in yiyunliu/sp-eta-postpone 2025-02-04 22:03:34 -05:00
yiyunliu pushed to logrel at yiyunliu/sp-eta-postpone 2025-02-04 22:03:34 -05:00
e923194e3d Finish adding pi and sigma types
d9b5ef1267 Refactor the impossible case proof
Compare 2 commits »
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-03 22:47:58 -05:00
bd7af7b297 Add README file
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-03 14:55:50 -05:00
84cd0715c7 Prove structural properties of DJoin
3d42581bbe Finish the confluence proof
f3f3991b02 Finish rred standardization
a0c20851fe Prove confluence of beta
cf31e6d285 Finish the confluence proof of ered
Compare 8 commits »
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-03 14:55:40 -05:00
84cd0715c7 Prove structural properties of DJoin
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-03 14:23:19 -05:00
3d42581bbe Finish the confluence proof
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-03 12:17:02 -05:00
f3f3991b02 Finish rred standardization
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-02 21:57:49 -05:00
a0c20851fe Prove confluence of beta
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-02 20:48:54 -05:00
cf31e6d285 Finish the confluence proof of ered
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-02 20:21:14 -05:00
376fce619c Save progress
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-02 20:08:47 -05:00
5624415bc9 Finish antirenaming for injective rens
yiyunliu created branch antirenaming in yiyunliu/sp-eta-postpone 2025-02-02 19:42:59 -05:00
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-02 19:42:59 -05:00
6cc3a65163 Discharge one case of antirenaming using injective renaming
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-31 21:57:11 -05:00
ecb50f1ab7 Add comment about the antirenaming proof
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-31 21:46:05 -05:00
d2cd3105c7 stuck on antirenaming because of scoped syntax
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-31 20:54:43 -05:00
580e3a8251 Prove that ered is strongly normalizing
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-31 20:12:39 -05:00
f57e10be93 Finish extracting leftmost-outermost red from sn
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-31 17:32:48 -05:00
571779a4dd Fix name change errors for EPar
5dd3428e2b Merge remote-tracking branch 'forgejo/nonessential'
47473fd3cd Minor
Compare 3 commits »
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-31 16:30:09 -05:00
47473fd3cd Minor