Verifying termination and reduction properties about higher-order logic programs

DOI10.1007/S10817-005-6534-3MaRDI QIDQ850496zbMATH OpenOpenAlexFDO

Authors Brigitte Pientka

Publication date 3 November 2006

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-005-6534-3

zbMATH Keywords

terminationLogical frameworks

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 1765685
• Automatic Termination Verification for Higher-Order Functional Programs
• Adapting functional programs to higher order logic
• Model checking higher-order programs
• Temporal verification of higher-order functional programs

Cites work

• scientific article; zbMATH DE number 1615245 (Why is no real title available?)
• scientific article; zbMATH DE number 1696606 (Why is no real title available?)
• scientific article; zbMATH DE number 2185672 (Why is no real title available?)
• scientific article; zbMATH DE number 65531 (Why is no real title available?)
• scientific article; zbMATH DE number 1765685 (Why is no real title available?)
• scientific article; zbMATH DE number 1405629 (Why is no real title available?)
• A coverage checking algorithm for LF
• A framework for defining logics
• A predicative analysis of structural recursion
• A semantic basis for the termination analysis of logic programs
• Automated Deduction – CADE-19
• Automating the dependency pair method.
• HiLog: A foundation for higher-order logic programming
• Modular termination proofs for rewriting using dependency pairs
• Natural deduction as higher-order resolution
• On proving the termination of algorithms by machine
• Proving termination properties of prolog programs: A semantic approach
• Termination of term rewriting using dependency pairs
• Termination proofs for logic programs
• The size-change principle for program termination
• Unification under a mixed prefix

Cited in

(8)

• scientific article; zbMATH DE number 1765685 (Why is no real title available?)
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• A case study in programming coinductive proofs: Howe's method
• Programming inductive proofs. A new approach based on contextual types
• αCheck: A mechanized metatheory model checker
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• POPLMark reloaded: mechanizing proofs by logical relations

Describes a project that uses

Uses Software

• Elf
• Twelf
• HiLog
• TALP

This page was built for publication: Verifying termination and reduction properties about higher-order logic programs

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