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-02-06 13:53:21 -05:00
286ceeed39 Need to extend the notion of semwt to cover arbitrarily scoped terms
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 13:21:45 -05:00
fecac84977 Set up interpretation for typed equality
yiyunliu merged pull request yiyunliu/sp-eta-postpone#1 2025-02-06 00:26:46 -05:00
logrelnew
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 00:26:46 -05:00
cd3b4981c7 Merge pull request 'logrelnew' (#1) from logrelnew into master
c24cc7c9b0 Finish ST Conv
64bcf8e9c1 Finish Proj case
d6a96430f0 Add semantic typing
55ccc2bc1d Prove the enhanced interpuniv bind inversion principle
Compare 19 commits »
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