equal
deleted
inserted
replaced
|
1 <HTML><HEAD><TITLE>HOL/Lambda/ReadMe</TITLE></HEAD> |
|
2 <BODY> |
|
3 |
|
4 <H1>Lambda Calculus in de Bruijn's Notation</H1> |
|
5 |
|
6 This theory defines lambda-calculus terms with de Bruijn indixes and proves |
|
7 confluence of beta, eta and beta+eta. |
|
8 <P> |
|
9 Beta is proved confluent both in the traditional way (see Barendregt's book) |
|
10 and also following Takahashi's elegant version using developments. |
|
11 <P> |
|
12 |
|
13 A report describing the whole theory with the exception of eta-reduction is |
|
14 found here: <A HREF = |
|
15 "ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/church-rosser.html" |
|
16 >More Church-Rosser Proofs (in Isabelle)</A>. |
|
17 |
|
18 </BODY> |
|
19 </HTML> |