CPP 2020 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (101)

A Johannes AltmanningerAltmanninger, Johannes TU Wien Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs
Nada AminAmin, Nada Harvard UniversityUnited States Committee Member in Program Committee within the CPP-track
Danil AnnenkovAnnenkov, Danil Concordium Blockchain Research Center, Aarhus UniversityDenmark ConCert: A Smart Contract Certification Framework in Coq
Jesús AransayAransay, Jesús Universidad de la Rioja, Spain Committee Member in Program Committee within the CPP-track
David AspinallAspinall, David University of Edinburgh Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL
Mauricio Ayala-RinconAyala-Rincon, Mauricio University of BrasíliaBrazil Committee Member in Program Committee within the CPP-track
B Casper BachBach, Casper Delft University of Technology Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
Yves BertotBertot, Yves INRIAFrance Session Chair of Proof engineering and user interaction (part of CPP)
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands Session Chair of Invited talk (part of CPP) PC Chairs' report Program Co-Chair in Program Committee within the CPP-track
Clément BlaudeauBlaudeau, Clément Ecole PolytechniqueFrance A Verified Packrat Parser Interpreter for Parsing Expression Grammars
Chad BrownBrown, Chad Czech Technical University in Prague Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Ahto BuldasBuldas, Ahto Tallinn University of Technology Verified Security of BLT Signature Scheme
David ButlerButler, David Alan Turing Institute Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL
Kevin BuzzardBuzzard, Kevin Imperial College London Formalising perfectoid spaces
C Xiaohong ChenChen, Xiaohong University of Illinois at Urbana-ChampaignUnited States Invited talk: Matching Logic: The Foundation of the K Framework
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Session Chair of Verified cryptography (part of CPP) Invited talk: Proof Assistants at the Hardware-Software Interface
Liron CohenCohen, Liron Ben-Gurion University of the NegevIsrael Committee Member in Program Committee within the CPP-track
Johan CommelinCommelin, Johan Universität Freiburg Formalising perfectoid spaces
D Dominique DevrieseDevriese, Dominique Vrije Universiteit BrusselBelgium Committee Member in Program Committee within the CPP-track
Christian DoczkalDoczkal, Christian Université Côte d'Azur Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
Tomás DíazDíaz, Tomás IMFD Chile A Mechanized Formalization of GraphQL
F Jean-Christophe FilliatreFilliatre, Jean-Christophe CNRS, ParisFrance Committee Member in Program Committee within the CPP-track
Denis FirsovFirsov, Denis Guardtime ASEstonia Verified Security of BLT Signature Scheme
Yannick ForsterForster, Yannick Saarland UniversityGermany Verified Programming of Turing Machines in Coq Coq à la Carte - A Practical Approach to Modular Syntax with Binders Undecidability of Higher-Order Unification Formalised in Coq
G Adria GasconGascon, Adria Alan Turing Institute Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL
Neil GhaniGhani, Neil University of Strathclyde Three equivalent ordinal notation systems in Cubical Agda
Shilpi GoelGoel, Shilpi Centaur Technology, Inc. Verifying x86 Instruction Implementations
Adam GrabowskiGrabowski, Adam University of BialystokPoland Committee Member in Program Committee within the CPP-track
Dan GrossmanGrossman, Dan University of WashingtonUnited States REPLICA: REPL Instrumentation for Coq Analysis
H Jesse Michael HanHan, Jesse Michael University of Pittsburgh A Formal Proof of the Independence of the Continuum Hypothesis
Paul HeHe, Paul University of PennsylvaniaUnited States An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Aquinas HoborHobor, Aquinas National University of Singapore A Functional Proof Pearl: Inverting the Ackermann Hierarchy
Cătălin HriţcuHriţcu, Cătălin Inria ParisFrance Session Chair of Invited talk (part of CPP) PC Chairs' report Program Co-Chair in Program Committee within the CPP-track
Warren HuntHunt, Warren University of Texas Committee Member in Program Committee within the CPP-track
Chung-Kil HurHur, Chung-Kil Seoul National UniversityKorea, South An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
I Fabian ImmlerImmler, Fabian Carnegie Mellon University The Poincaré-Bendixson Theorem in Isabelle/HOL
K Cezary KaliszykKaliszyk, Cezary University of Innsbruck Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Robbert KrebbersKrebbers, Robbert Delft University of TechnologyNetherlands Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
Fabian KunzeKunze, Fabian Saarland University Verified Programming of Turing Machines in Coq
L Risto LaanojaLaanoja, Risto Guardtime AS Verified Security of BLT Signature Scheme
Ori LahavLahav, Ori Tel Aviv University Session Chair of Automated verification and SAT solving (part of CPP) Committee Member in Program Committee within the CPP-track
Peter LammichLammich, Peter The University of Manchester Committee Member in Program Committee within the CPP-track
Dominique Larchey-WendlingLarchey-Wendling, Dominique CNRS, LORIAFrance Committee Member in Program Committee within the CPP-track
Sorin LernerLerner, Sorin University of California, San Diego REPLICA: REPL Instrumentation for Coq Analysis
Thomas LetanLetan, Thomas ANSSI FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
Robert Y. LewisLewis, Robert Y. Vrije Universiteit AmsterdamNetherlands Session Chair of Formalized mathematics 1 (part of CPP)
Hongjin LiangLiang, Hongjin Nanjing University, ChinaChina Committee Member in Program Committee within the CPP-track
M Assia MahboubiMahboubi, Assia INRIAFrance Committee Member in Program Committee within the CPP-track
Patrick MassotMassot, Patrick Université Paris Sud Formalising perfectoid spaces
Anshuman MohanMohan, Anshuman National University of SingaporeSingapore A Functional Proof Pearl: Inverting the Ackermann Hierarchy
Cesar MunozMunoz, Cesar NASAUnited States Committee Member in Program Committee within the CPP-track
Anders MörtbergMörtberg, Anders Department of Mathematics, Stockholm UniversitySweden Cubical Synthetic Homotopy Theory
N Raja NatarajanNatarajan, Raja Tata Institute of Fundamental Research Mumbai A Constructive Formalization of the Weak Perfect Graph Theorem
Jakob Botsch NielsenNielsen, Jakob Botsch Concordium Blockchain Research Center, Aarhus University ConCert: A Smart Contract Certification Framework in Coq
Vivek NigamNigam, Vivek Federal University of Paraiba / fortissGermany Committee Member in Program Committee within the CPP-track
Tobias NipkowNipkow, Tobias Technische Universität München Session Chair of Formalized mathematics 2 (part of CPP) Proof Pearl: Braun Trees
Fredrik Nordvall ForsbergNordvall Forsberg, Fredrik University of Strathclyde Three equivalent ordinal notation systems in Cubical Agda
O Federico OlmedoOlmedo, Federico University of Chile & IMFD Chile A Mechanized Formalization of GraphQL
Roy OverbeekOverbeek, Roy Vrije Universiteit AmsterdamNetherlands Formalizing Determinacy of Concurrent Revisions
P Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States Session Chair of Mechanized metatheory (part of CPP) Committee Member in Program Committee within the CPP-track
Damien PousPous, Damien CNRS, ENS Lyon Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
Loïc PujetPujet, Loïc Gallinette Project-Team, Inria Cubical Synthetic Homotopy Theory
R Vincent RahliRahli, Vincent University of Birmingham Committee Member in Program Committee within the CPP-track
Adrian Rebola PardoRebola Pardo, Adrian TU Wien Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs
Talia RingerRinger, Talia University of WashingtonUnited States REPLICA: REPL Instrumentation for Coq Analysis
Christine RizkallahRizkallah, Christine The University of MelbourneAustralia Committee Member in Program Committee within the CPP-track
Arjen RouvoetRouvoet, Arjen Delft University of TechnologyNetherlands Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
Grigore RoşuRoşu, Grigore University of Illinois at Urbana-ChampaignUnited States Invited talk: Matching Logic: The Foundation of the K Framework
Yann Régis-GianasRégis-Gianas, Yann IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2France FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
S Alex Sanchez-SternSanchez-Stern, Alex University of California, San DiegoUnited States REPLICA: REPL Instrumentation for Coq Analysis
Ilya SergeySergey, Ilya Yale-NUS College and National University of SingaporeSingapore Committee Member in Program Committee within the CPP-track
Thomas SewellSewell, Thomas Chalmers University of Technology, SwedenSweden Proof Pearl: Braun Trees
Natarajan ShankarShankar, Natarajan SRI International, USAUnited States A Verified Packrat Parser Interpreter for Parsing Expression Grammars
Zhong ShaoShao, Zhong Yale UniversityUnited States Session Chair of Concurrency and linearity (part of CPP)
Abhishek Kr SinghSingh, Abhishek Kr Tata Institute of Fundamental Research MumbaiIndia A Constructive Formalization of the Weak Perfect Graph Theorem
Anna SlobodovaSlobodova, Anna Centaur Technology, Inc. Verifying x86 Instruction Implementations
Simon SpiesSpies, Simon Saarland UniversityGermany Undecidability of Higher-Order Unification Formalised in Coq
Bas SpittersSpitters, Bas Concordium Blockchain Research Center, Aarhus University ConCert: A Smart Contract Certification Framework in Coq
Kathrin StarkStark, Kathrin Princeton University, USAGermany Session Chair of Decidability and complexity (part of CPP) Coq à la Carte - A Practical Approach to Modular Syntax with Binders Committee Member in Program Committee within the CPP-track
Rob SumnersSumners, Rob Centaur Technology, Inc. Verifying x86 Instruction Implementations
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States Session Chair of Program verification (part of CPP) Committee Member in Program Committee within the CPP-track
Sol SwordsSwords, Sol Centaur Technology, Inc. Verifying x86 Instruction Implementations
T Nicolas TabareauTabareau, Nicolas InriaFrance Committee Member in Program Committee within the CPP-track
Yong Kiam TanTan, Yong Kiam Carnegie Mellon University, USASingapore The Poincaré-Bendixson Theorem in Isabelle/HOL
Éric TanterTanter, Éric University of ChileChile A Mechanized Formalization of GraphQL
The mathlib Community The mathlib Community The Lean mathematical library
Linh TranTran, Linh National University of Singapore A Functional Proof Pearl: Inverting the Ackermann Hierarchy
Dmitriy TraytelTraytel, Dmitriy ETH ZurichSwitzerland Committee Member in Program Committee within the CPP-track
Ahto TruuTruu, Ahto Guardtime AS Verified Security of BLT Signature Scheme
U Josef UrbanUrban, Josef Czech Technical University in PragueCzechia Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
V Floris van Doornvan Doorn, Floris University of PittsburghUnited States Session Chair of Homotopy Type Theory and PC chairs' report (part of CPP) A Formal Proof of the Independence of the Continuum Hypothesis Committee Member in Program Committee within the CPP-track
Niccolò VeltriVeltri, Niccolò Tallinn University of Technology Formalizing π-calculus in Guarded Cubical Agda
Andrea VezzosiVezzosi, Andrea IT University Copenhagen Formalizing π-calculus in Guarded Cubical Agda
Eelco VisserVisser, Eelco Delft University of TechnologyNetherlands Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
W Qingxiang WangWang, Qingxiang University of Innsbruck Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Maximilian WuttkeWuttke, Maximilian Saarland University Verified Programming of Turing Machines in Coq
X Chuangjie XuXu, Chuangjie Ludwig-Maximilians-Universität München Three equivalent ordinal notation systems in Cubical Agda
Y Akihisa YamadaYamada, Akihisa National Institute of InformaticsJapan Committee Member in Program Committee within the CPP-track
Z Yannick ZakowskiZakowski, Yannick University of Pennsylvania An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Roberto ZuninoZunino, Roberto University of TrentoItaly Committee Member in Program Committee within the CPP-track