Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-06 23:41:45 -05:00
cf2726be8d Add subtyping
yiyunliu created branch subtyping in yiyunliu/sp-eta-postpone 2025-02-06 21:40:47 -05:00
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-06 21:40:47 -05:00
0e5b82b162 Move projection axioms to the subtyping relation
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 18:15:31 -05:00
2e2e41cbe6 Add missing Univ rule
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 18:09:26 -05:00
6daa275ac8 Prove the fundamental theorem
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 17:58:49 -05:00
399c97fa82 Add the semantic well-typedness rules to the hint db
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 17:47:43 -05:00
8d92f19d74 Add all(?) typing rules
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 17:00:11 -05:00
10f339c5b6 Add some syntactic typing rules
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 16:31:55 -05:00
82e21196c2 Minor
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 16:21:04 -05:00
e7a26e6bd6 Finish all Bind proj lemmas
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 16:02:28 -05:00
c25bac311c Add the first-component inversion lemma for pi and sigma
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 15:42:55 -05:00
aca7ebaf1e Finish all the semantic theory for the system with type-directed eq
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 15:20:45 -05:00
733e86c611 Finish SE_Pair
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 14:38:07 -05:00
435c0e037e Finish (simplified) SE_Bind
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 14:37:36 -05:00
1258ac263c Add structural rule for ctx equivalence
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-06 14:32:01 -05:00
db911cff36 Finish the context equality lemma
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 »