Partial Type Theory TT* with Extensions

Autoři

RACLAVSKÝ Jiří

Rok publikování 2023
Druh Další prezentace na konferencích
Fakulta / Pracoviště MU

Filozofická fakulta

Citace
Popis In the talk, we present some main features of TT*, but we focus on its extensions using evaluation terms. Evaluation terms correspond to Lisp's evaluation terms; see Farmer 2016 for a discussion of their need in computer science and also a set of problems brought by their adoption. The current version of TT* successfully resists the problems and allows thus deduction not only with higher-order functions-as-mappings, but also with (total or partial) functions-as-algorithms w.r.t. (total or partial) functions-as-mappings.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.