Conversion rules in type theory with 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í 2023
Druh Další prezentace na konferencích
Fakulta / Pracoviště MU

Filozofická fakulta

Citace
Popis To emulate metareasoning and metaprogramming of programming languages such as Lisp (Javascript etc.) (simple) type theory is extended by quotation and evaluation terms. But then both alpha- and beta-conversion rules fail, the system is inconsistent. One finds that a harmony between substitution, assignment, and free variables is broken; two possible solutions re-establish the harmony. The elaborated one corrects evaluation rule for abstractions.
Související projekty:

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