Další formáty:
BibTeX
LaTeX
RIS
@proceedings{2219755,
author = {Raclavský, Jiří},
booktitle = {XXVII Incontro di Logica},
keywords = {partial type theory; evaluation terms; beta-conversion},
language = {eng},
title = {Problems with Beta-conversion Rules in Type Theory with Quotation and Evaluation Terms},
year = {2022}
}
TY - CONF
ID - 2219755
AU - Raclavský, Jiří
PY - 2022
TI - Problems with Beta-conversion Rules in Type Theory with Quotation and Evaluation Terms
KW - partial type theory
KW - evaluation terms
KW - beta-conversion
N2 - The (partial) type theory is enriched by terms for quotation and evaluation, following thus Lisp's family of programming languages. As noted by Farmer, various problems arise from such extensions, most notably with the substitutability of free variables nested in those new terms. In particular, the beta-conversion rules fail in some cases. In the talk, we solve all these problems.
ER -
RACLAVSKÝ, Jiří. Problems with Beta-conversion Rules in Type Theory with Quotation and Evaluation Terms. In \textit{XXVII Incontro di Logica}. 2022.
|
