RACLAVSKÝ, Jiří. Conversion rules in type theory with evaluation terms. In Logic and Applications. 2023.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Conversion rules in type theory with evaluation terms
Autoři RACLAVSKÝ, Jiří.
Vydání Logic and Applications, 2023.
Další údaje
Originální jazyk angličtina
Typ výsledku Prezentace na konferencích
Obor 60301 Philosophy, History and Philosophy of science and technology
Stát vydavatele Chorvatsko
Utajení není předmětem státního či obchodního tajemství
WWW URL
Organizační jednotka Filozofická fakulta
Klíčová slova anglicky type theory; abstractions; substitution; beta-conversion rules
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnila: Mgr. Kateřina Urubková, učo 425917. Změněno: 13. 3. 2024 11:40.
Anotace
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.
Návaznosti
MUNI/A/1082/2022, interní kód MUNázev: Aspekty soudobé filozofie V
Investor: Masarykova univerzita, Aspekty soudobé filozofie V
VytisknoutZobrazeno: 12. 9. 2024 18:27