Adapting functional programs to higher order logic

Higher-Order and Symbolic Computation, pp. 377-409, 2008.

Cited by: 12|Bibtex|Views2|Links
EI
Keywords:
difficult termination prooflogical functionfunctional programmercomfortable settingunfamiliar aspectMore(10+)

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 ma...More

Code:

Data:

Your rating :
0

 

Tags
Comments