Adapting functional programs to higher order logic |
| |
Authors: | Scott Owens Konrad Slind |
| |
Affiliation: | (1) School of Computing, University of Utah, Salt Lake City, USA |
| |
Abstract: | 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. Electronic Supplementary Material The online version of this article () contains supplementary material, which is available to authorized users. |
| |
Keywords: | Higher order logic Recursive definition Termination Well-foundedness Regular expression pattern matching |
本文献已被 SpringerLink 等数据库收录! |
|