Verifying termination and reduction properties about higher-order logic programs

DOI10.1007/s10817-005-6534-3zbMath1102.68648OpenAlexW2031835656MaRDI QIDQ850496

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)

Related Items

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, αCheck: A mechanized metatheory model checker, POPLMark reloaded: Mechanizing proofs by logical relations, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), Programming Inductive Proofs, A case study in programming coinductive proofs: Howe’s method

Uses Software

• TALP
• HiLog
• Twelf
• Elf

Cites Work

• Termination proofs for logic programs
• Unification under a mixed prefix
• On proving the termination of algorithms by machine
• Modular termination proofs for rewriting using dependency pairs
• Termination of term rewriting using dependency pairs
• A predicative analysis of structural recursion
• A Coverage Checking Algorithm for LF
• Proving termination properties of prolog programs: A semantic approach
• A framework for defining logics
• HiLog: A foundation for higher-order logic programming
• A semantic basis for the termination analysis of logic programs
• Natural deduction as higher-order resolution
• The size-change principle for program termination
• Automated Deduction – CADE-19
• Automated Deduction – CADE-19
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item