<!-- $Id$ -->
<HTML><HEAD><TITLE>ZF/Resid</TITLE></HEAD><BODY>
<H2>Resid -- A theory of residuals</H2>
Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the
article
<P>
<PRE>
@Article{huet-residual,
author = "{G\'erard} Huet",
title = "Residual Theory in $\lambda$-Calculus: A Formal
Development",
journal = JFP,
year = 1994,
volume = 4,
number = 3,
pages = "371--394"}
</PRE>
See Rasmussen's report
<A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz">The Church-Rosser Theorem in Isabelle: A Proof Porting
Experiment</A>.
<HR>
<P>Last modified 5 March 1996
<ADDRESS>
<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>