Termination Checking in the Presence of Nested Inductive and Coinductive Types | Zendy

Thorsten Altenkirch | Zendy; Nils Anders Danielsson | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Termination Checking in the Presence of Nested Inductive and Coinductive Types

Author(s) -

Thorsten Altenkirch,

Nils Anders Danielsson

Publication year - 2018

Publication title -

epic series in computing

Language(s) - English

Resource type - Conference proceedings

ISSN - 2398-7340

DOI - 10.29007/n51d

Subject(s) - coinduction , programming language , computer science , functional programming , simplicity , simple (philosophy) , extension (predicate logic) , theoretical computer science , mathematics , philosophy , geometry , epistemology , mathematical proof

In the dependently typed functional programming language Agda one can easily mix induction and coinduction. The implementation of the termination/productivity checker is based on a simple extension of a termination checker for a language with inductive types. However, this simplicity comes at a price: only types of the form X .Y .F X Y can be handled directly, not types of the form Y .X .F X Y . We explain the implementation of the termination checker and the ensuing problem.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research