2026-07-22T19:33:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10519 2024-03-06T10:46:07Z ddc:004 open_access

Polymorphic Higher-Order Termination Czajka, Łukasz Kop, Cynthia termination polymorphism higher-order rewriting permutative conversions 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Łukasz Czajka and Cynthia Kop 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.12 urn:nbn:de:0030-drops-105193 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.12 eng https://creativecommons.org/licenses/by/3.0/legalcode