Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    A Scheme for Defining Partial Higher-Order Functions by Recursion

    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.


    PDF filePDF Version of this Paper (117kb)