--- a/Nominal/Ex/Exec/document/root.bib	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-@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},
-}