Partial Type Theory TT* with Extensions
| Authors | |
|---|---|
| Year of publication | 2023 |
| Type | Appeared in Conference without Proceedings |
| MU Faculty or unit | |
| 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: |