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