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

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Filozofickou fakultu. Oficiální stránka publikace je na webu muni.cz.
Autoři

RACLAVSKÝ Jiří

Rok publikování 2022
Druh Další prezentace na konferencích
Fakulta / Pracoviště MU

Filozofická fakulta

Citace
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.