# Masarykova univerzita

Informace o publikaci

# Novel rules of beta-conversion in partial type theory

Autoři KUCHYŇKA Petr 2021 Další prezentace na konferencích In partial type theory, i.e. a higher-order logical system that manipulates both total and partial functions, a precise formulation of valid rules of $\beta$-conversion and even their versions that substitute a value is possible if explicit substitution and two special evaluation terms are involved. We derive the latter rules from the primary versions of $\beta$-conversion rules and other primitive rules of the natural deduction for the system. In addition, we formulate and derive further novel variants of $\beta$-conversion rules which are also needed for capturing inferences with terms that denote partial functions.

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.