The size-change termination principle for constructor based languages

DOI10.2168/LMCS-10(1:11)2014MaRDI QIDQ5404477zbMATH OpenOpenAlexFDO

Authors Hyvernat Pierre

Publication date 24 March 2014

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1306.3833

zbMATH Keywords

MLprogram analysissize-change principletermination analysis

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Abstract: This paper describes an automatic termination checker for a generic first-order call-by-value language in ML style. We use the fact that value are built from variants and tuples to keep some information about how arguments of recursive call evolve during evaluation. The result is a criterion for termination extending the size-change termination principle of Lee, Jones and Ben-Amram that can detect size changes inside subvalues of arguments. Moreover the corresponding algorithm is easy to implement, making it a good candidate for experimentation.

Recommendations

• The size-change principle for program termination
• Programming Languages and Systems
• scientific article; zbMATH DE number 2043534
• Size-Change Termination and Bound Analysis
• Rewriting Techniques and Applications

Cited in

(13)

• A Classical Realizability Model for a Semantical Value Restriction
• Size-Change Termination and Bound Analysis
• scientific article; zbMATH DE number 2043534 (Why is no real title available?)
• Size-based termination of higher-order rewriting
• Dependency pairs termination in dependent type theory modulo rewriting
• The size-change principle for program termination
• Programming Languages and Systems
• Compositional coinduction with sized types
• Rewriting Techniques and Applications
• Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
• T-rex: termination of recursive functions using lexicographic linear combinations
• The size-change principle for mixed inductive and coinductive types
• Totality for mixed inductive and coinductive types

This page was built for publication: The size-change termination principle for constructor based languages

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