Publication details

Partial Type Theory TT* with Extensions

Authors

RACLAVSKÝ Jiří

Year of publication 2023
Type Appeared in Conference without Proceedings
MU Faculty or unit

Faculty of Arts

Citation
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info