| 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 |
