@misc{berry_fiore_2025,
  doi = {10.48550/ARXIV.2505.07780},
  url = {https://arxiv.org/abs/2505.07780},
  author = {Berry, David G. and Fiore, Marcelo P.},
  keywords = {Logic in Computer Science (cs.LO), Category Theory (math.CT), FOS: Computer and information sciences, FOS: Computer and information sciences, FOS: Mathematics, FOS: Mathematics, F.3.2; F.4.1, 03B40, 03B38, 68N18},
  title = {Formal P-Category Theory and Normalization by Evaluation in Rocq},
  publisher = {arXiv},
  year = {2025},
  copyright = {Creative Commons Attribution Non Commercial No Derivatives 4.0 International}
}