Yiyun Liu
|
687d1be03f
|
Finish preservation
|
2025-02-25 22:35:59 -05:00 |
|
Yiyun Liu
|
bb39f157ba
|
Finish regularity
|
2025-02-25 21:04:32 -05:00 |
|
Yiyun Liu
|
96bc223b0a
|
Finish renaming and preservation
|
2025-02-25 20:18:40 -05:00 |
|
|
|
cc0e9219c4
|
Finish two cases of renaming
|
2025-02-25 16:50:12 -05:00 |
|
|
|
291d821d94
|
Add some admits to work on later
|
2025-02-25 16:12:44 -05:00 |
|
Yiyun Liu
|
ba77752329
|
Add more cases to the soundness proof
|
2025-02-12 20:18:12 -05:00 |
|
Yiyun Liu
|
48adb34946
|
Add simplified projection lemma
|
2025-02-12 19:53:20 -05:00 |
|
|
|
5ac2bf1c40
|
Minor
|
2025-02-12 15:56:35 -05:00 |
|
|
|
c5de86339f
|
Finish subject reduction
|
2025-02-10 21:50:23 -05:00 |
|
|
|
8f8f428562
|
Finish preservation
|
2025-02-10 14:16:43 -05:00 |
|
|
|
5918fdf47e
|
Prove all but 5 cases of regularity
|
2025-02-10 13:51:35 -05:00 |
|
Yiyun Liu
|
26e3c1c42a
|
Add some cases for regularity
|
2025-02-10 01:15:44 -05:00 |
|
Yiyun Liu
|
c8e84ef93c
|
Finish morphing
|
2025-02-10 00:17:01 -05:00 |
|
Yiyun Liu
|
2c47d78ad6
|
Add stub for morphing
|
2025-02-09 23:32:07 -05:00 |
|
Yiyun Liu
|
ea1fba8ae9
|
Finish syntactic renaming
|
2025-02-09 20:41:27 -05:00 |
|
|
|
df5c6bf0b1
|
Minor
|
2025-02-09 17:05:36 -05:00 |
|
|
|
ab1bd8eef8
|
Add semantic rules for function beta and eta
|
2025-02-09 16:12:57 -05:00 |
|
Yiyun Liu
|
4396786701
|
Reformulate renaming
|
2025-02-08 22:56:45 -05:00 |
|
|
|
0e5b82b162
|
Move projection axioms to the subtyping relation
|
2025-02-06 21:40:26 -05:00 |
|
