<html><head><base href="http://www.cs.nott.ac.uk/~txa/publ/tlca93.bib"></head><body style="-webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><base href="http://www.cs.nott.ac.uk/~txa/publ/tlca93.bib">I used them in <div><span class="Apple-style-span" style="font-family: monospace; white-space: pre-wrap; ">@InProceedings{alti:tlca93,</span></div><pre style="word-wrap: break-word; white-space: pre-wrap;"> author = "Thorsten Altenkirch",
title = "A Formalization of the Strong Normalization Proof for
{System F} in {LEGO}",
booktitle = "Typed Lambda Calculi and Applications",
year = "1993",
editor = "M. Bezem, J.F. Groote",
series = "LNCS 664",
pages = "13 - 28",
}
</pre><div id="myEventWatcherDiv" style="display:none;"></div><div>See Section 3.3</div><div><br></div><div>Cheers,</div><div>Thorsten</div><div><br><div><div>On 22 Mar 2011, at 11:22, Nicolas Pouillard wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div>Hello,<br><br>I'm looking for a paper to cite about the Fin data type and its use<br>to represent binders (say λ-terms). (I already have those about the<br>approach with nested data types).<br><br>Any idea?<br><br>Thanks in advance,<br><br>-- <br>Nicolas Pouillard<br><a href="http://nicolaspouillard.fr">http://nicolaspouillard.fr</a><br>_______________________________________________<br>Agda mailing list<br>Agda@lists.chalmers.se<br>https://lists.chalmers.se/mailman/listinfo/agda<br></div></blockquote></div><br></div></body></html>