src/HOL/Proofs/Lambda/document/root.bib

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Proofs/Lambda/document/root.bib	Mon Sep 06 14:18:16 2010 +0200
@@ -0,0 +1,43 @@
+@TechReport{Loader1998,
+  author =	 {Ralph Loader},
+  title =	 {{N}otes on {S}imply {T}yped {L}ambda {C}alculus},
+  institution =	 {Laboratory for Foundations of Computer Science,
+                  School of Informatics, University of Edinburgh},
+  year =	 1998,
+  number =	 {ECS-LFCS-98-381}
+}
+
+@InProceedings{Matthes-ESSLLI2000,
+  author =	 {Ralph Matthes},
+  title =	 {{L}ambda {C}alculus: {A} {C}ase for {I}nductive
+                  {D}efinitions},
+  booktitle =	 {Lecture notes of the 12th European Summer School in
+                  Logic, Language and Information (ESSLLI 2000)},
+  year =	 2000,
+  month =	 {August},
+  publisher =	 {School of Computer Science, University of
+                  Birmingham}
+}
+
+@Article{Matthes-Joachimski-AML,
+  author =       {Felix Joachimski and Ralph Matthes},
+  title =        {Short Proofs of Normalization for the simply-typed
+                  $\lambda$-calculus, permutative conversions and
+                  {G}{\"o}del's {T}},
+  journal =      {Archive for Mathematical Logic},
+  year =         2003,
+  volume =       42,
+  number =       1,
+  pages =        {59--87}
+}
+
+@Article{Takahashi-IandC,
+  author = 	 {Masako Takahashi},
+  title = 	 {Parallel reductions in $\lambda$-calculus},
+  journal = 	 {Information and Computation},
+  year = 	 1995,
+  volume =	 118,
+  number =	 1,
+  pages =	 {120--127},
+  month =	 {April}
+}