Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 22:23:46 -05:00
9f3b04d041 Finish sn red preservation
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 17:30:07 -05:00
fc0e096c04 Add two cases for red sn preservation
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 15:11:22 -05:00
2af49373e3 Repair epar sn preservation
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 14:35:38 -05:00
396bddc8b3 Finish unmorphing
yiyunliu created branch nat in yiyunliu/sp-eta-postpone 2025-02-21 13:23:44 -05:00
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 13:23:44 -05:00
fd0b48073d Add nat type definition
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-19 18:03:44 -05:00
0e0d9b20e5 Try making the cases mutually recursive?
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-19 17:41:26 -05:00
fe5c16361a Add definition for algorithmic domain
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-19 16:04:19 -05:00
df0b955e4e Add the stub for Equations but might give up later
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-17 23:31:39 -05:00
d48d9db1b7 Finish the conversion proof completely
9c5eb31edf Finish all cases of subtyping
735c7f2046 Prove some simple soundness cases of subtyping
067ae89b1d Finish soundness for subtyping
Compare 4 commits »
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-17 23:31:22 -05:00
d48d9db1b7 Finish the conversion proof completely
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-17 22:50:40 -05:00
9c5eb31edf Finish all cases of subtyping
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-17 21:43:31 -05:00
735c7f2046 Prove some simple soundness cases of subtyping
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-17 18:35:06 -05:00
067ae89b1d Finish soundness for subtyping
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-17 18:05:50 -05:00
ef3de3af3d Add the specification for algorithmic subtyping
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-16 23:53:24 -05:00
ef3de3af3d Add the specification for algorithmic subtyping
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-16 23:41:37 -05:00
8daaae9831 Minor
eaf59fc45e Finish all cases of algorithmic completeness
21d9a2ce1b Add standardization_lo
bdba6f50e5 Finish the soundness proof completely
d24991e994 Finish most of the neu abs case
Compare 24 commits »
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-16 23:41:26 -05:00
8daaae9831 Minor
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-16 23:25:42 -05:00
eaf59fc45e Finish all cases of algorithmic completeness
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-16 23:00:30 -05:00
21d9a2ce1b Add standardization_lo