CPP 2024 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (104)

A Arthur AdjedjAdjedj, Arthur ENS Paris Saclay, Université Paris-Saclay Martin-Löf à la Coq
Benedikt AhrensAhrens, Benedikt Delft University of TechnologyNetherlands Univalent Double Categories Displayed Monoidal Categories for the Semantics of Linear Logic PC Member in Program Committee within the CPP-track
Zhendong AngAng, Zhendong National University of Singapore Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Andrew W. AppelAppel, Andrew W. Princeton University VCFloat2: Floating-point error analysis in Coq
Robert AtkeyAtkey, Robert University of Strathclyde Session Chair of Formalizations of Category Theory (part of CPP) PC Member in Program Committee within the CPP-track
Jeremy AvigadAvigad, Jeremy Carnegie Mellon University, USA PC Member in Program Committee within the CPP-track
B Mireia González BedmarBedmar, Mireia González University of Barcelona and Formal Vindications S.L. UTC time, formally verified
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States Compositional Verification of Concurrent C Programs with Search Structure Templates Steering Committee Member in Steering Committee within the CPP-track
Frédéric BessonBesson, Frédéric INRIA PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
Sandrine BlazyBlazy, Sandrine University of RennesFrance Session Chair of Business Meeting (part of CPP) Session Chair of Logic and Beyond (part of CPP) PC Chair in Program Committee within the CPP-track Committee Member in Steering Committee within the CPP-track PC Chair in Organizing Committee within the CPP-track
Thomas BourgeatBourgeat, Thomas EPFL PC Member in Program Committee within the CPP-track
Joaquim Casals BuñuelBuñuel, Joaquim Casals University of Barcelona and Formal Vindications S.L. UTC time, formally verified
C Jacques CaretteCarette, Jacques McMaster UniversityCanada PC Member in Program Committee within the CPP-track
Arthur CharguéraudCharguéraud, Arthur InriaFrance Session Chair of Verified Compilation (part of CPP) PC Member in Program Committee within the CPP-track
Clément ChavanonChavanon, Clément INRIA PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Committee Member in Steering Committee within the CPP-track
Jesper CockxCockx, Jesper Delft University of TechnologyNetherlands PC Member in Program Committee within the CPP-track
Évelyne ContejeanContejean, Évelyne CNRS, ENS Paris-Saclay & Université Paris-Saclay PC Member in Program Committee within the CPP-track
D Ana de Almeida Borgesde Almeida Borges, Ana University of Barcelona and Formal Vindications S.L. UTC time, formally verified
María Inés de Frutos-Fernándezde Frutos-Fernández, María Inés Universidad Autónoma de Madrid A Formalization of Complete Discrete Valuation Rings and Local Fields
E Gabriel EbnerEbner, Gabriel Microsoft Research Lean Formalization of Extended Regular Expression Matching with Lookarounds
Chelsea EdmondsEdmonds, Chelsea University of SheffieldUnited Kingdom Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
Andres ErbsenErbsen, Andres PC Member in Program Committee within the CPP-track
Joseph EremondiEremondi, Joseph University of ReginaCanada Strictly Monotone Brouwer Trees for Well Founded Recursion Over Multiple Arguments
F Francisco FerreiraFerreira, Francisco Royal Holloway, University of London PC Member in Program Committee within the CPP-track
G Siddhartha GadgilGadgil, Siddhartha Indian Institute of Science Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture
Georges GonthierGonthier, Georges Inria Steering Committee Member in Steering Committee within the CPP-track
H Lasse Letager HansenHansen, Lasse Letager Aarhus University The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. HaselwarterHaselwarter, Philipp G. Aarhus UniversityDenmark The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Kesha HietalaHietala, Kesha Amazon Web ServicesUnited States PC Member in Program Committee within the CPP-track
Nao HirokawaHirokawa, Nao Japan Advanced Institute of Science and Technology Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Kuen-Bang Hou (Favonia)Hou (Favonia), Kuen-Bang University of MinnesotaUnited States Session Chair of Formalizing Mathematics (part of CPP) PC Member in Program Committee within the CPP-track
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography Steering Committee Chair in Steering Committee within the CPP-track
Benjamin Salling HvassHvass, Benjamin Salling Aarhus University The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
J Joost J. JoostenJoosten, Joost J. University of Barcelona UTC time, formally verified
K Cezary KaliszykKaliszyk, Cezary University of Innsbruck Improved Assistance for Interactive Proof
Ariel E. KellisonKellison, Ariel E. Cornell UniversityUnited States VCFloat2: Floating-point error analysis in Coq
Dohan KimKim, Dohan University of Innsbruck Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Dominik KirstKirst, Dominik Ben-Gurion University of the Negev A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic
Gerwin KleinKlein, Gerwin Proofcraft and UNSW SydneyAustralia Committee Member in Steering Committee within the CPP-track
Hsiang-Shang ‘Josh’ KoKo, Hsiang-Shang ‘Josh’ Institute of Information Science, Academia SinicaTaiwan PC Member in Program Committee within the CPP-track
Wen KokkeKokke, Wen University of Edinburgh PC Member in Program Committee within the CPP-track
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands Unification for Subformula Linking under Quantifiers Steering Committee Member in Steering Committee within the CPP-track
Nikolai KudasovKudasov, Nikolai Innopolis UniversityRussia Formalizing the ∞-categorical Yoneda lemma
L Peter LammichLammich, Peter The University of Manchester PC Member in Program Committee within the CPP-track
Meven Lennon-BertrandLennon-Bertrand, Meven University of CambridgeUnited Kingdom Martin-Löf à la Coq
Sarah LoosLoos, Sarah Google PC Member in Program Committee within the CPP-track
M Kenji MaillardMaillard, Kenji INRIAFrance Martin-Löf à la Coq
William ManskyMansky, William University of Illinois ChicagoUnited States Compositional Verification of Concurrent C Programs with Search Structure Templates
Umang MathurMathur, Umang National University of SingaporeSingapore Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Ralph MatthesMatthes, Ralph IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse Displayed Monoidal Categories for the Semantics of Linear Logic
Dale MillerMiller, Dale INRIA Saclay and LIX/Institut Polytechnique de ParisFrance Steering Committee Member in Steering Committee within the CPP-track
Alberto MomiglianoMomigliano, Alberto Università degli Studi di Milano PC Member in Program Committee within the CPP-track
David MonniauxMonniaux, David Université Grenoble Alpes - CNRS - Grenoble INP - VerimagFrance Memory simulations, security and optimization in a verified compiler
Ike MulderMulder, Ike Radboud University NijmegenNetherlands Unification for Subformula Linking under Quantifiers
Cesar MunozMunoz, Cesar NASAUnited States A Temporal Differential Dynamic Logic Formal Embedding
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology PC Member in Program Committee within the CPP-track
N Duc-Than NguyenNguyen, Duc-Than University of Illinois at ChicagoUnited States Compositional Verification of Concurrent C Programs with Search Structure Templates
Tobias NipkowNipkow, Tobias Technische Universität München Steering Committee Member in Steering Committee within the CPP-track
Michael NorrishNorrish, Michael Australian National UniversityAustralia PC Member in Program Committee within the CPP-track
Paige Randall NorthNorth, Paige Randall Utrecht University Univalent Double Categories PC Member in Program Committee within the CPP-track
Filippo Alberto Edoardo Nuccio Mortarino Majno di CapriglioNuccio Mortarino Majno di Capriglio, Filippo Alberto Edoardo Université Jean Monnet Saint-ÉtienneFrance A Formalization of Complete Discrete Valuation Rings and Local Fields
P Christine Paulin-MohringPaulin-Mohring, Christine Université Paris-Saclay PC Member in Program Committee within the CPP-track
Lawrence PaulsonPaulson, Lawrence University of CambridgeUnited Kingdom Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
Brigitte PientkaPientka, Brigitte McGill UniversityCanada Session Chair of Business Meeting (part of CPP) Session Chair of Interactive Proof Development (part of CPP) PC Chair in Program Committee within the CPP-track Steering Committee Member in Steering Committee within the CPP-track PC Chair in Organizing Committee within the CPP-track
Andrei PopescuPopescu, Andrei University of SheffieldUnited Kingdom Steering Committee Member in Steering Committee within the CPP-track
Loïc PujetPujet, Loïc Stockholm University Martin-Löf à la Coq
Pierre-Marie PédrotPédrot, Pierre-Marie INRIAFrance Martin-Löf à la Coq
George PîrleaPîrlea, George National University of Singapore Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
R Azalea RaadRaad, Azalea Imperial College LondonUnited Kingdom Under-approximation for Scalable Bug Detection
Tahina RamananandroRamananandro, Tahina Microsoft ResearchUnited States PC Member in Program Committee within the CPP-track
Nima RasekhRasekh, Nima Max Planck Institute for MathematicsGermany Univalent Double Categories
Eduardo Hermo ReyesReyes, Eduardo Hermo University of Barcelona and Formal Vindications S.L. UTC time, formally verified
Emily RiehlRiehl, Emily Johns Hopkins University Formalizing the ∞-categorical Yoneda lemma
Juan Conejero RodríguezRodríguez, Juan Conejero University of Barcelona and Formal Vindications S.L. UTC time, formally verified
Philipp RuemmerRuemmer, Philipp University of Regensburg and Uppsala UniversityGermany PC Member in Program Committee within the CPP-track
S Ilya SergeySergey, Ilya National University of SingaporeSingapore Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Zhong ShaoShao, Zhong Yale UniversityUnited States Steering Committee Member in Steering Committee within the CPP-track
Ian ShillitoShillito, Ian Australian National University A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic
Kiraku ShintaniShintani, Kiraku Japan Advanced Institute of Science and Technology Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
J Tanner SlagelSlagel, J Tanner NASA A Temporal Differential Dynamic Logic Formal Embedding
Bas SpittersSpitters, Bas Aarhus University The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Bas SpittersSpitters, Bas Aarhus UniversityDenmark PC Member in Program Committee within the CPP-track
T Anand Rao TadipatriTadipatri, Anand Rao Indian Institute of Science Education and Research Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture
Yong Kiam TanTan, Yong Kiam *Institute for Infocomm Research, ASTAR** PC Member in Program Committee within the CPP-track
Enrico TassiTassi, Enrico INRIAFrance PC Member in Program Committee within the CPP-track
René ThiemannThiemann, René University of Innsbruck Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Amin TimanyTimany, Amin Aarhus UniversityDenmark Session Chair of Business Meeting (part of CPP) Session Chair of Mechanized separation logic (part of CPP) Business Meeting Steering Committee Member in Steering Committee within the CPP-track Conference Chair in Organizing Committee within the CPP-track
Laura TitoloTitolo, Laura AMA/NASA LaRCUnited States A Temporal Differential Dynamic Logic Formal Embedding
Alwen TiuTiu, Alwen The Australian National University PC Member in Program Committee within the CPP-track
Dmitriy TraytelTraytel, Dmitriy University of CopenhagenDenmark Session Chair of Business Meeting (part of CPP) Session Chair of Isabelle, PVS (part of CPP) Business Meeting Steering Committee Member in Steering Committee within the CPP-track Conference Chair in Organizing Committee within the CPP-track
Jean-Baptiste TristanTristan, Jean-Baptiste Amazon Web ServicesUnited States PC Member in Program Committee within the CPP-track
Ninet TristanTristan, Ninet Thales PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
V Niels van der Weidevan der Weide, Niels Radboud University Univalent Double Categories Displayed Monoidal Categories for the Semantics of Linear Logic
Margus VeanesVeanes, Margus Microsoft Research Lean Formalization of Extended Regular Expression Matching with Lookarounds
W Shengyi WangWang, Shengyi Princeton University, USA Compositional Verification of Concurrent C Programs with Search Structure Templates
Jonathan WeinbergerWeinberger, Jonathan Johns Hopkins University Formalizing the ∞-categorical Yoneda lemma
Lauren WhiteWhite, Lauren NASAUnited States A Temporal Differential Dynamic Logic Formal Embedding
Théo WinterhalterWinterhalter, Théo INRIA SaclayFrance The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography PC Member in Program Committee within the CPP-track
Kobe WullaertWullaert, Kobe Delft University of Technology Displayed Monoidal Categories for the Semantics of Linear Logic
Z Vadim ZalivaZaliva, Vadim University of Cambridge, UKUnited States Session Chair of Compiler / Program Verification (part of CPP) PC Member in Program Committee within the CPP-track
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Steering Committee Member in Steering Committee within the CPP-track
Qiyuan ZhaoZhao, Qiyuan National University of SingaporeSingapore Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Ekaterina ZhuchkoZhuchko, Ekaterina Tallinn University of Technology Lean Formalization of Extended Regular Expression Matching with Lookarounds