2021
Novel rules of beta-conversion in partial type theory
RACLAVSKÝ, Jiří and Petr KUCHYŇKABasic information
Original name
Novel rules of beta-conversion in partial type theory
Authors
RACLAVSKÝ, Jiří (203 Czech Republic, guarantor, belonging to the institution) and Petr KUCHYŇKA (203 Czech Republic)
Edition
27th International Conference on Types for Proofs and Programs (TYPES2021), Nizozemí (online), 14. - 18. 6. 2021, 2021
Other information
Language
English
Type of outcome
Presentations at conferences
Field of Study
60301 Philosophy, History and Philosophy of science and technology
Country of publisher
Netherlands
Confidentiality degree
is not subject to a state or trade secret
References:
RIV identification code
RIV/00216224:14210/21:00119013
Organization unit
Faculty of Arts
Keywords in English
beta-reduction; partial type theory; partial lambda-calculus; explicit substitution; partiality; natural deduction
Tags
Tags
International impact, Reviewed
Changed: 21/3/2022 13:18, Mgr. et Mgr. Lucie Racyn
Abstract
In the original language
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.
Links
| GA19-12420S, research and development project |
|