Adapting functional programs to higher order logic

Higher-order logic proof systems combine functional programming with logic, providing functional programmers with a comfortable setting for the formalization of programs, specifications, and proofs. However, a possibly unfamiliar aspect of working in such an environment is that formally establishing program termination is necessary. In many cases, termination can be automatically proved, but there are useful programs that diverge and others that always terminate but have difficult termination proofs. We discuss techniques that support the expression of such programs as logical functions. Three programs, a depth-first search, an unfold, and a regular expression matcher are used to demonstrate the techniques.

• Type: Journal
• Year: 2008
• Where: LISP
• Authors: Scott Owens, Konrad Slind
• Keywords: Difficult Termination Proofs, Functional Programmers, Functional Programming, LISP 2008