T-rex: termination of recursive functions using lexicographic linear combinations

DOI10.4230/LIPICS.ICALP.2024.139MaRDI QIDQ6875040zbMATH OpenFDO

Authors Raphael Douglas Giles, Vincent Jackson, Christine Rizkallah

Publication date 14 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ICALP.2024.139

zbMATH Keywords

recursive functionstermination

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Cites work

• A closer look at termination
• A predicative analysis of structural recursion
• An Unsolvable Problem of Elementary Number Theory
• Computer Aided Verification
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• scientific article; zbMATH DE number 4072437 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Khachiyan's linear programming algorithm
• On computable numbers, with an application to the Entscheidungsproblem.
• Ranking functions for linear-constraint loops
• Termination checking with types
• Termination of Isabelle functions via termination of rewriting
• The size-change principle for program termination
• The size-change termination principle for constructor based languages
• Über die Verallgemeinerung der Theorie der Rekursiven Funktionen für Abstrakte Mengen Geeigneter Struktur als Definitionsbereiche
• Verification, Model Checking, and Abstract Interpretation
• Zum Hilbertschen Aufbau der reellen Zahlen.

This page was built for publication: T-rex: termination of recursive functions using lexicographic linear combinations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6875040)