Další formáty:
BibTeX
LaTeX
RIS
@proceedings{1861562, author = {Raclavský, Jiří and Kuchyňka, Petr}, booktitle = {Czech Gathering of Logicians (CGL2022)}, keywords = {beta-reduction; partial type theory; partial lambda-calculus; natural deduction}, language = {eng}, note = {(conf.)}, title = {Derivability of rules of beta-conversion in partial type theory}, url = {http://uivty.cs.cas.cz/~clog2022/}, year = {2022} }
TY - CONF ID - 1861562 AU - Raclavský, Jiří - Kuchyňka, Petr PY - 2022 TI - Derivability of rules of beta-conversion in partial type theory N1 - (conf.) KW - beta-reduction KW - partial type theory KW - partial lambda-calculus KW - natural deduction UR - http://uivty.cs.cas.cz/~clog2022/ N2 - 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). ER -
RACLAVSKÝ, Jiří a Petr KUCHYŇKA. Derivability of rules of beta-conversion in partial type theory. In \textit{Czech Gathering of Logicians (CGL2022)}. 2022.
|