Text size
  • Small
  • Medium
  • Large
Contrast
  • 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

    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 filePDF Version of this Paper (117kb)