k 2023

Conversion rules in type theory with evaluation terms

RACLAVSKÝ, Jiří

Základní údaje

Originální název

Conversion rules in type theory with evaluation terms

Autoři

Vydání

Logic and Applications, 2023

Další údaje

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í

Odkazy

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ěněno: 13. 3. 2024 11:40, Mgr. Kateřina Urubková

Anotace

V originále

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 MU
Název: Aspekty soudobé filozofie V
Investor: Masarykova univerzita, Aspekty soudobé filozofie V