--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Exec/document/root.bib	Tue May 22 14:55:58 2012 +0200
@@ -0,0 +1,76 @@
+@inproceedings{HuffmanUrban10,
+  author = 	 {B.~Huffman and C.~Urban},
+  title = 	 {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle},
+  booktitle = {Proc.~of the 1st Conference on  Interactive Theorem Proving (ITP'10)}, 
+  pages = {35--50},
+  volume = {6172},
+  series = {LNCS},
+  year = 	 {2010}
+}
+@inproceedings{Sac11,
+  author    = {Cezary Kaliszyk and
+               Christian Urban},
+  title     = {Quotients revisited for {I}sabelle/{HOL}},
+  booktitle = {Proc. of the 26th ACM Symposium on Applied Computing (SAC'11)},
+  year      = {2011},
+  pages     = {1639-1644},
+  publisher = {ACM},
+  editor    = {William C. Chu and W. Eric Wong and Mathew J. Palakal and Chih-Cheng Hung},
+}
+@inproceedings{Esop11,
+  author    = {Christian Urban and
+               Cezary Kaliszyk},
+  title     = {General Bindings and Alpha-Equivalence in {N}ominal {I}sabelle},
+  year      = {2011},
+  pages     = {480-500},
+  booktitle     = {Proc. of the 20th European Symposium on Programming (ESOP'11)},
+  publisher = {Springer Verlag},
+  series    = {LNCS},
+  volume    = {6602},
+  editor    = {Gilles Barthe},
+}
+
+@book{LambdaBook,
+  author = {Hendrik Pieter Barendregt},
+  title={{The Lambda Calculus: Its Syntax and Semantics}},
+  year={2001},
+  publisher={Elsevier},
+  volume  = {103},
+  series  = {Studies in Logic and the Foundations of Mathematics},
+}
+
+@article{Pitts03,
+  author =	 {Andrew M.~Pitts},
+  title =	 {{N}ominal {L}ogic, {A} {F}irst {O}rder {T}heory of {N}ames and
+                  {B}inding},
+  journal =	 {Information and Computation},
+  year =	 {2003},
+  volume =	 {183},
+  pages =	 {165--193}
+}
+
+@Article{Norrish06,
+  author =       {Michael Norrish},
+  title =        {Mechanising $\lambda$-Calculus Using a Classical First Order
+                  Theory of Terms with Permutations},
+  journal =      {Higher-Order and Symbolic Computation},
+  year =         2006,
+  volume =       19,
+  pages =        {169--195},
+  doi =          {10.1007/s10990-006-8745-7}
+}
+
+@Inproceedings{NominalLambda,
+    author = {Christian Urban},
+    title = {{Nominal techniques in Isabelle/HOL}},
+    booktitle = {Proceedings of the 20th International Conference on Automated Deduction (CADE'05)},
+    year = {2005},
+    pages = {38--53},
+    publisher = {Springer}
+}
+@article{LocallyNameless,
+  author    = {Randy Pollack and Masahiko Sato and Wilmer Ricciotti},
+  title     = {A Canonical Locally Named Representation of Binding},
+  journal   = {Journal of Automated Reasoning},
+  year      = {2011},
+}