Formalizing termination proofs under polynomial quasi-interpretations

MaRDI QIDQ5014441zbMATH OpenFDO

Authors Naohi Eguchi

Publication date 2 December 2021

Full work available at URL https://arxiv.org/abs/1509.03014, http://eptcs.web.cse.unsw.edu.au/paper.cgi?FICS2015.5

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) First-order arithmetic and fragments (03F30) Functional programming and lambda calculus (68N18)

Recommendations

• Quasi-interpretations. A way to control resources
• scientific article; zbMATH DE number 2084367
• scientific article; zbMATH DE number 2242587
• Algorithms with polynomial interpretation termination proof
• scientific article; zbMATH DE number 1348481

Cites work

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 5722524 (Why is no real title available?)
• scientific article; zbMATH DE number 4066875 (Why is no real title available?)
• scientific article; zbMATH DE number 1215494 (Why is no real title available?)
• scientific article; zbMATH DE number 1339873 (Why is no real title available?)
• scientific article; zbMATH DE number 2006637 (Why is no real title available?)
• scientific article; zbMATH DE number 2079048 (Why is no real title available?)
• scientific article; zbMATH DE number 2084367 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 814819 (Why is no real title available?)
• A term rewriting characterization of the functions computable in polynomial space
• Algorithms with polynomial interpretation termination proof
• Analysing the implicit complexity of programs.
• Improved witnessing and local improvement principles for second-order bounded arithmetic
• Orderings for term-rewriting systems
• Proof-theoretic analysis of termination proofs
• Quasi-interpretations. A way to control resources
• Relationships between nondeterministic and deterministic tape complexities
• Subrecursiveness: Machine-independent notions of computability in restricted time and storage
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths

Cited in

(5)

• Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
• scientific article; zbMATH DE number 2084367 (Why is no real title available?)
• Polynomials over the reals in proofs of termination : from theory to practice
• Formal correctness of a quadratic unification algorithm
• scientific article; zbMATH DE number 2242587 (Why is no real title available?)

This page was built for publication: Formalizing termination proofs under polynomial quasi-interpretations

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