Other formats:
BibTeX
LaTeX
RIS
@proceedings{1776237, author = {Raclavský, Jiří and Kuchyňka, Petr}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES2021), Nizozemí (online), 14. - 18. 6. 2021}, keywords = {beta-reduction; partial type theory; partial lambda-calculus; explicit substitution; partiality; natural deduction}, language = {eng}, note = {(conf.)}, title = {Novel rules of beta-conversion in partial type theory}, url = {https://types21.liacs.nl/}, year = {2021} }
TY - CONF ID - 1776237 AU - Raclavský, Jiří - Kuchyňka, Petr PY - 2021 TI - Novel rules of beta-conversion in partial type theory N1 - (conf.) KW - beta-reduction KW - partial type theory KW - partial lambda-calculus KW - explicit substitution KW - partiality KW - natural deduction UR - https://types21.liacs.nl/ N2 - 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. ER -
RACLAVSKÝ, Jiří and Petr KUCHYŇKA. Novel rules of beta-conversion in partial type theory. In \textit{27th International Conference on Types for Proofs and Programs (TYPES2021), Nizozemí (online), 14. - 18. 6. 2021}. 2021.
|