src/HOL/Lambda/README.html
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 15582 7219facb3fd0
child 36862 952b2b102a0a
permissions -rw-r--r--
simplified code generator setup
webertj@15283
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
webertj@15283
     2
paulson@1542
     3
<!-- $Id$ -->
webertj@15582
     4
webertj@15582
     5
<HTML>
webertj@15582
     6
webertj@15582
     7
<HEAD>
webertj@15582
     8
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
webertj@15582
     9
  <TITLE>HOL/Lambda</TITLE>
webertj@15582
    10
</HEAD>
webertj@15582
    11
nipkow@1346
    12
<BODY>
nipkow@1346
    13
nipkow@1346
    14
<H1>Lambda Calculus in de Bruijn's Notation</H1>
nipkow@1346
    15
nipkow@1346
    16
This theory defines lambda-calculus terms with de Bruijn indixes and proves
nipkow@1346
    17
confluence of beta, eta and  beta+eta.
nipkow@1346
    18
<P>
nipkow@1432
    19
nipkow@1346
    20
nipkow@1645
    21
The paper
nipkow@13360
    22
<A HREF="http://www.in.tum.de/~nipkow/pubs/jar2001.html">
paulson@1541
    23
More Church-Rosser Proofs (in Isabelle/HOL)</A>
paulson@1541
    24
describes the whole theory.
nipkow@1346
    25
paulson@1542
    26
<HR>
paulson@1542
    27
nipkow@8888
    28
<P>Last modified 20.5.2000
paulson@1542
    29
nipkow@1346
    30
</BODY>
nipkow@1346
    31
</HTML>