@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},

}