Publication details
Novel rules of beta-conversion in partial type theory
| Authors | |
|---|---|
| Year of publication | 2021 |
| Type | Appeared in Conference without Proceedings |
| MU Faculty or unit | |
| Citation | |
| Description | 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. |
| Related projects: |