Proving termination of normalization functions for conditional expressions
From MaRDI portal
Publication:1101251
DOI10.1007/BF00246023zbMath0642.68159WikidataQ57382750 ScholiaQ57382750MaRDI QIDQ1101251
Publication date: 1986
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
LCF; domain theory; total correctness; recursion relation; Boyer-Moore theorem prover; termination proofs; longest common factor
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Normalising the associative law: An experiment with Martin-Löf's type theory, 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
Uses Software