@inproceedings{RSW25,
  author    = "{Rosain, Johann and Sozeau, Matthieu and Winterhalter, Théo}",
  title     = "{A Ghost Sort for Proof-Relevant yet Erased Data in Rocq and MetaRocq (abstract)}",
  booktitle = "{Book of Abstracts of the 31st International Conference on Types for Proofs and Programs}",
  year      = {2025},
}