BCS is a registered charity: No 292786
3rd Irish Workshop on Formal Methods
Galway, Ireland. 1st - 2nd July 1999
W. M. Farmer
This paper describes a scheme for defining partial higher-order functions as the least fixed points of monotone functionals.
The scheme can be used to define both single functions by recursion and systems of functions by mutual recursion. The scheme is implemented in the IMPS Interactive Mathematical Proof System.
The IMPS implementation includes an automatic syntactic check for monotonicity that succeeds for many common recursive definitions.