Conversion rules in type theory with evaluation terms

RACLAVSKÝ, Jiří. Conversion rules in type theory with evaluation terms. In Logic and Applications. 2023.

Basic information

Original name

Conversion rules in type theory with evaluation terms

Authors

RACLAVSKÝ, Jiří

Edition

Logic and Applications, 2023

---

Other information

Language

English

Type of outcome

Prezentace na konferencích

Field of Study

60301 Philosophy, History and Philosophy of science and technology

Country of publisher

Croatia

Confidentiality degree

není předmětem státního či obchodního tajemství

References:

URL

Organization unit

Faculty of Arts

Keywords in English

type theory; abstractions; substitution; beta-conversion rules

Tags

International impact, Reviewed

---

Abstract

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.

---

Links

MUNI/A/1082/2022, interní kód MU

Name: Aspekty soudobé filozofie V Investor: Masaryk University