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, 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