Index of /ports/math/isabelle/work/Isabelle2005/src/ZF/Resid
Name Last modified Size Description
Parent Directory 09-Aug-2008 06:10 -
Confluence.thy 17-Jun-2005 07:15 3k
Confluence.thy.html 09-Aug-2008 06:10 0k
ROOT.ML 22-Dec-2001 10:42 1k
ROOT.ML.html 09-Aug-2008 06:10 0k
Redex.thy 17-Jun-2005 07:15 6k
Redex.thy.html 09-Aug-2008 06:10 0k
Reduction.thy 17-Jun-2005 07:15 8k
Reduction.thy.html 09-Aug-2008 06:10 0k
Residuals.thy 17-Jun-2005 07:15 6k
Residuals.thy.html 09-Aug-2008 06:10 0k
Substitution.thy 17-Jun-2005 07:15 9k
Substitution.thy.html 09-Aug-2008 06:10 0k
ZF/Resid/README
Resid -- A theory of residuals
Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the
article
@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"}
See Rasmussen's report The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment.