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