Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
7
 Projects Packages Public activity Starred repositories
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-07 16:46:05 -05:00
0746e9a354 Finish subtyping semantics
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-07 01:19:27 -05:00
4bc08e1897 Add one interpuniv sub case
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-07 00:43:19 -05:00
707483d401 Add injectivity for subtyping
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-07 00:39:45 -05:00
2f4ea2c78b Add more noconfusion lemmas for untyped subtyping
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