The following pages link to (Q4993352):
Displaying 19 items.
- Semantical analysis of contextual types (Q2200843) (← links)
- (Q4611379) (← links)
- (Q4611383) (← links)
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types (Q5016211) (← links)
- Model structure on the universe of all types in interval type theory (Q5022925) (← links)
- Syntax and models of Cartesian cubical type theory (Q5022926) (← links)
- Canonicity and homotopy canonicity for cubical type theory (Q5028486) (← links)
- Cubical methods in homotopy type theory and univalent foundations (Q5055493) (← links)
- On Church’s thesis in cubical assemblies (Q5055494) (← links)
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types (Q5056372) (← links)
- (Q5089011) (← links)
- (Q5091148) (← links)
- (Q5119390) (← links)
- (Q5155672) (← links)
- Indexed type theories (Q5156767) (← links)
- Modal dependent type theory and dependent right adjoints (Q5220184) (← links)
- Normalization by evaluation for modal dependent type theory (Q6065506) (← links)
- A general framework for the semantics of type theory (Q6149910) (← links)
- Two-level type theory and applications (Q6149950) (← links)
