Derivability of rules of beta-conversion in partial type theory
| Autoři | |
|---|---|
| Rok publikování | 2022 |
| Druh | Další prezentace na konferencích |
| Fakulta / Pracoviště MU | |
| Citace | |
| Popis | 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). |
| Související projekty: |