<div dir="ltr"><br><div class="gmail_extra"><br>On Mon, Nov 18, 2013 at 11:35 AM, Nils Anders Danielsson <span dir="ltr">&lt;<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>&gt;</span> wrote:<br><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div class="im">On 2013-11-18 00:26, Kenichi Asai wrote:<br>

<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
I wonder if there is an agda implementation of Conor McBride&#39;s paper<br>
&quot;First-order unification by structural recursion&quot;.  Any information is<br>
welcome.<br>
</blockquote>
<br></div>
I believe that Andrea Vezzosi made use of this approach in his<br>
implementation of pattern unification:<br>
<br>
  <a href="https://github.com/Saizan/miller" target="_blank">https://github.com/Saizan/<u></u>miller</a><div class="im"><br></div></blockquote><div><br></div><div>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:</div>
<div><br></div><div> <a href="http://code.haskell.org/~Saizan/unification/">http://code.haskell.org/~Saizan/unification/</a></div><div><br></div><div>It was one of my first Agda programs and I&#39;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.</div>
<div><br></div><div>One complication is that it threads various extensionality proofs alongside &quot;Property&quot;&#39;s so that we don&#39;t need to postulate functional extensionality.</div><div><br></div><div><br></div>
<div>[1] <a href="http://www.strictlypositive.org/foubsr-website/">http://www.strictlypositive.org/foubsr-website/</a></div><div><br></div><div><br></div><div>-- Andrea Vezzosi</div><div><br></div><div><br></div><div><br>
</div><div><br></div></div></div></div>