Adapting functional programs to higher order logic
Higher-Order and Symbolic Computation, pp. 377-409, 2008.
difficult termination prooflogical functionfunctional programmercomfortable settingunfamiliar aspectMore(10+)
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 ma...More
Full Text (Upload PDF)
PPT (Upload PPT)