Skip to content

REFERENCES.md

Latest commit

 

History

History
95 lines (68 loc) · 2.45 KB

REFERENCES.md

File metadata and controls

95 lines (68 loc) · 2.45 KB
Raw

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