@article(Aydemir2007,
 author       = {Brian E. Aydemir and Aaron Bohannon and Stephanie Weirich},
 year         = {2007},
 title        = {Nominal Reasoning Techniques in Coq: (Extended Abstract)},
 journal      = {Electron. Notes Theor. Comput. Sci.},
 volume       = {174},
 number       = {5},
 pages        = {69--77},
 doi          = {10.1016/j.entcs.2007.01.028},
)
@article(Bengtson2007,
 author       = {Jesper Bengtson and Joachim Parrow},
 year         = {2009},
 title        = {Formalising the pi-calculus using nominal logic},
 journal      = {Log. Methods Comput. Sci.},
 volume       = {5},
 number       = {2},
 doi          = {10.2168/lmcs-5(2:16)2009},
 url          = {http://arxiv.org/abs/0809.3960},
)
@mastersthesis(Chou2015-mt,
 author       = {Pritam Choudhury},
 year         = {2015},
 title        = {Constructive Representation of Nominal Sets in Agda},
 school       = {Cambridge University},
)
@article(Copello2018-2,
 author       = {Ernesto Copello and Nora Szasz and \'Alvaro Tasistro},
 year         = {2018},
 title        = {Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders},
 journal      = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {274},
 doi          = {10.4204/EPTCS.274.2},
)
@article(Copello2018,
 author       = {Ernesto Copello and Nora Szasz and \'Alvaro Tasistro},
 year         = {2018},
 title        = {Machine-checked Proof of the Church-Rosser Theorem for the Lambda Calculus Using the Barendregt Variable Convention in Constructive Type Theory},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {338},
 pages        = {79--95},
 doi          = {10.1016/j.entcs.2018.10.006},
)
@article(Copello2016,
 author       = {Ernesto Copello and \'Alvaro Tasistro and Nora Szasz and Ana Bove and Maribel Fernández},
 year         = {2016},
 title        = {Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {323},
 pages        = {109--124},
 doi          = {10.1016/j.entcs.2016.06.008},
 note         = {Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015)},
)
@inbook(Coquand2010,
 author       = {Thierry Coquand and Arnaud Spiwack},
 year         = {2010},
 title        = {Contribuciones cient{\'\i}ficas en honor de Mirian Andr{\'e}s G{\'o}mez},
 chapter      = {Constructively finite?},
 pages        = {217--230},
)
@article(Gabbay2002,
 author       = {M. J. Gabbay and A. M. Pitts},
 year         = {2002},
 title        = {A New Approach to Abstract Syntax with Variable Binding},
 journal      = {Formal Aspects of Computing},
 volume       = {13},
 pages        = {341--363},
 doi          = {10.1007/s001650200016},
)
@book(Hungerford,
 author       = {Thomas William. Hungerford},
 year         = {1974},
 title        = {Algebra},
 series       = {Graduate texts in mathematics},
 publisher    = {Springer},
 address      = {New York},
 doi          = {10.1007/978-1-4612-6101-8},
)
@misc(pagano2022,
 author       = {Miguel Pagano and José E. Solsona},
 year         = {2022},
 title        = {Nominal Sets in Agda},
 howpublished = {\url{https://github.com/miguelpagano/nominal-sets/}},
)
@misc(Paranhos2022,
 author       = {Fabrício S. Paranhos and Daniel Ventura},
 title        = {Towards a Formalization of Nominal Sets in Coq},
 howpublished = {\url{https://popl22.sigplan.org/details/CoqPL-2022-papers/4/Towards-a-Formalization-of-Nominal-Sets-in-Coq}},
 note         = {Online; accessed 1 May 2022},
)
@mastersthesis(paranhos-thesis,
 author       = {Fabrício Sanches Paranhos},
 year         = {2022},
 title        = {Uma Formalização da Teoria Nominal em Coq},
 type         = {Master thesis},
 school       = {Universidade Federal de Goiás (UFG), Brasil},
 url          = {http://repositorio.bc.ufg.br/tede/handle/tede/12314},
)
@book(Pitts2013-book,
 author       = {Andrew M. Pitts},
 year         = {2013},
 title        = {Nominal Sets: Names and Symmetry in Computer Science},
 series       = {Cambridge tracts in Theoretical Computer Science},
 publisher    = {Cambridge University Press},
 address      = {Cambridge, England},
 doi          = {10.1017/CBO9781139084673},
)
@misc(Swan2017,
 author       = {Andrew Swan},
 year         = {2017},
 title        = {Some Brouwerian Counterexamples Regarding Nominal Sets in Constructive Set Theory},
 doi          = {10.48550/ARXIV.1702.01556},
)
@misc(agdalib,
 author       = {{\relax The Agda Team}},
 year         = {2021},
 title        = {The Agda standard library, version 1.7},
 howpublished = {\url{https://github.com/agda/agda-stdlib}},
)
@inproceedings(Urban2006,
 author       = {Christian Urban and Stefan Berghofer},
 year         = {2006},
 title        = {A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL},
 editor       = {Ulrich Furbach and Natarajan Shankar},
 booktitle    = {Automated Reasoning, Third International Joint Conference, {IJCAR} 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {4130},
 publisher    = {Springer},
 pages        = {498--512},
 doi          = {10.1007/11814771\_41},
)