# References

This file centralizes public external references cited in `README.md` and `docs/agents/`.
When adding new references to shared docs, prefer linking here instead of duplicating partial
citations inline.

## Papers

### ERHL25

Martin Avanzini, Gilles Barthe, Davide Davoli, and Benjamin Grégoire.
*A Quantitative Probabilistic Relational Hoare Logic*.
In *Proceedings of the 52nd ACM SIGPLAN Symposium on Principles of Programming Languages*
(POPL 2025), Denver, Colorado, USA, January 2025.
DOI: <https://doi.org/10.1145/3704876>
Public abstract and metadata: <https://inria.hal.science/hal-04834149v1>
Preprint: <https://arxiv.org/abs/2407.17127>

Used in:
- `docs/agents/program-logic.md`
- `docs/agents/proof-workflows.md`
- `docs/agents/gotchas.md`

### LOOM26

Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, and Ilya Sergey.
*Foundational Multi-Modal Program Verifiers*.
*Proceedings of the ACM on Programming Languages* 10 (POPL), Article 77, January 2026.
DOI: <https://doi.org/10.1145/3776719>

Used in:
- `README.md`

### PRHL14

Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy,
and Santiago Zanella-Béguelin.
*Probabilistic Relational Verification for Cryptographic Implementations*.
In *Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*
(POPL 2014).
DOI: <https://doi.org/10.1145/2535838.2535847>
Public metadata: <https://inria.hal.science/hal-00935743v1>

Background reference for:
- pRHL mentions in `docs/agents/program-logic.md`

### FCF14

Adam Petcher and Greg Morrisett.
*The Foundational Cryptography Framework*.
arXiv:1410.3735, 2014.
DOI: <https://doi.org/10.48550/arXiv.1410.3735>
Public abstract: <https://arxiv.org/abs/1410.3735>

Used in:
- `README.md`

## Projects and Repositories

### MATHLIB4

The Lean community.
*mathlib4: The math library of Lean 4*.
GitHub repository: <https://github.com/leanprover-community/mathlib4>
Documentation: <https://leanprover-community.github.io/mathlib4_docs/>

Used in:
- `README.md`

### LOOM-REPO

VERSE Lab.
*loom*.
GitHub repository: <https://github.com/verse-lab/loom>

Used in:
- `README.md`

### FCF-REPO

Adam Petcher.
*fcf*.
GitHub repository: <https://github.com/adampetcher/fcf>

Used in:
- `README.md`

### LEANCRYPTO3-REPO

`dtumad/lean-crypto-formalization`.
Deprecated Lean 3 repository for formalizing cryptography proofs.
GitHub repository: <https://github.com/dtumad/lean-crypto-formalization>

Used in:
- `README.md`