<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<title>ZF/Resid/README</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/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz">The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment</a>.
</body>
</html>