3rd Irish Workshop on Formal Methods

Galway, Ireland. 1st - 2nd July 1999

AUTHORS

W. M. Farmer

ABSTRACT

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.

PAPER FORMATS

PDF Version of this Paper (117kb)