CoqPL 2025 Contributors

Sat 25 Jan 2025 Denver, Colorado, United States

co-located with POPL 2025

Filter

Role Type

Contributing to

Number of Roles

Country

Results (39)

B Stephanie BalzerBalzer, Stephanie Carnegie Mellon UniversityUnited States A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
Calvin BeckBeck, Calvin University of Pennsylvania, USACanada Vellvm: Formalizing the Informal
Yves BertotBertot, Yves INRIAFrance Session with the Coq Development Team
C Hanxi ChenChen, Hanxi University of Pennsylvania Vellvm: Formalizing the Informal
Joshua M. CohenCohen, Joshua M. Princeton University Implementing OCaml APIs in Coq
D Benjamin DelawareDelaware, Benjamin Purdue UniversityUnited States Session Chair of Session 2 (part of CoqPL) Session Chair of Session 3 (part of CoqPL) Towards Automated Verification of LLM-Synthesized C Programs Co-chair in Program Committee within the CoqPL-track
Marko DokoDoko, Marko Heriot-Watt University, UK CoqNFU: Towards Formalizing NFU in Coq
E Sebastian ErdwegErdweg, Sebastian JGU MainzGermany A Framework of Differential Operators
F Qiuyi FengFeng, Qiuyi Formal Verification of Quantum Stabilizer Code
G Tarakaram GollamudiGollamudi, Tarakaram None A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
Lourdes del Carmen González-HuescaGonzález-Huesca, Lourdes del Carmen National Autonomous University of MexicoMexico Committee Member in Program Committee within the CoqPL-track
J Jules JacobsJacobs, Jules Cornell University A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
K Cezary KaliszykKaliszyk, Cezary University of MelbourneAustralia Towards Mining Robust Coq Proof Patterns
L Ignacio LagunaLaguna, Ignacio Lawrence Livermore National LaboratoryUnited States Towards Verified Linear Algebra Programs Through Equivalence
Xuan-Bach D. LeLe, Xuan-Bach D. University of MelbourneAustralia Towards Mining Robust Coq Proof Patterns
Yao LiLi, Yao Portland State UniversityUnited States Committee Member in Program Committee within the CoqPL-track
M Gregory MalechaMalecha, Gregory BedRock SystemsUnited States Committee Member in Program Committee within the CoqPL-track
Prasita MukherjeeMukherjee, Prasita Towards Automated Verification of LLM-Synthesized C Programs
P Udaya ParampalliParampalli, Udaya Formal Verification of Quantum Stabilizer Code
Piotr PolesiukPolesiuk, Piotr University of Wrocław Committee Member in Program Committee within the CoqPL-track
Thibaut PéramiPérami, Thibaut University of Cambridge Towards general white-box automation: a typeclass-guided context cleaner
R Jan-Paul Ramos-DavilaRamos-Davila, Jan-Paul Cornell UniversityUnited States Formal Verification of a Software Defined Delay-Tolerant Network
Christine RizkallahRizkallah, Christine University of MelbourneAustralia Towards Mining Robust Coq Proof Patterns Formal Verification of Quantum Stabilizer Code
S John SarracinoSarracino, John Lawrence Livermore National Laboratory Towards Verified Linear Algebra Programs Through Equivalence
Matthew SottileSottile, Matthew Lawrence Livermore National Laboratory Towards Verified Linear Algebra Programs Through Equivalence
Matthieu SozeauSozeau, Matthieu InriaFrance Session with the Coq Development Team
Bas SpittersSpitters, Bas Aarhus UniversityDenmark Committee Member in Program Committee within the CoqPL-track
Kathrin StarkStark, Kathrin Heriot-Watt UniversityUnited Kingdom Session Chair of Session 1 (part of CoqPL) Co-chair in Program Committee within the CoqPL-track
T Nicolas TabareauTabareau, Nicolas Inria Session with the Coq Development Team
Enrico TassiTassi, Enrico INRIAFrance Elpi: rule-based meta-languge for Rocq Session with the Coq Development Team
Mohit TekriwalTekriwal, Mohit Lawrence Livermore National LaboratoryUnited States Towards Verified Linear Algebra Programs Through Equivalence
Romain TetleyTetley, Romain Committee Member in Program Committee within the CoqPL-track
X Runqing XuXu, Runqing A Framework of Differential Operators
Y Yihan YangYang, Yihan Harvey Mudd College Towards Verified Linear Algebra Programs Through Equivalence
Yue YaoYao, Yue Carnegie Mellon University A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
Qianchuan YeYe, Qianchuan University at Buffalo, SUNYUnited States Session Chair of Session 4 (16:00 - 17:30) (part of CoqPL) Committee Member in Program Committee within the CoqPL-track
Irene YoonYoon, Irene France Committee Member in Program Committee within the CoqPL-track
Z Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Vellvm: Formalizing the Informal
Č Vedran ČačićČačić, Vedran CoqNFU: Towards Formalizing NFU in Coq