Interpreting higher computations as types with totality
From MaRDI portal
Recommendations
- 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
Cites work
- 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
Cited in
(8)- scientific article; zbMATH DE number 841092 (Why is no real title available?)
- Equational theories for inductive types
- On the identity type as the type of computational paths
- Threshold voting leads to type-revelation
- Higher types, finite domains and resource-bounded Turing machines
- Can partial indexings be totalized?
- scientific article; zbMATH DE number 1497732 (Why is no real title available?)
- scientific article; zbMATH DE number 218500 (Why is no real title available?)
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)
