Publication details

Derivability of rules of beta-conversion in partial type theory

Authors

RACLAVSKÝ Jiří KUCHYŇKA Petr

Year of publication 2022
Type Appeared in Conference without Proceedings
MU Faculty or unit

Faculty of Arts

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:

You are running an old browser version. We recommend updating your browser to its latest version.

More info