[Agda] Agda implementation of McBride's unification paper?

[Andrea Vezzosi]

On Mon, Nov 18, 2013 at 11:35 AM, Nils Anders Danielsson <nad at cse.gu.se>wrote:

> On 2013-11-18 00:26, Kenichi Asai wrote:
>
>> I wonder if there is an agda implementation of Conor McBride's paper
>> "First-order unification by structural recursion".  Any information is
>> welcome.
>>
>
> I believe that Andrea Vezzosi made use of this approach in his
> implementation of pattern unification:
>
>   https://github.com/Saizan/miller
>
>
I indeed reuse many concepts there, but a few years before I had also
implemented the original paper and the correctness proof[1] in Agda:

 http://code.haskell.org/~Saizan/unification/

It was one of my first Agda programs and I've never put much effort into
cleaning it up so the correctness proof is quite rough, though it should be
readable with the paper on the side.

One complication is that it threads various extensionality proofs alongside
"Property"'s so that we don't need to postulate functional extensionality.


[1] http://www.strictlypositive.org/foubsr-website/


-- Andrea Vezzosi
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131118/04031108/attachment.html