Łukasz Czajka

Polymorphic Higher-order Termination

2019 · arXiv (Cornell University)

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 …