equal
deleted
inserted
replaced
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
|
2 |
|
3 <html> |
|
4 |
|
5 <head> |
|
6 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
|
7 <title>ZF/Resid/README</title> |
|
8 </head> |
|
9 |
|
10 <body> |
|
11 |
|
12 <h2>Resid -- A theory of residuals</h2> |
|
13 |
|
14 Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the |
|
15 article |
|
16 |
|
17 <p> |
|
18 |
|
19 <pre> |
|
20 @Article{huet-residual, |
|
21 author = "{G\'erard} Huet", |
|
22 title = "Residual Theory in $\lambda$-Calculus: A Formal Development", |
|
23 journal = JFP, |
|
24 year = 1994, |
|
25 volume = 4, |
|
26 number = 3, |
|
27 pages = "371--394"} |
|
28 </pre> |
|
29 |
|
30 See Rasmussen's report <a |
|
31 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>. |
|
32 |
|
33 </body> |
|
34 </html> |
|