Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
yiyunliu created pull request yiyunliu/sp-eta-postpone#1 2025-02-06 00:26:40 -05:00
logrelnew
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-06 00:08:12 -05:00
c24cc7c9b0 Finish ST Conv
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 23:56:55 -05:00
64bcf8e9c1 Finish Proj case
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 21:44:41 -05:00
d6a96430f0 Add semantic typing
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 21:28:51 -05:00
55ccc2bc1d Prove the enhanced interpuniv bind inversion principle
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 21:20:44 -05:00
4134fbdada Finish InterpUniv_Join
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 21:14:45 -05:00
76f8c32dad Finish the hard fun case for interpuniv_join
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 20:36:47 -05:00
1997e8bc12 Side step the need for join subst
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 20:06:09 -05:00
7cc6435ea3 Finish most of InterpUniv join
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 18:57:06 -05:00
af224831e4 Finish the injectivity of bind and noconfusion
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 16:52:32 -05:00
e444c8408f Show that sne and bind are not joinable
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 15:48:06 -05:00
0e254c5ac3 Start the proof that joinability preserves meaning
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 14:44:39 -05:00
7f29fe0347 Add induction principle for InterpUniv
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 14:04:51 -05:00
2393cc5103 Finish adequacy ext
yiyunliu created branch logrelnew in yiyunliu/sp-eta-postpone 2025-02-05 13:46:13 -05:00
yiyunliu pushed to logrelnew at yiyunliu/sp-eta-postpone 2025-02-05 13:46:13 -05:00
f83af1241b Merge remote-tracking branch 'origin/logrel' into logrelnew
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