logrelnew #1

Merged

yiyunliu merged 18 commits from logrelnew into master 2025-02-06 05:26:46 +00:00

Conversation 0 Commits 18 Files changed 4 +1363 -187

yiyunliu commented 2025-02-06 05:26:40 +00:00

Owner

Copy link

No description provided.

yiyunliu added 18 commits 2025-02-06 05:26:40 +00:00

Refactor the impossible case proof d9b5ef1267

Finish adding pi and sigma types e923194e3d

Add logical relation for SN ee24f8093e

Add a constant to avoid kripke LR 38a0416b2c

Merge remote-tracking branch 'origin/logrel' into logrelnew f83af1241b

Finish adequacy ext 2393cc5103

Add induction principle for InterpUniv 7f29fe0347

Start the proof that joinability preserves meaning 0e254c5ac3

Show that sne and bind are not joinable e444c8408f

Finish the injectivity of bind and noconfusion af224831e4

Finish most of InterpUniv join 7cc6435ea3

Side step the need for join subst 1997e8bc12

Finish the hard fun case for interpuniv_join 76f8c32dad

Finish InterpUniv_Join 4134fbdada

Prove the enhanced interpuniv bind inversion principle 55ccc2bc1d

Add semantic typing d6a96430f0

Finish Proj case 64bcf8e9c1

Finish ST Conv c24cc7c9b0

yiyunliu merged commit cd3b4981c7 into master 2025-02-06 05:26:46 +00:00

yiyunliu referenced this pull request from a commit 2025-02-06 05:26:46 +00:00

Merge pull request 'logrelnew' (#1) from logrelnew into master

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

yiyunliu/sp-eta-postpone!1

No description provided.