CPP 2023 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (126)

A Reynald AffeldtAffeldt, Reynald National Institute of Advanced Industrial Science and Technology (AIST)Japan Semantics of Probabilistic Programs using S-Finite Kernels in Coq Committee Member in Program Committee within the CPP-track
Xavier AllamigeonAllamigeon, Xavier Inria and Ecole Polytechnique A Formal Disproof of Hirsch Conjecture
Danil AnnenkovAnnenkov, Danil ConcordiumDenmark Formalising Decentralised Exchanges in Coq
Arvind ArasuArasu, Arvind Microsoft Research FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Luca ArnaboldiArnaboldi, Luca The University of EdinburghUnited Kingdom Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively
Parsia AtaeiAtaei, Parsia Cornell University P4Cub: A Little Language for Big Routers
Robert AtkeyAtkey, Robert University of Strathclyde Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively
B Anne BaanenBaanen, Anne Vrije Universiteit Amsterdam Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Mantas BakšysBakšys, Mantas University of Cambridge A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States Committee Member in Steering Committee within the CPP-track
Alex BestBest, Alex Vrije Universiteit AmsterdamNetherlands Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands Committee Member in Steering Committee within the CPP-track
Sandrine BlazyBlazy, Sandrine University of Rennes; Inria; CNRS; IRISAFrance CompCert: a journey through the landscape of mechanized semantics for verified compilation Mechanised Semantics for Gated Static Single Assignment
Valentin BlotBlot, Valentin LMF, Inria, Université Paris-Saclay Compositional pre-processing for automated reasoning in dependent type theory
Anthony BordgBordg, Anthony University of Cambridge Encoding Dependently-Typed Constructions into Simple Type Theory
C Eric CampbellCampbell, Eric Cornell UniversityUnited States P4Cub: A Little Language for Big Routers
Quentin CanuCanu, Quentin Inria and Ecole Polytechnique A Formal Disproof of Hirsch Conjecture
Tej ChajedChajed, Tej VMware ResearchUnited States Committee Member in Program Committee within the CPP-track
John ChenChen, John Cornell UniversityUnited States P4Cub: A Little Language for Big Routers
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Session Chair of Formalized Mathematics I (part of CPP) Committee Member in Steering Committee within the CPP-track
Koen ClaessenClaessen, Koen Chalmers University of TechnologySweden Committee Member in Program Committee within the CPP-track
Ranald CloustonClouston, Ranald ANUAustralia Committee Member in Program Committee within the CPP-track
Joshua CluneClune, Joshua Carnegie Mellon University A Formalized Reduction of Keller's Conjecture
Cyril CohenCohen, Cyril Inria Semantics of Probabilistic Programs using S-Finite Kernels in Coq
Nirvana CoppolaCoppola, Nirvana Vrije Universiteit Amsterdam Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Denis CousineauCousineau, Denis Mitsubishi Electric R&D Centre Europe Compositional pre-processing for automated reasoning in dependent type theory
Enzo CranceCrance, Enzo Mitsubishi Electric R&D Centre EuropeFrance Compositional pre-processing for automated reasoning in dependent type theory
D Matthew L. DaggittDaggitt, Matthew L. Heriott-Watt University Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively
Sander R. DahmenDahmen, Sander R. Vrije Universiteit Amsterdam Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Leonardo de Mourade Moura, Leonardo Microsoft ResearchUnited States Committee Member in Program Committee within the CPP-track
Louise Dubois de Prisquede Prisque, Louise Dubois LMF, Inria, Université Paris-Saclay Compositional pre-processing for automated reasoning in dependent type theory
Rémy DegenneDegenne, Rémy Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9198-CRIStAL, F-59000 Lille, France A formalization of Doob's martingale convergence theorems in mathlib
Antoine Delignat-LavaudDelignat-Lavaud, Antoine Microsoft Research, n.n. ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER
Delphine DemangeDemange, Delphine Univ Rennes, Inria, CNRS, IRISAFrance Mechanised Semantics for Gated Static Single Assignment
Ryan DoengesDoenges, Ryan Cornell UniversityUnited States P4Cub: A Little Language for Big Routers
E Chelsea EdmondsEdmonds, Chelsea University of CambridgeUnited Kingdom A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
F Xinyu FengFeng, Xinyu Nanjing UniversityChina Committee Member in Program Committee within the CPP-track
Denis FirsovFirsov, Denis Tallinn University of TechnologyEstonia Committee Member in Program Committee within the CPP-track
Yannick ForsterForster, Yannick InriaFrance A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl) Committee Member in Program Committee within the CPP-track
Nate FosterFoster, Nate Cornell UniversityUnited States P4Cub: A Little Language for Big Routers
Cédric FournetFournet, Cédric Microsoft Research ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER
Aymeric FromherzFromherz, Aymeric InriaFrance FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Michael FärberFärber, Michael Universität Innsbruck, AustriaAustria Terms for Efficient Proof Checking and Parsing
Hugo FéréeFérée, Hugo Université Paris Cité / IRIFUnited Kingdom Formalizing and computing propositional quantifiers
G Milos GligoricGligoric, Milos University of Texas at AustinUnited States Committee Member in Program Committee within the CPP-track
Georges GonthierGonthier, Georges InriaFrance Committee Member in Steering Committee within the CPP-track
Stephane Graham-LengrandGraham-Lengrand, Stephane SRIUnited States Committee Member in Program Committee within the CPP-track
Benjamin GregoireGregoire, Benjamin INRIA Practical and sound equality tests, automatically
Elsa GunterGunter, Elsa University of IllinoisUnited States Committee Member in Program Committee within the CPP-track
H Asta Halkjær FromHalkjær From, Asta Technical University of Denmark Aesop: White-Box Best-First Proof Search for Lean
Chris HawblitzelHawblitzel, Chris Microsoft ResearchUnited States Committee Member in Program Committee within the CPP-track
Ian J. HayesHayes, Ian J. The University of QueenslandAustralia Verifying term graph optimizations using Isabelle/HOL
Yann HerklotzHerklotz, Yann Imperial College LondonUnited Kingdom Mechanised Semantics for Gated Static Single Assignment
Kesha HietalaHietala, Kesha University of MarylandUnited States FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany Steering Committee Chair in Steering Committee within the CPP-track
I Natalie IsakIsak, Natalie Microsoft P4Cub: A Little Language for Big Routers
J Felix JahnJahn, Felix Saarland University A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
K Cezary KaliszykKaliszyk, Cezary University of Innsbruck Improved Assistance for Interactive Proof
Chantal KellerKeller, Chantal LRI, Université Paris-SudFrance Compositional pre-processing for automated reasoning in dependent type theory
Chantal KellerKeller, Chantal Université Paris SaclayFrance Committee Member in Program Committee within the CPP-track
Marie KerjeanKerjean, Marie CNRS, Université Sorbonne Paris NordFrance Committee Member in Program Committee within the CPP-track
Yoonseung KimKim, Yoonseung Yale UniversityUnited States Session Chair of Applications (part of CPP) Committee Member in Program Committee within the CPP-track
Gerwin KleinKlein, Gerwin CSIRO's Data61 and UNSW SydneyAustralia Committee Member in Steering Committee within the CPP-track
Christina KohlKohl, Christina University of Innsbruck A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Wen KokkeKokke, Wen University of Strathclyde Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively
Ekaterina KomandantskayaKomandantskaya, Ekaterina Heriot-Watt University, UKUnited Kingdom Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively
Katherine KosaianKosaian, Katherine Carnegie Mellon University A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Angeliki Koutsoukou-ArgyrakiKoutsoukou-Argyraki, Angeliki University of Cambridge, Department of Computer Science and TechnologyUnited Kingdom A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands Session Chair of Logical Foundations (part of CPP) Conference Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
L Thomas LamiauxLamiaux, Thomas University of Paris-Saclay, Ens Paris-Saclay Computing Cohomology Rings in Cubical Agda
Jannis LimpergLimperg, Jannis Vrije Universiteit AmsterdamNetherlands Aesop: White-Box Best-First Proof Search for Lean
Axel LjungströmLjungström, Axel Stockholm University Computing Cohomology Rings in Cubical Agda
Jean-Christophe LéchenetLéchenet, Jean-Christophe Université Côte d’Azur, Inria Practical and sound equality tests, automatically
M Assia MahboubiMahboubi, Assia INRIAFrance Compositional pre-processing for automated reasoning in dependent type theory
Kenji MaillardMaillard, Kenji Inria NantesFrance Committee Member in Program Committee within the CPP-track
Patrick MassotMassot, Patrick Formalising the h-principle and sphere eversion
Adrián Doña MateoMateo, Adrián Doña The University of Edinburgh Encoding Dependently-Typed Constructions into Simple Type Theory
Bhavik MehtaMehta, Bhavik University of Cambridge Formalising Sharkovsky's Theorem (Proof Pearl)
Aart MiddeldorpMiddeldorp, Aart University of Innsbruck A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Dale MillerMiller, Dale Inria & École PolytechniqueFrance Committee Member in Steering Committee within the CPP-track
César MuñozMuñoz, César Amazon Web ServicesUnited States Committee Member in Program Committee within the CPP-track
Anders MörtbergMörtberg, Anders Department of Mathematics, Stockholm UniversitySweden Computing Cohomology Rings in Cubical Agda
N Oliver NashNash, Oliver Imperial College, London Formalising the h-principle and sphere eversion
Haobin NiNi, Haobin Cornell University ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER
Eske Hoy NielsenNielsen, Eske Hoy Aarhus University Formalising Decentralised Exchanges in Coq
Tobias NipkowNipkow, Tobias Technische Universität MünchenGermany Committee Member in Program Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
P Bryan ParnoParno, Bryan Carnegie Mellon UniversityUnited States FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Lawrence PaulsonPaulson, Lawrence University of CambridgeUnited Kingdom Committee Member in Program Committee within the CPP-track
Rudy PetersonPeterson, Rudy Cornell University P4Cub: A Little Language for Big Routers
Anja Petković KomelPetković Komel, Anja TU Wien, ViennaAustria Committee Member in Program Committee within the CPP-track
Brigitte PientkaPientka, Brigitte McGill UniversityCanada Session Chair of Business Meeting (part of CPP) Session Chair of Proof Search (part of CPP) PC Chair in Program Committee within the CPP-track PC Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
Clément Pit-ClaudelPit-Claudel, Clément EPFL / AWSUnited States Committee Member in Program Committee within the CPP-track
André PlatzerPlatzer, André Karlsruhe Institute of Technology A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Andrei PopescuPopescu, Andrei University of SheffieldUnited Kingdom Committee Member in Steering Committee within the CPP-track
Pierre-Marie PédrotPédrot, Pierre-Marie INRIAFrance Committee Member in Program Committee within the CPP-track
R Ravi RamamurthyRamamurthy, Ravi Microsoft Research FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Tahina RamananandroRamananandro, Tahina Microsoft ResearchUnited States ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Aseem RastogiRastogi, Aseem Microsoft ResearchIndia FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Christine RizkallahRizkallah, Christine University of MelbourneAustralia Committee Member in Program Committee within the CPP-track
Cody RouxRoux, Cody AWSUnited States Session Chair of Languages and Compilers (part of CPP) Committee Member in Program Committee within the CPP-track
S Ayumu SaitoSaito, Ayumu Tokyo Institute of Technology Semantics of Probabilistic Programs using S-Finite Kernels in Coq
Kazuhiko SakaguchiSakaguchi, Kazuhiko InriaFrance Committee Member in Program Committee within the CPP-track
Zhong ShaoShao, Zhong Yale UniversityUnited States Committee Member in Steering Committee within the CPP-track
Calvin ShyuShyu, Calvin Cornell University P4Cub: A Little Language for Big Routers
Anna SlobodovaSlobodova, Anna IntelUnited States Committee Member in Program Committee within the CPP-track
Gert SmolkaSmolka, Gert Saarland University A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Bas SpittersSpitters, Bas Concordium Blockchain Research Center, Aarhus University Formalising Decentralised Exchanges in Coq
Pierre-Yves StrubStrub, Pierre-Yves MetaFrance A Formal Disproof of Hirsch Conjecture
Aaron StumpStump, Aaron University of IowaUnited States Committee Member in Program Committee within the CPP-track
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
T Yong Kiam TanTan, Yong Kiam Carnegie Mellon University A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Enrico TassiTassi, Enrico INRIAFrance Practical and sound equality tests, automatically
René ThiemannThiemann, René University of InnsbruckAustria Committee Member in Program Committee within the CPP-track
Amin TimanyTimany, Amin Aarhus UniversityDenmark Committee Member in Program Committee within the CPP-track
Dmitriy TraytelTraytel, Dmitriy University of CopenhagenDenmark Session Chair of Practical Proving (part of CPP) Conference Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
U Josef UrbanUrban, Josef Czech Technical University in PragueCzechia Committee Member in Program Committee within the CPP-track
Mark UttingUtting, Mark The University of QueenslandAustralia Verifying term graph optimizations using Isabelle/HOL
V Viktor VafeiadisVafeiadis, Viktor MPI-SWSGermany Session Chair of Formalized Mathematics II (part of CPP) Committee Member in Program Committee within the CPP-track
Floris van Doornvan Doorn, Floris University of PittsburghUnited States Formalising the h-principle and sphere eversion
Sam van Goolvan Gool, Sam Université Paris Cité / IRIF Formalizing and computing propositional quantifiers
Pierre VialVial, Pierre Inria Compositional pre-processing for automated reasoning in dependent type theory
W Yuting WangWang, Yuting Shanghai Jiao Tong UniversityChina Committee Member in Program Committee within the CPP-track
Brae J. WebbWebb, Brae J. The University of QueenslandAustralia Verifying term graph optimizations using Isabelle/HOL
Tjark WeberWeber, Tjark Uppsala UniversitySweden Committee Member in Program Committee within the CPP-track
Y Kexing YingYing, Kexing University of Cambridge A formalization of Doob's martingale convergence theorems in mathlib
Z Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Session Chair of CompCert and Beyond (part of CPP) Session Chair of Business Meeting (part of CPP) PC Chair in Program Committee within the CPP-track PC Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track