A |

antifounded coinduction, corecursion | Antifounded Coinduction in Type Theory |

C |

coinduction | Beating the Productivity Checker Using Embedded Languages Termination Checking in the Presence of Nested Inductive and Coinductive Types |

coinductive | Cyclic Proofs and Coinductive Principles |

constructive | Cyclic Proofs and Coinductive Principles |

corecursion | Beating the Productivity Checker Using Embedded Languages Termination Checking in the Presence of Nested Inductive and Coinductive Types |

D |

dependent types | MiniAgda: Integrating Sized and Dependent Types Beating the Productivity Checker Using Embedded Languages Termination Casts: A Flexible Approach to Termination with General Recursion Termination Checking in the Presence of Nested Inductive and Coinductive Types |

E |

Event-B | Rewriting and Well-Definedness within a Proof System |

G |

general recursion | General Recursion and Formal Topology Termination Casts: A Flexible Approach to Termination with General Recursion |

I |

inductive | Cyclic Proofs and Coinductive Principles |

inductively generated formal topologies | General Recursion and Formal Topology |

M |

mixed induction and coinduction | Beating the Productivity Checker Using Embedded Languages Termination Checking in the Presence of Nested Inductive and Coinductive Types |

P |

partial functions | Rewriting and Well-Definedness within a Proof System |

pattern matching | MiniAgda: Integrating Sized and Dependent Types |

Productivity | MiniAgda: Integrating Sized and Dependent Types |

Prover Extensibility | Rewriting and Well-Definedness within a Proof System |

R |

recursion operator | General Recursion and Formal Topology |

S |

sized types | MiniAgda: Integrating Sized and Dependent Types |

subset, quotient types | Antifounded Coinduction in Type Theory |

T |

term rewriting | Rewriting and Well-Definedness within a Proof System |

termination | MiniAgda: Integrating Sized and Dependent Types |

transition systems | Cyclic Proofs and Coinductive Principles |

type theory | Termination Casts: A Flexible Approach to Termination with General Recursion Antifounded Coinduction in Type Theory |

types | Cyclic Proofs and Coinductive Principles |

W |

Well-definedness | Rewriting and Well-Definedness within a Proof System |

wellfounded induction, recursion | Antifounded Coinduction in Type Theory |