Derivability of rules of beta-conversion in partial type theory
| Authors | |
|---|---|
| Year of publication | 2022 |
| Type | Appeared in Conference without Proceedings |
| MU Faculty or unit | |
| Citation | |
| Description | In partial type theory (PTT), the rules of beta-conversion should be appropriately conditioned in order to preserve their validity which can be negatively affected by partiality (non-denoting expressions). After showing that within a particular natural deduction for PTT, we derive also their novel variants which allow inferences not permissible using the original variants. Moreover, we derive even versions that substitute value (resembling call-by-value evaluation). |
| Related projects: |