Formalizing termination proofs under polynomial quasi-interpretations

zbMATH Open1476.68060arXiv1509.03014MaRDI QIDQ5014441FDOQ5014441

Authors: Naohi Eguchi 

Publication date: 2 December 2021

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

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

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)

Cites Work

• Relationships between nondeterministic and deterministic tape complexities
• Title not available (Why is that?)
• Algorithms with polynomial interpretation termination proof
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Quasi-interpretations. A way to control resources
• Orderings for term-rewriting systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proof-theoretic analysis of termination proofs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
• Analysing the implicit complexity of programs.
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• Subrecursiveness: Machine-independent notions of computability in restricted time and storage
• A term rewriting characterization of the functions computable in polynomial space
• Title not available (Why is that?)
• Improved witnessing and local improvement principles for second-order bounded arithmetic
• Title not available (Why is that?)

Cited In (5)

• Title not available (Why is that?)
• Polynomials over the reals in proofs of termination : from theory to practice
• Formal correctness of a quadratic unification algorithm
• Title not available (Why is that?)
• Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs

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)