Conversion rules in type theory with evaluation terms
| Autoři | |
|---|---|
| Rok publikování | 2023 |
| Druh | Další prezentace na konferencích |
| Fakulta / Pracoviště MU | |
| 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: |