First-Order Unification by Structural Recursion
This page provides access to the online resources for `First-Order Unification
by Structural Recursion', by Conor McBride. Specifically,
- A postscript file containing the correctness proof
for the program given in the paper.
- The entire development, program and proof, as a
script for the author's OLEG proof assistant.
OLEG is the author's unofficial, unsupported and highly experimental version
of Randy Pollack's marvellous type-theory-based proof assistant (whose name
may not be mentioned for legal reasons, but is an anagram of OLEG). It is
available by email on request from the author, whose
homepage is
located at the University of Nottingham.
OLEG binaries exist for Linux (on Intel machines) and Solaris (on Sun
Sparc machines). Its source code is also available, but (to the
author's knowledge) it only compiles with the Standard ML of New
Jersey compiler, version 0.93, which (ditto) has long since ceased to be
supported.
Conor McBride
9 October 2003
Last modified: Thu Feb 3 11:52:48 GMT 2005