The Coq mailing list

[Conor McBride <ctm AT cs.nott.ac.uk>]

Colin Riba wrote:
> Hi all
>
> I'm looking for a formalisation of first order unification in Coq.
> Can somebody tell me if there are contributions and/or papers on this topics ?

My old LEGO formalization ought to be readily portable to Coq:

  http://www.cs.nott.ac.uk/~ctm/foubsr-website/

The relevant paper is in JFP 13(6). A preprint is here:

  http://www.cs.nott.ac.uk/~ctm/unify.ps.gz

The main novelty was that I used dependent data structures to remove the need
for a termination proof.

Hoping this is useful

Conor

--
http://www.cs.nott.ac.uk/~ctm

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.