Name
Abstract | ||
|---|---|---|
Induction-induction is a principle for defining data types in Martin-Löf Type Theory. An inductive-inductive definition consists of a set A, together with an A-indexed family B : A → Set, where both A and B are inductively defined in such a way that the constructors for A can refer to B and vice versa. In addition, the constructors for B can refer to the constructors for A. We extend the usual initial algebra semantics for ordinary inductive data types to the inductive-inductive setting by considering dialgebras instead of ordinary algebras. This gives a new and compact formalisation of inductive-inductive definitions, which we prove is equivalent to the usual formulation with elimination rules. |
Year | Venue | Keywords |
|---|---|---|
2011 | CALCO | inductive-inductive definition,ordinary algebra,defining data type,compact formalisation,type theory,a-indexed family b,usual initial algebra semantics,usual formulation,ordinary inductive data type,elimination rule,categorical semantics |
Field | DocType | Citations |
Discrete mathematics,Initial algebra,Categorical semantics,Computer science,Type theory,Data type,Versa,Semantics,Type constructor | Conference | 3 |
PageRank | References | Authors |
0.45 | 14 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thorsten Altenkirch | 1 | 668 | 56.85 |
| Peter Morris | 2 | 3 | 0.45 |
| Fredrik Nordvall Forsberg | 3 | 28 | 8.82 |
| Anton Setzer | 4 | 230 | 22.50 |