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 analysistermination analysissize-change principle

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

(10)

• scientific article; zbMATH DE number 7559275 (Why is no real title available?)
• The size-change principle for program termination
• Rewriting Techniques and Applications
• Programming Languages and Systems
• Size-based termination of higher-order rewriting
• Compositional coinduction with sized types
• A Classical Realizability Model for a Semantical Value Restriction
• Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
• Size-Change Termination and Bound Analysis
• scientific article; zbMATH DE number 2043534 (Why is no real title available?)

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)