CPP 2021 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (141)

A Reynald AffeldtAffeldt, Reynald National Institute of Advanced Industrial Science and Technology (AIST), Japan Committee Member in Program Committee within the CPP -track
Sean AndersonAnderson, Sean Portland State University Towards formally verified compilation of tag-based policy enforcement
June AndronickAndronick, June CSIRO's Data61 and UNSWAustralia Committee Member in Program Committee within the CPP -track Steering Committee Member in Steering Committee within the CPP -track
Danil AnnenkovAnnenkov, Danil Concordium Blockchain Research Center, Aarhus UniversityDenmark Extracting Smart Contracts Tested and Verified in Coq
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Carnegie Mellon University, USAUnited States Committee Member in Program Committee within the CPP -track
B Anindya BanerjeeBanerjee, Anindya IMDEA Software InstituteSpain A Formal Proof of PAC Learnability for Decision Stumps
Heiko BeckerBecker, Heiko MPI-SWSGermany Lassie: HOL4 Tactics by Example
Jesper BengtsonBengtson, Jesper IT University of Copenhagen Machine-Checked Semantic Session Typing
Véronique BenzakenBenzaken, Véronique Université Paris SaclayFrance A Coq Formalization of Data Provenance
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States Chairs' report and community meeting Conference Co-Chair in Organization Committee within the CPP -track
Bruno BernardoBernardo, Bruno Nomadic Labs Formally Verified Decentralized Exchange with Mi-Cho-Coq
Lars BirkedalBirkedal, Lars Aarhus University Contextual Refinement of the Michael-Scott Queue (Proof Pearl) Reasoning About Monotonicity in Separation Logic
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands A Modular Isabelle Framework for Verifying Saturation Provers Steering Committee Member in Steering Committee within the CPP -track
Sören BleikertzBleikertz, Sören Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
Nathaniel BosBos, Nathaniel McGill University Lassie: HOL4 Tactics by Example
Dmitri BoulytchevBoulytchev, Dmitri Saint Petersburg State University / JetBrains ResearchRussia Certified Semantics for miniKanren
Joachim BreitnerBreitner, Joachim DFINITY FoundationGermany Committee Member in Program Committee within the CPP -track
Stefan BrunthalerBrunthaler, Stefan Universität der Bundeswehr MünchenGermany Towards Efficient and Verified Virtual Machines for Dynamic Languages
Pierre-Léo BégayBégay, Pierre-Léo Orange Labs & Verimag Developing and certifying Datalog optimizations in Coq/MathComp
C Jacques CaretteCarette, Jacques McMaster UniversityCanada Formalizing Category Theory in Agda
Harold CarrCarr, Harold Oracle Labs, USAUnited States Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Elliot CattCatt, Elliot ANU On the Formalisation of Kolmogorov Complexity
Raphaël CauderlierCauderlier, Raphaël Nomadic Labs Formally Verified Decentralized Exchange with Mi-Cho-Coq
CHR ChhakChhak, CHR Portland State University Towards formally verified compilation of tag-based policy enforcement
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Steering Committee Member in Steering Committee within the CPP -track
Jesper CockxCockx, Jesper TU DelftNetherlands Session Chair of Proof Tactics (part of CPP ) Committee Member in Program Committee within the CPP -track
Cyril CohenCohen, Cyril Université Côte d’Azur, Inria, France Session Chair of Rewriting and Automated Reasoning (part of CPP ) Committee Member in Program Committee within the CPP -track
Sarah Cohen-BoulakiaCohen-Boulakia, Sarah LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay A Coq Formalization of Data Provenance
Johan CommelinCommelin, Johan Universität Freiburg Formalizing the Ring of Witt Vectors
Evelyne ContejeanContejean, Evelyne CNRS A Coq Formalization of Data Provenance
Pierre CrégutCrégut, Pierre Orange Labs Developing and certifying Datalog optimizations in Coq/MathComp
D Nils Anders DanielssonDanielsson, Nils Anders University of Gothenburg, Chalmers University of Technology Committee Member in Program Committee within the CPP -track
Eva DarulovaDarulova, Eva MPI-SWS Lassie: HOL4 Tactics by Example
Martin DesharnaisDesharnais, Martin Universität der Bundeswehr MünchenGermany Towards Efficient and Verified Virtual Machines for Dynamic Languages
Brijesh DongolDongol, Brijesh University of Surrey Committee Member in Program Committee within the CPP -track
Aaron DutleDutle, Aaron NASA Langley Research CenterUnited States Formal Verification of Semi-algebraic Sets and Real Analytic Functions
F Bertram FelgenhauerFelgenhauer, Bertram A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Amy FeltyFelty, Amy University of OttawaCanada Steering Committee Member in Steering Committee within the CPP -track
Yannick ForsterForster, Yannick Saarland UniversityGermany Session Chair of Logic, Set Theory, and Category Theory (part of CPP ) Committee Member in Program Committee within the CPP -track
Nathan FultonFulton, Nathan IBM Research CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
G Ivan GavranGavran, Ivan MPI-SWS Lassie: HOL4 Tactics by Example
Shilpi GoelGoel, Shilpi Centaur Technology, Inc. Committee Member in Program Committee within the CPP -track
Georges GonthierGonthier, Georges Inria Steering Committee Member in Steering Committee within the CPP -track
Colin GonzálezGonzález, Colin Université de Paris, Irif -- Nomadic Labs Formally Verified Decentralized Exchange with Mi-Cho-Coq
H Max W. HaslbeckHaslbeck, Max W. University of Innsbruck An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR
Jonas Kastberg HinrichsenHinrichsen, Jonas Kastberg IT University of CopenhagenDenmark Machine-Checked Semantic Session Typing
Štěpán HolubHolub, Štěpán Charles UniversityCzechia Formalization of Combinatorics on Words in Isabelle/HOL
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany Session Chair of Invited Talk (part of CPP ) Chairs' report and community meeting Co-chair in Program Committee within the CPP -track PC and Conference Co-Chair in Organization Committee within the CPP -track Steering Committee Member in Steering Committee within the CPP -track
Jason Z.S. HuHu, Jason Z.S. McGill UniversityCanada Formalizing Category Theory in Agda
Chung-Kil HurHur, Chung-Kil Seoul National University, South Korea Committee Member in Program Committee within the CPP -track
J Arvid JakobssonJakobsson, Arvid Nomadic Labs Formally Verified Decentralized Exchange with Mi-Cho-Coq
Moa JohanssonJohansson, Moa Chalmers University of TechnologySweden Committee Member in Program Committee within the CPP -track
K Tobias KappéKappé, Tobias Cornell University Monadic Second-Order Logic and Pomset Languages
Chantal KellerKeller, Chantal LRI, Univ. Paris-SudFrance A Coq Formalization of Data Provenance
Dominik KirstKirst, Dominik Saarland UniversityGermany The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq
Gerwin KleinKlein, Gerwin CSIRO's Data61 and UNSW SydneyAustralia Steering Committee Member in Steering Committee within the CPP -track
Alexander KogtenkovKogtenkov, Alexander Schaffhausen Institute of Technology, SwitzerlandRussia Mechanically-checked soundness of type-based null safety
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University, UK Session Chair of AI and Machine Learning (part of CPP ) Committee Member in Program Committee within the CPP -track
Igor KonnovKonnov, Igor Informal Systems IncAustria Specification and model checking of Tendermint consensus in TLA+
Angeliki Koutsoukou-ArgyrakiKoutsoukou-Argyraki, Angeliki University of Cambridge, Department of Computer Science and TechnologyUnited Kingdom Committee Member in Program Committee within the CPP -track
Robbert KrebbersKrebbers, Robbert Radboud University Nijmegen Machine-Checked Semantic Session Typing
L Olivier LaurentLaurent, Olivier CNRS & ENS LyonFrance An Anti-Locally-Nameless Approach to Formalizing Quantifiers
Meven Lennon-BertrandLennon-Bertrand, Meven Inria – LS2N, Université de NantesFrance Gradualizing the Calculus of Inductive Constructions
Robert Y. LewisLewis, Robert Y. Vrije Universiteit AmsterdamNetherlands Formalizing the Ring of Witt Vectors Committee Member in Program Committee within the CPP -track
Hongjin LiangLiang, Hongjin Nanjing University, ChinaChina Committee Member in Program Committee within the CPP -track
Jannis LimpergLimperg, Jannis Vrije Universiteit AmsterdamNetherlands A Novice-Friendly Induction Tactic for Lean
Andreas LochbihlerLochbihler, Andreas Digital AssetSwitzerland Session Chair of Security, Blockchains, and Smart Contracts (part of CPP ) A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers Committee Member in Program Committee within the CPP -track
Alexander LochmannLochmann, Alexander University of Innsbruck A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Daniël LouwrinkLouwrink, Daniël University of Amsterdam Machine-Checked Semantic Session Typing
Petr LozovLozov, Petr Sain Petersburg State University, SPbGU Certified Semantics for miniKanren
Andreas LööwLööw, Andreas Chalmers University of Technology Lutsig: A Verified Verilog Compiler for Verified Circuit Development
M Assia MahboubiMahboubi, Assia INRIAFrance Steering Committee Member in Steering Committee within the CPP -track
Kenji MaillardMaillard, Kenji Inria Nantes & University of Chile Gradualizing the Calculus of Inductive Constructions
Rupak MajumdarMajumdar, Rupak MPI-SWS Lassie: HOL4 Tactics by Example
Petar MaksimovićMaksimović, Petar Imperial College London, UK Committee Member in Program Committee within the CPP -track
William ManskyMansky, William University of Illinois at ChicagoUnited States Session Chair of Program Logics (part of CPP ) Committee Member in Program Committee within the CPP -track
Ognjen MarićMarić, Ognjen Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
Simon MeierMeier, Simon Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
Aart MiddeldorpMiddeldorp, Aart University of Innsbruck A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Dale MillerMiller, Dale INRIA Saclay and LIXFrance Steering Committee Member in Steering Committee within the CPP -track
Mikkel MiloMilo, Mikkel Concordium Blockchain Research Center, Aarhus University Extracting Smart Contracts Tested and Verified in Coq
Zarko MilosevicMilosevic, Zarko Informal Systems Specification and model checking of Tendermint consensus in TLA+
Victor Cacciari MiraldoMiraldo, Victor Cacciari DFINITY Foundation Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Fabian MitterwallnerMitterwallner, Fabian University of Innsbruck A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Mark MoirMoir, Mark Oracle Labs, New Zealand Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Jean-François MoninMonin, Jean-François Verimag Developing and certifying Datalog optimizations in Coq/MathComp
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology A Minimalistic Verified Bootstrapped Compiler (Proof Pearl) Steering Committee Member in Steering Committee within the CPP -track
Anders MörtbergMörtberg, Anders Department of Mathematics, Stockholm UniversitySweden Committee Member in Program Committee within the CPP -track
N Phoebe NicholsNichols, Phoebe Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
Jakob Botsch NielsenNielsen, Jakob Botsch Concordium Blockchain Research Center, Aarhus University Extracting Smart Contracts Tested and Verified in Coq
Tobias NipkowNipkow, Tobias Technische Universität München Invited Talk: Teaching Algorithms and Data Structures with a Proof Assistant Steering Committee Member in Steering Committee within the CPP -track
Michael NorrishNorrish, Michael Data61, CSIRO & ANUAustralia On the Formalisation of Kolmogorov Complexity
O Sabine OechsnerOechsner, Sabine Aarhus University Formalising MPC-in-the-head-based zero-knowledge
Sam OwreOwre, Sam SRI InternationalUnited States Committee Member in Program Committee within the CPP -track
P Karl PalmskogPalmskog, Karl KTH Royal Institute of TechnologySweden Committee Member in Program Committee within the CPP -track
Mário PereiraPereira, Mário NOVA LINCS & Nova School of Sciences and Tecnhology Cameleer: a Deductive Verification Tool for OCaml
Vasily PestunPestun, Vasily IBM Research; IHES CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Nika PonaPona, Nika Digamma.ai How to verify an ASN.1 Protocol C-language Stack in Coq?
Andrei PopescuPopescu, Andrei University of SheffieldUnited Kingdom Session Chair of Invited Talk (part of CPP ) Chairs' report and community meeting Co-chair in Program Committee within the CPP -track PC Co-Chair in Organization Committee within the CPP -track
Damien PousPous, Damien CNRS Committee Member in Program Committee within the CPP -track
R Tahina RamananandroRamananandro, Tahina Microsoft ResearchUnited States Committee Member in Program Committee within the CPP -track
António RavaraRavara, António Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCSPortugal Cameleer: a Deductive Verification Tool for OCaml
Felix RechRech, Felix Saarland UniversityGermany The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq
Dmitry RozplokhasRozplokhas, Dmitry Saint Petersburg State University and JetBrains Research Certified Semantics for miniKanren
S Matthias SchmalzSchmalz, Matthias Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
Ilya SergeySergey, Ilya Yale-NUS College and National University of SingaporeSingapore Committee Member in Program Committee within the CPP -track
Peter SewellSewell, Peter University of Cambridge Invited Talk: Underpinning the foundations: Sail-based semantics, testing, and reasoning, for production and CHERI-enabled architectures
Natarajan ShankarShankar, Natarajan SRI International, USA Session Chair of Lightning Talks (part of CPP ) Committee Member in Program Committee within the CPP -track
Zhong ShaoShao, Zhong Yale University Steering Committee Chair in Steering Committee within the CPP -track
Avraham ShinnarShinnar, Avraham IBM Research CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Nikolaj SidorencoSidorenco, Nikolaj Aarhus University Formalising MPC-in-the-head-based zero-knowledge
Lisandra SilvaSilva, Lisandra University of Minho Formal Verification of Authenticated, Append-Only Skip Lists in Agda
J Tanner SlagelSlagel, J Tanner NASA Langley Research CenterUnited States Formal Verification of Semi-algebraic Sets and Real Analytic Functions
Bas SpittersSpitters, Bas Concordium Blockchain Research Center, Aarhus University Extracting Smart Contracts Tested and Verified in Coq Formalising MPC-in-the-head-based zero-knowledge
Kathrin StarkStark, Kathrin Princeton University, USAUnited States Committee Member in Program Committee within the CPP -track
Štěpán StarostaStarosta, Štěpán Faculty of Information Technology, Czech Technical University in PragueCzechia Formalization of Combinatorics on Words in Isabelle/HOL
Guy L. Steele Jr.Steele Jr., Guy L. Oracle LabsUnited States Formal Verification of Authenticated, Append-Only Skip Lists in Agda
T Nicolas TabareauTabareau, Nicolas InriaFrance Gradualizing the Calculus of Inductive Constructions
Éric TanterTanter, Éric University of Chile Gradualizing the Calculus of Inductive Constructions
Joseph TassarottiTassarotti, Joseph Boston College A Formal Proof of PAC Learnability for Decision Stumps
René ThiemannThiemann, René University of Innsbruck An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR Committee Member in Program Committee within the CPP -track
Amin TimanyTimany, Amin Aarhus UniversityDenmark Session Chair of Formalized Mathematics (part of CPP ) Reasoning About Monotonicity in Separation Logic Committee Member in Program Committee within the CPP -track
Andrew TolmachTolmach, Andrew Portland State University Towards formally verified compilation of tag-based policy enforcement
Sophie TourretTourret, Sophie Max Planck Institute for Informatics A Modular Isabelle Framework for Verifying Saturation Provers
Barry TragerTrager, Barry IBM Research CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Jean-Baptiste TristanTristan, Jean-Baptiste Boston CollegeUnited States A Formal Proof of PAC Learnability for Decision Stumps
U Josef UrbanUrban, Josef Czech Technical University in PragueCzechia Committee Member in Program Committee within the CPP -track
V Koundinya VajjhaVajjha, Koundinya University of Pittsburgh CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq A Formal Proof of PAC Learnability for Decision Stumps
Floris van Doornvan Doorn, Floris University of PittsburghUnited States Committee Member in Program Committee within the CPP -track
Ratko G. VeprekVeprek, Ratko G. Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
Simon Friis VindumVindum, Simon Friis Aarhus UniversityDenmark Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
Andrey VyatkinVyatkin, Andrey Saint Petersburg State University Certified Semantics for miniKanren
W Mark WassellWassell, Mark University of Cambridge Formalising MiniSail in Isabelle
Christoph WeidenbachWeidenbach, Christoph MPI-INFGermany Committee Member in Program Committee within the CPP -track
Lauren WhiteWhite, Lauren Kansas State UniversityUnited States Formal Verification of Semi-algebraic Sets and Real Analytic Functions
Josef WidderWidder, Josef Informal Systems Specification and model checking of Tendermint consensus in TLA+
Freek WiedijkWiedijk, Freek Radboud University NijmegenNetherlands Session Chair of Compilers and Interpreters (part of CPP ) Committee Member in Program Committee within the CPP -track
Z Yannick ZakowskiZakowski, Yannick InriaFrance Session Chair of Semantics (part of CPP ) Committee Member in Program Committee within the CPP -track
Vadim ZalivaZaliva, Vadim Carnegie Mellon University, USAUnited States How to verify an ASN.1 Protocol C-language Stack in Coq?
Rébecca ZucchiniZucchini, Rébecca LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay A Coq Formalization of Data Provenance
Å Johannes Åman PohjolaÅman Pohjola, Johannes Data61 at CSIRO / UNSW Committee Member in Program Committee within the CPP -track