Interpreting higher computations as types with totality
The paper may be seen as a foundational study on the notion of totality, using Girard's qualitative domains as a tool. The starting observation is that in qualitative domains there is no ``intrinsic way to refer to total objects. Hence, the authors add more structure to qualitative domains, defining (partial) \(E\)-structures and totality domains, where a certain subset of total elements is selected (interestingly, these total elements are not in general the maximal elements of the domain). Each of these new classes of structures is proved closed under products \(\Pi (x\in X)Y_x\) indexed by stable parameterization. The principal object of study is now introduced by a monotone inductive definition: a hierarchy of totality domains and of names for them, where new structures are obtained via stable parameterization. The main theorem of the paper, proved by the so-called mollification method, is that the complexity of the hierarchy definition is equivalent to recursion in Kleene's \({}^3 E\) functional.
- scientific article; zbMATH DE number 3986625
- Computational higher-dimensional type theory
- An intuitionistic theory of types with assumptions of high-arity variables
- Semantics of higher inductive types
- scientific article; zbMATH DE number 1302061
- scientific article; zbMATH DE number 1047956
- Computability in higher types, P and the completeness of type assignment
- Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality
- Interpreting descriptions in intensional type theory
- Expressing computational complexity in constructive type theory
- scientific article; zbMATH DE number 218500 (Why is no real title available?)
- Recursive Functionals and Quantifiers of Finite Types I
- The system \({\mathcal F}\) of variable types, fifteen years later
- Total objects in inductively defined types
- Total sets and objects in domain theory
- Π12-logic, Part 1: Dilators
- Threshold voting leads to type-revelation
- Can partial indexings be totalized?
- Higher types, finite domains and resource-bounded Turing machines
- scientific article; zbMATH DE number 1497732 (Why is no real title available?)
- On the identity type as the type of computational paths
- scientific article; zbMATH DE number 218500 (Why is no real title available?)
- scientific article; zbMATH DE number 841092 (Why is no real title available?)
- Equational theories for inductive types
This page was built for publication: Interpreting higher computations as types with totality
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1337495)
