CPP 2025 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (104)

A Cass AlexandruAlexandru, Cass RPTU Kaiserslautern-LandauGermany Intrinsically Correct Sorting in Cubical Agda
Ricardo AlmeidaAlmeida, Ricardo University of Edinburgh A CHERI C Memory Model for Verified Temporal Safety
José Bacelar AlmeiraAlmeira, José Bacelar University of Minho & INESC TEC Leakage-Free Probabilistic Jasmin Programs
B Anne BaanenBaanen, Anne Vrije Universiteit Amsterdam Certifying rings of integers in number fields
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States PC Member in Program Committee within the CPP-track
Lars BirkedalBirkedal, Lars Aarhus UniversityDenmark The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands PC Member in Program Committee within the CPP-track
Sandrine BlazyBlazy, Sandrine University of RennesFrance Session Chair of Session 5 (part of CPP) Business Meeting PC Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track PC Chair in Program Committee within the CPP-track
Sylvie BoldoBoldo, Sylvie Inria and Université Paris-SaclayFrance PC Member in Program Committee within the CPP-track
Sylvain BoulméBoulmé, Sylvain Université Grenoble Alpes - CNRS - Grenoble INP - VerimagFrance Formally verified hardening of C programs against hardware fault injection
C Brian CampbellCampbell, Brian University of Edinburgh A CHERI C Memory Model for Verified Temporal Safety
Mario CarneiroCarneiro, Mario CMUUnited States PC Member in Program Committee within the CPP-track
Nicolas ChappeChappe, Nicolas Inria Lyon, LIP Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IR
Agnishom ChattopadhyayChattopadhyay, Agnishom Rice University Verified and Efficient Matching of Regular Expressions with Lookaround
Alain Chavarri VillarelloChavarri Villarello, Alain Vrije Universiteit Amsterdam Certifying rings of integers in number fields
James CheneyCheney, James University of EdinburghUnited Kingdom Nominal Matching Logic With Fixpoints
Louis CheungCheung, Louis University of Melbourne Formalized Burrows-Wheeler Transform
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Committee Member in Steering Committee within the CPP-track
Vikraman ChoudhuryChoudhury, Vikraman Università di Bologna & Inria OLASItaly Intrinsically Correct Sorting in Cubical Agda
Johan CommelinCommelin, Johan University of Utrecht PC Member in Program Committee within the CPP-track
D Sander R. DahmenDahmen, Sander R. Vrije Universiteit Amsterdam Certifying rings of integers in number fields
Ana de Almeida Borgesde Almeida Borges, Ana Portugal PC Member in Program Committee within the CPP-track
Tom de Jongde Jong, Tom University of NottinghamUnited Kingdom PC Member in Program Committee within the CPP-track
F Maribel FernandezFernandez, Maribel King's College LondonUnited Kingdom Nominal Matching Logic With Fixpoints
Nathaniel FilardoFilardo, Nathaniel University of Cambridge A CHERI C Memory Model for Verified Temporal Safety
Denis FirsovFirsov, Denis Tallinn University of TechnologyEstonia Leakage-Free Probabilistic Jasmin Programs
Asta Halkjær FromFrom, Asta Halkjær University of Copenhagen An Isabelle/HOL Framework for Synthetic Completeness Proofs
Daniel FruminFrumin, Daniel University of GroningenNetherlands PC Member in Program Committee within the CPP-track
G Aina Linn GeorgesGeorges, Aina Linn Max Planck Institute for Software Systems (MPI-SWS) The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
Georges GonthierGonthier, Georges Inria Committee Member in Steering Committee within the CPP-track
Jason GrossGross, Jason MIT CSAILUnited States PC Member in Program Committee within the CPP-track
H Katharina HeidlerHeidler, Katharina Technical University Munich Formalizing the One-way to Hiding Theorem
Ludovic HenrioHenrio, Ludovic University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIPFrance Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IR
Florent HivertHivert, Florent Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA Machine Checked Proofs and Programs in Algebraic Combinatorics
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany Steering Committee Chair in Steering Committee within the CPP-track
Chung-Kil HurHur, Chung-Kil Seoul National UniversitySouth Korea CRIS: The power of imagination in specification and verification
J Martin JensenJensen, Martin Aarhus University CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
K Cezary KaliszykKaliszyk, Cezary University of MelbourneAustralia PC Member in Program Committee within the CPP-track
Jeehoon KangKang, Jeehoon KAISTSouth Korea PC Member in Program Committee within the CPP-track
Dohan KimKim, Dohan University of Innsbruck An Isabelle formalization of co-rewrite pairs for non-reachability in conditional rewriting
Christina KirkKirk, Christina University of Innsbruck Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Gerwin KleinKlein, Gerwin Proofcraft and UNSW SydneyAustralia Committee Member in Steering Committee within the CPP-track
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University and Southampton UniversityUnited Kingdom PC Member in Program Committee within the CPP-track
Nicolai KrausKraus, Nicolai University of NottinghamUnited Kingdom PC Member in Program Committee within the CPP-track
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands Committee Member in Steering Committee within the CPP-track PC Member in Program Committee within the CPP-track
L Ambroise LafontLafont, Ambroise Ecole PolytechniqueFrance PC Member in Program Committee within the CPP-track
Vincent LaporteLaporte, Vincent Inria PC Member in Program Committee within the CPP-track
Robert Y. LewisLewis, Robert Y. Brown UniversityUnited States PC Member in Program Committee within the CPP-track
Wu Angela LiLi, Wu Angela Rice University Verified and Efficient Matching of Regular Expressions with Lookaround
Jannis LimpergLimperg, Jannis University of Munich (LMU)Germany Tactic Script Optimisation for Aesop
M Konstantinos MamourasMamouras, Konstantinos Rice UniversityUnited States Verified and Efficient Matching of Regular Expressions with Lookaround
William ManskyMansky, William University of Illinois ChicagoUnited States PC Member in Program Committee within the CPP-track
Patrick MassotMassot, Patrick Université Paris-SaclayFrance PC Member in Program Committee within the CPP-track
Micaela MayeroMayero, Micaela LIPN, Université Paris 13France PC Member in Program Committee within the CPP-track
Wolfgang MeierMeier, Wolfgang Aarhus University CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
Kayvan MemarianMemarian, Kayvan University of CambridgeUnited Kingdom A CHERI C Memory Model for Verified Temporal Safety
Aart MiddeldorpMiddeldorp, Aart University of Innsbruck Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Dale MillerMiller, Dale INRIA Saclay and LIX/Institut Polytechnique de ParisFrance Committee Member in Steering Committee within the CPP-track
Yasuhiko MinamideMinamide, Yasuhiko Tokyo Institute of TechnologyJapan Session Chair of Session 3 (part of CPP) Formalization of Differential Privacy in Isabelle/HOL Further Tackling Post Correspondence Problem and Proof Generation PC Member in Program Committee within the CPP-track
Alistair MoffatMoffat, Alistair The University of Melbourne Formalized Burrows-Wheeler Transform
Alberto MomiglianoMomigliano, Alberto Università degli Studi di Milano Split Decisions: Explicit Contexts for Substructural Languages
David MonniauxMonniaux, David CNRSFrance Formally verified hardening of C programs against hardware fault injection
Cesar MunozMunoz, Cesar NASAUnited States PC Member in Program Committee within the CPP-track
N Tobias NipkowNipkow, Tobias Technische Universität München Committee Member in Steering Committee within the CPP-track
O Tiago OliveiraOliveira, Tiago SandboxAQ Leakage-Free Probabilistic Jasmin Programs
Akihiro OmoriOmori, Akihiro Department of Mathematical and Computing Science, Tokyo Institute of Technology Further Tackling Post Correspondence Problem and Proof Generation
P Karl PalmskogPalmskog, Karl KTH Royal Institute of TechnologySweden PC Member in Program Committee within the CPP-track
Jennifer PaykinPaykin, Jennifer IntelUnited States Session Chair of Session 2 (part of CPP) PC Member in Program Committee within the CPP-track
Basile PesinPesin, Basile Ecole Nationale de l'Aviation Civile (ENAC) Formally verified hardening of C programs against hardware fault injection
Jean Pichon-PharabodPichon-Pharabod, Jean Aarhus UniversityDenmark CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
Brigitte PientkaPientka, Brigitte McGill UniversityCanada Split Decisions: Explicit Contexts for Substructural Languages Committee Member in Steering Committee within the CPP-track
Clément Pit-ClaudelPit-Claudel, Clément EPFLSwitzerland PC Member in Program Committee within the CPP-track
Marie-Laure PotetPotet, Marie-Laure Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG Formally verified hardening of C programs against hardware fault injection
Damien PousPous, Damien CNRS PC Member in Program Committee within the CPP-track
Jonathan ProtzenkoProtzenko, Jonathan Microsoft Azure ResearchUnited States PC Member in Program Committee within the CPP-track
R Emily RiehlRiehl, Emily Johns Hopkins University Prospects for Computer Formalization of Infinite-Dimensional Category Theory
Christine RizkallahRizkallah, Christine University of MelbourneAustralia Formalized Burrows-Wheeler Transform
Jurriaan RotRot, Jurriaan Radboud University Nijmegen Intrinsically Correct Sorting in Cubical Agda
S Teppei SaitoSaito, Teppei Japan Advanced Institute of Science and Technology, Japan An Isabelle formalization of co-rewrite pairs for non-reachability in conditional rewriting
Chuta SanoSano, Chuta McGill UniversityCanada Split Decisions: Explicit Contexts for Substructural Languages
Tetsuya SatoSato, Tetsuya Tokyo Institute of TechnologyJapan Formalization of Differential Privacy in Isabelle/HOL
Mircea SebeSebe, Mircea UIUC Nominal Matching Logic With Fixpoints
Peter SewellSewell, Peter University of CambridgeUnited Kingdom A CHERI C Memory Model for Verified Temporal Safety
Zhong ShaoShao, Zhong Yale UniversityUnited States Committee Member in Steering Committee within the CPP-track
Bas SpittersSpitters, Bas Aarhus University CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
Ian StarkStark, Ian The University of EdinburghUnited Kingdom A CHERI C Memory Model for Verified Temporal Safety
Kathrin StarkStark, Kathrin Heriot-Watt UniversityUnited Kingdom Conference Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
T Nicolas TabareauTabareau, Nicolas InriaFrance Session Chair of Session 1 (part of CPP) Business Meeting PC Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track PC Chair in Program Committee within the CPP-track
Joseph TassarottiTassarotti, Joseph New York UniversityUnited States PC Member in Program Committee within the CPP-track
René ThiemannThiemann, René University of Innsbruck An Isabelle formalization of co-rewrite pairs for non-reachability in conditional rewriting
Amin TimanyTimany, Amin Aarhus UniversityDenmark Conference Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
Laura TitoloTitolo, Laura AMA/NASA LaRCUnited States PC Member in Program Committee within the CPP-track
Dmitriy TraytelTraytel, Dmitriy University of CopenhagenDenmark Committee Member in Steering Committee within the CPP-track
U Dominique UnruhUnruh, Dominique RWTH Aachen Formalizing the One-way to Hiding Theorem Leakage-Free Probabilistic Jasmin Programs
V Niels van der Weidevan der Weide, Niels Radboud University Intrinsically Correct Sorting in Cubical Agda
Simon Friis VindumVindum, Simon Friis Aarhus UniversityDenmark The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
W Conrad WattWatt, Conrad Nanyang Technological UniversitySingapore PC Member in Program Committee within the CPP-track
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States PC Member in Program Committee within the CPP-track
Y Akihisa YamadaYamada, Akihisa National Institute of InformaticsJapan An Isabelle formalization of co-rewrite pairs for non-reachability in conditional rewriting
Irene YoonYoon, Irene France PC Member in Program Committee within the CPP-track
Z Daniel ZackonZackon, Daniel McGill UniversityCanada Split Decisions: Explicit Contexts for Substructural Languages
Yannick ZakowskiZakowski, Yannick InriaFrance Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IR
Vadim ZalivaZaliva, Vadim University of Cambridge, UKUnited States A CHERI C Memory Model for Verified Temporal Safety
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Committee Member in Steering Committee within the CPP-track