|
|
c24cc7c9b0
|
Finish ST Conv
|
2025-02-06 00:08:02 -05:00 |
|
|
|
64bcf8e9c1
|
Finish Proj case
|
2025-02-05 23:56:47 -05:00 |
|
|
|
d6a96430f0
|
Add semantic typing
|
2025-02-05 21:44:35 -05:00 |
|
|
|
55ccc2bc1d
|
Prove the enhanced interpuniv bind inversion principle
|
2025-02-05 21:28:39 -05:00 |
|
|
|
4134fbdada
|
Finish InterpUniv_Join
|
2025-02-05 21:20:37 -05:00 |
|
|
|
76f8c32dad
|
Finish the hard fun case for interpuniv_join
|
2025-02-05 21:14:31 -05:00 |
|
Yiyun Liu
|
1997e8bc12
|
Side step the need for join subst
|
2025-02-05 20:36:39 -05:00 |
|
Yiyun Liu
|
7cc6435ea3
|
Finish most of InterpUniv join
|
2025-02-05 20:06:03 -05:00 |
|
Yiyun Liu
|
af224831e4
|
Finish the injectivity of bind and noconfusion
|
2025-02-05 18:56:47 -05:00 |
|
|
|
e444c8408f
|
Show that sne and bind are not joinable
|
2025-02-05 16:52:25 -05:00 |
|
|
|
0e254c5ac3
|
Start the proof that joinability preserves meaning
|
2025-02-05 15:47:51 -05:00 |
|
|
|
7f29fe0347
|
Add induction principle for InterpUniv
|
2025-02-05 14:44:26 -05:00 |
|
|
|
2393cc5103
|
Finish adequacy ext
|
2025-02-05 14:04:44 -05:00 |
|
|
|
f83af1241b
|
Merge remote-tracking branch 'origin/logrel' into logrelnew
|
2025-02-05 13:46:08 -05:00 |
|
|
|
38a0416b2c
|
Add a constant to avoid kripke LR
|
2025-02-04 22:14:27 -05:00 |
|
|
|
ee24f8093e
|
Add logical relation for SN
|
2025-02-04 16:05:02 -05:00 |
|
|
|
e923194e3d
|
Finish adding pi and sigma types
|
2025-02-04 15:29:47 -05:00 |
|
|
|
d9b5ef1267
|
Refactor the impossible case proof
|
2025-02-04 15:06:17 -05:00 |
|
