Další formáty:
BibTeX
LaTeX
RIS
@proceedings{2317981, author = {Raclavský, Jiří}, booktitle = {Logic and Applications}, keywords = {type theory; abstractions; substitution; beta-conversion rules}, language = {eng}, note = {(conf.)}, title = {Conversion rules in type theory with evaluation terms}, url = {https://lap.math.hr/}, year = {2023} }
TY - CONF ID - 2317981 AU - Raclavský, Jiří PY - 2023 TI - Conversion rules in type theory with evaluation terms N1 - (conf.) KW - type theory KW - abstractions KW - substitution KW - beta-conversion rules UR - https://lap.math.hr/ N2 - 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. ER -
RACLAVSKÝ, Jiří. Conversion rules in type theory with evaluation terms. In \textit{Logic and Applications}. 2023.
|