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>HOL/Lambda</TITLE> |
|
8 </HEAD> |
|
9 |
|
10 <BODY> |
|
11 |
|
12 <H1>Lambda Calculus in de Bruijn's Notation</H1> |
|
13 |
|
14 This theory defines lambda-calculus terms with de Bruijn indixes and proves |
|
15 confluence of beta, eta and beta+eta. |
|
16 <P> |
|
17 |
|
18 |
|
19 The paper |
|
20 <A HREF="http://www.in.tum.de/~nipkow/pubs/jar2001.html"> |
|
21 More Church-Rosser Proofs (in Isabelle/HOL)</A> |
|
22 describes the whole theory. |
|
23 |
|
24 <HR> |
|
25 |
|
26 <P>Last modified 20.5.2000 |
|
27 |
|
28 </BODY> |
|
29 </HTML> |