# Polymorphic Higher-order Termination

## TL;DR

This paper extends higher-order polynomial interpretations to impredicative polymorphism within System F-omega, enabling direct termination proofs for complex rewrite rules and inductive data types, demonstrated on a logic fragment.

## Contribution

It introduces a novel termination method for impredicative polymorphic systems by interpreting terms in an extended System F-omega, broadening applicability.

## Key findings

- Proves termination of a significant fragment of second-order propositional logic.
- Enables direct interpretation of rewrite rules using impredicative polymorphism.
- Facilitates encoding of inductive data types in termination proofs.

## Abstract

We generalise the termination method of higher-order polynomial interpretations to a setting with impredicative polymorphism. Instead of using weakly monotonic functionals, we interpret terms in a suitable extension of System F-omega. This enables a direct interpretation of rewrite rules which make essential use of impredicative polymorphism. In addition, our generalisation eases the applicability of the method in the non-polymorphic setting by allowing for the encoding of inductive data types. As an illustration of the potential of our method, we prove termination of a substantial fragment of full intuitionistic second-order propositional logic with permutative conversions.