Pages that link to "Item:Q4508246"
From MaRDI portal
The following pages link to A general formulation of simultaneous inductive-recursive definitions in type theory (Q4508246):
Displayed 38 items.
- Map fusion for nested datatypes in intensional type theory (Q627204) (← links)
- Viewing \({\lambda}\)-terms through maps (Q740485) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- Induction-recursion and initial algebras. (Q1412830) (← links)
- Predicativity and constructive mathematics (Q2080590) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- Finitary higher inductive types in the groupoid model (Q2130587) (← links)
- Constructing a universe for the setoid model (Q2233391) (← links)
- Canonicity for cubical type theory (Q2319982) (← links)
- Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory (Q2503336) (← links)
- Regular universes and formal spaces (Q2575774) (← links)
- Indexed induction-recursion (Q2577476) (← links)
- From realizability to induction via dependent intersection (Q2636522) (← links)
- Another Look at Function Domains (Q2805150) (← links)
- A Brief Overview of Agda – A Functional Language with Dependent Types (Q3183520) (← links)
- Working with Mathematical Structures in Type Theory (Q3499757) (← links)
- Least and Greatest Fixpoints in Game Semantics (Q3617718) (← links)
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (Q3637183) (← links)
- An induction principle for nested datatypes in intensional type theory (Q3638923) (← links)
- Typed Applicative Structures and Normalization by Evaluation for System F ω (Q3644739) (← links)
- (Q4611383) (← links)
- A Syntax for Higher Inductive-Inductive Types (Q4993350) (← links)
- (Q5089009) (← links)
- Variations on inductive-recursive definitions (Q5111280) (← links)
- (Q5155674) (← links)
- Dependent Types at Work (Q5191088) (← links)
- (Q5216301) (← links)
- ETA-RULES IN MARTIN-LÖF TYPE THEORY (Q5240810) (← links)
- Program Testing and the Meaning Explanations of Intuitionistic Type Theory (Q5253930) (← links)
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe (Q5262927) (← links)
- Pure type systems with explicit substitutions (Q5371956) (← links)
- Well-founded recursion with copatterns and sized types (Q5371960) (← links)
- Partiality and recursion in interactive theorem provers – an overview (Q5741556) (← links)
- Containers, monads and induction recursion (Q5741557) (← links)
- From type theory to setoids and back (Q5889302) (← links)
- A Comparison of Type Theory with Set Theory (Q6075430) (← links)
- Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)
- An intuitionistic set-theoretical model of fully dependent CC (Q6174091) (← links)