Problems with Beta-conversion Rules in Type Theory with Quotation and Evaluation Terms



Year of publication 2022
Type Appeared in Conference without Proceedings
MU Faculty or unit

Faculty of Arts

Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.