Conversion rules in type theory with evaluation terms



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

Faculty of Arts

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.