Polymorphic Higher-Order Termination

Authors Łukasz Czajka , Cynthia Kop

Thumbnail PDF


  • Filesize: 0.53 MB
  • 18 pages

Document Identifiers

Author Details

Łukasz Czajka
  • Faculty of Informatics, TU Dortmund, Germany
Cynthia Kop
  • Institute of Computer Science, Radboud University Nijmegen, The Netherlands

Cite AsGet BibTex

Łukasz Czajka and Cynthia Kop. Polymorphic Higher-Order Termination. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Type theory
  • termination
  • polymorphism
  • higher-order rewriting
  • permutative conversions


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. F. Blanqui. Definitions by rewriting in the Calculus of Constructions. MSCS, 15(1):37-92, 2005. Google Scholar
  2. D. Cousineau and G. Dowek. Embedding Pure Type Systemsin the lambda-Pi-calculus modulo. In TLCA, pages 102-117, 2017. Google Scholar
  3. Ł. Czajka and C. Kop. Polymorphic Higher-Order Termination (extended version), 2019. URL: http://arxiv.org/abs/1904.09859.
  4. G. Dowek. Models and termination of proof reduction in the λΠ-calculus modulo theory. In ICALP, pages 109:1-109:14, 2017. Google Scholar
  5. M. Fiore and M. Hamana. Multiversal Polymorphic Algebraic Theories: syntacs, semantics, translations and equational logic. In LICS, pages 520-520, 2013. Google Scholar
  6. C. Fuhs and C. Kop. Polynomial Interpretations for Higher-Order Rewriting. In RTA, pages 176-192, 2012. Google Scholar
  7. J.-V. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge University Press, 1989. Google Scholar
  8. J.-Y. Girard. Une Extension De l'Interpretation De Gödel a l'Analyse, Et Son Application a l'Elimination Des Coupures Dans l'Analyse Et La Theorie Des Types. In SLS, pages 63-92. Elsevier, 1971. Google Scholar
  9. M. Hamana. Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation. In FLOPS, pages 99-115, 2018. Google Scholar
  10. B. Jacobs and J. Rutten. An introduction to (co)algebras and (co)induction. In Advanced Topics in Bisimulation and Coinduction, pages 38-99. Cambridge University Press, 2011. Google Scholar
  11. J. Jouannaud and A. Rubio. Polymorphic higher-order recursive path orderings. JACM, 54(1):1-48, 2007. Google Scholar
  12. C. Kop. Higher Order Termination. PhD thesis, VU University Amsterdam, 2012. Google Scholar
  13. C. Kop and F. van Raamsdonk. Dynamic Dependency Pairs for Algebraic Functional Systems. LMCS, 8(2):10:1-10:51, 2012. Google Scholar
  14. D. Kozen and A. Silva. Practical coinduction. Mathematical Structures in Computer Science, 27(7):1132-1152, 2017. Google Scholar
  15. J.C. van de Pol. Termination of Higher-order Rewrite Systems. PhD thesis, University of Utrecht, 1996. Google Scholar
  16. D. Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2012. Google Scholar
  17. M.H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006. Google Scholar
  18. M.H. Sørensen and P. Urzyczyn. A Syntactic Embedding of Predicate Logic into Second-Order Propositional Logic. Notre Dame Journal of Formal Logic, 51(4):457-473, 2010. Google Scholar
  19. S. Suzuki, K. Kusakari, and F. Blanqui. Argument Filterings and Usable Rules in Higher-Order Rewrite Systems. IPSJ Transactions on Programming, 4(2):1-12, 2011. Google Scholar
  20. M. Tatsuta. Simple Saturated Sets for Disjunction and Second-Order Existential Quantification. In TLCA 2007, pages 366-380, 2007. Google Scholar
  21. Terese. Term Rewriting Systems. Cambridge University Press, 2003. Google Scholar
  22. A.S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 1996. Google Scholar
  23. J.C. van de Pol. Termination Proofs for Higher-order Rewrite Systems. In HOA, pages 305-325, 1993. Google Scholar
  24. J.C. van de Pol and H. Schwichtenberg. Strict Functionals for Termination Proofs. In TLCA 95, pages 350-364, 1995. Google Scholar
  25. D. Wahlstedt. Type Theory with First-Order Data Types and Size-Change Termination. PhD thesis, Göteborg University, 2004. Google Scholar
  26. D. Walukiewicz-Chrząszcz. Termination of rewriting in the Calculus of Constructions. JFP, 13(2):339-414, 2003. Google Scholar
  27. A. Wojdyga. Short Proofs of Strong Normalization. In MFCS, pages 613-623, 2008. Google Scholar