Proving termination of normalization functions for conditional expressions
From MaRDI portal
Publication:1101251
DOI10.1007/BF00246023zbMath0642.68159DBLPjournals/jar/Paulson86WikidataQ57382750 ScholiaQ57382750MaRDI QIDQ1101251
Publication date: 1986
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
LCFdomain theorytotal correctnessrecursion relationBoyer-Moore theorem provertermination proofslongest common factor
Related Items (6)
On proving the termination of algorithms by machine ⋮ Constructing recursion operators in intuitionistic type theory ⋮ Size-based termination of higher-order rewriting ⋮ Representing inductively defined sets by wellorderings in Martin-Löf's type theory ⋮ Normalising the associative law: An experiment with Martin-Löf's type theory ⋮ Synthesis of ML programs in the system Coq
Uses Software
This page was built for publication: Proving termination of normalization functions for conditional expressions
