Proving termination of normalization functions for conditional expressions

DOI10.1007/BF00246023MaRDI QIDQ1101251zbMATH OpenDBLPWikidataFDO

Authors Lawrence C. Paulson

Publication date 1986

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

Full work available at URL https://doi.org/10.1007/BF00246023

zbMATH Keywords

Boyer-Moore theorem proverdomain theoryLCFlongest common factorrecursion relationtermination proofstotal correctness

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Termination analysis for functional programs
• An ordinal measure based procedure for termination of functions
• scientific article; zbMATH DE number 3557747
• scientific article; zbMATH DE number 1487841
• scientific article; zbMATH DE number 4072437

Cited in

(9)

• Constructing recursion operators in intuitionistic type theory
• Synthesis of ML programs in the system Coq
• On proving the termination of algorithms by machine
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• scientific article; zbMATH DE number 1670762 (Why is no real title available?)
• scientific article; zbMATH DE number 3557747 (Why is no real title available?)
• Size-based termination of higher-order rewriting
• Function definition in higher-order logic
• Normalising the associative law: An experiment with Martin-Löf's type theory

Describes a project that uses

Uses Software

• LCF

This page was built for publication: Proving termination of normalization functions for conditional expressions

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