Pritam Choudhury (2015):
Constructive Representation of Nominal Sets in Agda.
Cambridge University.
Ernesto Copello, Nora Szasz & Álvaro Tasistro (2018):
Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders.
Electronic Proceedings in Theoretical Computer Science 274,
doi:10.4204/EPTCS.274.2.
Ernesto Copello, Nora Szasz & Álvaro Tasistro (2018):
Machine-checked Proof of the Church-Rosser Theorem for the Lambda Calculus Using the Barendregt Variable Convention in Constructive Type Theory.
Electronic Notes in Theoretical Computer Science 338,
pp. 79–95,
doi:10.1016/j.entcs.2018.10.006.
Ernesto Copello, Álvaro Tasistro, Nora Szasz, Ana Bove & Maribel Fernández (2016):
Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory.
Electronic Notes in Theoretical Computer Science 323,
pp. 109–124,
doi:10.1016/j.entcs.2016.06.008.
Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015).
Thierry Coquand & Arnaud Spiwack (2010):
Contribuciones científicas en honor de Mirian Andrés Gómez, chapter Constructively finite?,
pp. 217–230.
M. J. Gabbay & A. M. Pitts (2002):
A New Approach to Abstract Syntax with Variable Binding.
Formal Aspects of Computing 13,
pp. 341–363,
doi:10.1007/s001650200016.
Thomas William. Hungerford (1974):
Algebra.
Graduate texts in mathematics.
Springer,
New York,
doi:10.1007/978-1-4612-6101-8.
Miguel Pagano & José E. Solsona (2022):
Nominal Sets in Agda.
https://github.com/miguelpagano/nominal-sets/.
Fabrício S. Paranhos & Daniel Ventura:
Towards a Formalization of Nominal Sets in Coq.
https://popl22.sigplan.org/details/CoqPL-2022-papers/4/Towards-a-Formalization-of-Nominal-Sets-in-Coq.
Online; accessed 1 May 2022.
Andrew M. Pitts (2013):
Nominal Sets: Names and Symmetry in Computer Science.
Cambridge tracts in Theoretical Computer Science.
Cambridge University Press,
Cambridge, England,
doi:10.1017/CBO9781139084673.
Andrew Swan (2017):
Some Brouwerian Counterexamples Regarding Nominal Sets in Constructive Set Theory,
doi:10.48550/ARXIV.1702.01556.
The Agda Team (2021):
The Agda standard library, version 1.7.
https://github.com/agda/agda-stdlib.
Christian Urban & Stefan Berghofer (2006):
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.
In: Ulrich Furbach & Natarajan Shankar: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings,
Lecture Notes in Computer Science 4130.
Springer,
pp. 498–512,
doi:10.1007/11814771_41.
eptcs@eptcs.org