scientific article; zbMATH DE number 1302063
From MaRDI portal
Publication:4247308
Recommendations
Cited in
(46)- An information system interpretation of Martin-Löf's partial type theory with universes
- Types, tableaus, and Gödel's God
- Induction-recursion and initial algebras.
- Universics: a theory of universes of discourse for metamathematics and foundations
- On the number of types
- The strength of Martin-Löf type theory with a superuniverse. I
- Predicativity and constructive mathematics
- Axiomatic reals and certified efficient exact real computation
- Graded modal dependent type theory
- Constructive completions of ordered sets, groups and fields
- Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
- Maximal and partial points in formal spaces
- Regular universes and formal spaces
- Indexed induction-recursion
- Observability in the univalent universe
- First steps towards cumulative inductive types in CIC
- Joyal's arithmetic universes via type theory
- Universe polymorphism in Coq
- scientific article; zbMATH DE number 3881865 (Why is no real title available?)
- From mathesis universalis to provability, computability, and constructivity
- Universe Types for Topology and Encapsulation
- scientific article; zbMATH DE number 3950525 (Why is no real title available?)
- scientific article; zbMATH DE number 4027461 (Why is no real title available?)
- A construction of type: type in Martin-Löf's partial type theory with one universe
- scientific article; zbMATH DE number 65535 (Why is no real title available?)
- scientific article; zbMATH DE number 515742 (Why is no real title available?)
- scientific article; zbMATH DE number 713392 (Why is no real title available?)
- scientific article; zbMATH DE number 2111733 (Why is no real title available?)
- A realizability semantics for inductive formal topologies, Church's thesis and axiom of choice
- Applications of type theory
- On the n-uniqueness of types in rosy theories
- Multimodal dependent type theory
- UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY
- On the ubiquity of certain total type structures
- scientific article; zbMATH DE number 2247252 (Why is no real title available?)
- Dependent products and 1-inaccessible universes
- From type theory to setoids and back
- Universes in explicit mathematics
- Type theories, toposes and constructive set theory: Predicative aspects of AST
- Normalization by evaluation for modal dependent type theory
- Generalized universe hierarchies and first-class universe levels
- Coalgebras in functional programming and type theory
- Non-trivial universes and sequences of universes
- Topological quantum gates in homotopy type theory
- Interpretation of inaccessible sets in Martin-Löf type theory with one Mahlo universe
- Propositional functions and families of types
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4247308)
