Conversion rules in type theory with evaluation terms

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Arts. Official publication website can be found on muni.cz.
Authors

RACLAVSKÝ Jiří

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

Faculty of Arts

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

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