Adapting functional programs to higher order logic

13 years 7 months ago
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.
Scott Owens, Konrad Slind
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where LISP
Authors Scott Owens, Konrad Slind
Comments (0)