The following pages link to (Q4263867):
Displaying 20 items.
- Induction-recursion and initial algebras. (Q1412830) (← links)
- Finitary higher inductive types in the groupoid model (Q2130587) (← links)
- Constructing a universe for the setoid model (Q2233391) (← links)
- Indexed induction-recursion (Q2577476) (← links)
- Type-theoretic approaches to ordinals (Q2700785) (← links)
- Type-level Computation Using Narrowing in Ωmega (Q2866338) (← links)
- Turing-Completeness Totally Free (Q2941179) (← links)
- Proof-Producing Reflection for HOL (Q2945631) (← links)
- How to Reason Coinductively Informally (Q3305562) (← links)
- (Q4611383) (← links)
- (Q4989403) (← links)
- A Syntax for Higher Inductive-Inductive Types (Q4993350) (← links)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- Variations on inductive-recursive definitions (Q5111280) (← links)
- Dependent Types at Work (Q5191088) (← links)
- (Q5216301) (← links)
- Program Testing and the Meaning Explanations of Intuitionistic Type Theory (Q5253930) (← links)
- For Finitary Induction-Induction, Induction is Enough (Q6079233) (← links)
- Impredicative encodings of inductive-inductive data in Cedille (Q6535795) (← links)
