CPP 2018 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (95)

A Reynald AffeldtAffeldt, Reynald National Institute of Advanced Industrial Science and Technology (AIST), Japan Committee Member in Program Committee within the CPP-track
Thorsten AltenkirchAltenkirch, Thorsten University of Nottingham Session Chair of Type Theory, Set Theory, and Formalized Mathematics (part of CPP)
Sidney AmaniAmani, Sidney UNSW, Australia Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
June AndronickAndronick, June Data61,CSIRO (formerly NICTA) and UNSWAustralia Session Chair of Invited Talk by René Thiemann (part of CPP) Program Co-Chair in Program Committee within the CPP-track
B Joachim BardBard, Joachim Saarland University, Germany Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States Committee Member in Program Committee within the CPP-track
Dariusz BiernackiBiernacki, Dariusz University of Wrocław A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands A Verified SAT Solver with Watched Literals Using Imperative HOL Committee Member in Program Committee within the CPP-track
Sandrine BlazyBlazy, Sandrine IRISA, University of Rennes 1France Committee Member in Program Committee within the CPP-track
Sylvie BoldoBoldo, Sylvie Inria and Université Paris-SaclayFrance Committee Member in Program Committee within the CPP-track
Maria Paola BonacinaBonacina, Maria Paola University of Verona, Italy Proofs in Conflict-Driven Theory Combination
Maksym BortinBortin, Maksym Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Joachim BreitnerBreitner, Joachim University of PennsylvaniaUnited States Total Haskell is Reasonable Coq
Myriam BégelBégel, Myriam ENS Paris-Saclay, France Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
C Kaustuv ChaudhuriChaudhuri, Kaustuv Inria, FranceFrance A Two-Level Logic Perspective on (Simultaneous) Substitutions
James CheneyCheney, James University of Edinburgh, UKUnited States Committee Member in Program Committee within the CPP-track
D Jose DivasónDivasón, Jose Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Boris DjalalDjalal, Boris INRIA A Constructive Formalisation of Semi-algebraic Sets and Functions
Christian DoczkalDoczkal, Christian CNRS, France Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
F Amy FeltyFelty, Amy University of OttawaCanada Session Chair of Invited Talk by Brigitte Pientka (part of CPP) Program Co-Chair in Program Committee within the CPP-track
Denis FirsovFirsov, Denis University of Iowa, USA Generic Derivation of Induction for Impredicative Encodings in Cedille
Mathias FleuryFleury, Mathias MPI-INFGermany A Verified SAT Solver with Watched Literals Using Imperative HOL
Cédric FournetFournet, Cédric Microsoft Research A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Dan FruminFrumin, Dan Radboud University Finite Sets in Homotopy Type Theory
Hugo FéréeFérée, Hugo University of Kent, UKUnited Kingdom Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
G Herman GeuversGeuvers, Herman Radboud University Nijmegen, Netherlands Finite Sets in Homotopy Type Theory
Léon GondelmanGondelman, Léon LRI, Université Paris-Sud Finite Sets in Homotopy Type Theory
Stéphane Graham-LengrandGraham-Lengrand, Stéphane CNRS, France Proofs in Conflict-Driven Theory Combination
Niklas GrimmGrimm, Niklas Vienna University of Technology, Austria A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Dan GrossmanGrossman, Dan University of WashingtonUnited States Œuf: Minimizing the Coq Extraction TCB Adapting Proof Automation to Adapt Proofs
Elsa GunterGunter, Elsa University of IllinoisUnited States Committee Member in Program Committee within the CPP-track
H Cătălin HriţcuHriţcu, Cătălin Inria Paris A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Marieke HuismanHuisman, Marieke University of TwenteNetherlands Committee Member in Program Committee within the CPP-track
Warren HuntHunt, Warren University of Texas AustinUnited States Committee Member in Program Committee within the CPP-track
Samuel HymHym, Samuel University of Lille, France Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Reiner HähnleHähnle, Reiner Technical University of DarmstadtGermany Committee Member in Program Committee within the CPP-track
J Sebastiaan JoostenJoosten, Sebastiaan Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
K Jonas KaiserKaiser, Jonas Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Cezary KaliszykKaliszyk, Cezary University of Innsbruck Formal Microeconomic Foundations and the First Welfare Theorem
Dominik KirstKirst, Dominik Saarland UniversityGermany Large Model Constructions for Second-Order ZF in Dependent Type Theory
Ondřej KunčarKunčar, Ondřej Technische Universität München, Germany Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
L Peter LammichLammich, Peter Technische Universität München A Verified SAT Solver with Watched Literals Using Imperative HOL
K. Rustan M. LeinoLeino, K. Rustan M. AmazonUnited States Session Chair of Verified Applications (part of CPP) Committee Member in Program Committee within the CPP-track
Sergueï LengletLenglet, Sergueï University of Lorraine, France HOpi in Coq
John LeoLeo, John Halfaya ResearchUnited States Adapting Proof Automation to Adapt Proofs
M Matteo MaffeiMaffei, Matteo Saarland University A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Assia MahboubiMahboubi, Assia INRIAFrance Committee Member in Program Committee within the CPP-track
Kenji MaillardMaillard, Kenji Inria Paris and ENS Paris A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Micaela MayeroMayero, Micaela Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
James McKinnaMcKinna, James Triangulating Context Lemmas
Craig McLaughlinMcLaughlin, Craig The University of Edinburgh Triangulating Context Lemmas
Alberto MomiglianoMomigliano, Alberto Università degli Studi di Milano Committee Member in Program Committee within the CPP-track
Jean-Yves MoyenMoyen, Jean-Yves University of Copenhagen, Denmark Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Eric MullenMullen, Eric University of Washington Œuf: Minimizing the Coq Extraction TCB
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology, SwedenSweden Committee Member in Program Committee within the CPP-track
N Vivek NigamNigam, Vivek Federal University of Paraiba / fortissGermany Committee Member in Program Committee within the CPP-track
Tobias NipkowNipkow, Tobias Technical University MunichGermany Committee Member in Program Committee within the CPP-track
David NowakNowak, David CNRS, France Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
P Julian ParsertParsert, Julian University of Innsbruck, Austria Formal Microeconomic Foundations and the First Welfare Theorem
Stuart PernsteinerPernsteiner, Stuart University of Washington, USA Œuf: Minimizing the Coq Extraction TCB
Brigitte PientkaPientka, Brigitte McGill University Session Chair of Formalizing Meta-Theory (part of CPP) POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
Jonathan ProtzenkoProtzenko, Jonathan Microsoft Research, n.n.United States A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
George PîrleaPîrlea, George University College LondonUnited Kingdom Mechanising Blockchain Consensus
R Tahina RamananandroRamananandro, Tahina Microsoft Research, n.n.United States A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Aseem RastogiRastogi, Aseem Microsoft ResearchIndia A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Talia RingerRinger, Talia University of WashingtonUnited States Adapting Proof Automation to Adapt Proofs
Christine RizkallahRizkallah, Christine University of Pennsylvania, USAUnited States Total Haskell is Reasonable Coq
Damien RouhlingRouhling, Damien University of Côte d'Azur, France A Formal Proof in Coq of a Control Function for the Inverted Pendulum
S Alan SchmittSchmitt, Alan Inria HOpi in Coq
Steven SchäferSchäfer, Steven Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Ilya SergeySergey, Ilya University College LondonUnited Kingdom Mechanising Blockchain Consensus
Natarajan ShankarShankar, Natarajan SRI International, USA Session Chair of Verifying Programs and Systems (part of CPP) Proofs in Conflict-Driven Theory Combination
Zhong ShaoShao, Zhong Yale University Session Chair of Trusted Verification Frameworks and Systems (part of CPP)
Gert SmolkaSmolka, Gert Saarland University Large Model Constructions for Second-Order ZF in Dependent Type Theory Committee Member in Program Committee within the CPP-track
Antal Spector-ZabuskySpector-Zabusky, Antal Total Haskell is Reasonable Coq
Bas SpittersSpitters, Bas Committee Member in Program Committee within the CPP-track
Mark StaplesStaples, Mark CSIRO, Australia Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Ian StarkStark, Ian The University of EdinburghUnited Kingdom Triangulating Context Lemmas
Kathrin StarkStark, Kathrin Saarland University, Germany Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Pierre-Yves StrubStrub, Pierre-Yves Ecole PolytechniqueFrance Committee Member in Program Committee within the CPP-track
Aaron StumpStump, Aaron University of Iowa, USA Generic Derivation of Induction for Impredicative Encodings in Cedille
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
T Zachary TatlockTatlock, Zachary University of Washington, SeattleUnited States Œuf: Minimizing the Coq Extraction TCB
René ThiemannThiemann, René University of Innsbruck Session Chair of Proof Methods and Libraries (part of CPP) Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Laurent ThéryThéry, Laurent INRIAFrance Committee Member in Program Committee within the CPP-track
U Josef UrbanUrban, Josef Czech Technical University in PragueCzechia Committee Member in Program Committee within the CPP-track
V Viktor VafeiadisVafeiadis, Viktor MPI-SWS, GermanyGreece Committee Member in Program Committee within the CPP-track
Niels van der Weidevan der Weide, Niels Radboud University Nijmegen, Netherlands Finite Sets in Homotopy Type Theory
W Conrad WattWatt, Conrad University of Cambridge, UK Mechanising and Verifying the WebAssembly Specification
Stephanie WeirichWeirich, Stephanie University of Pennsylvania, USAUnited States Total Haskell is Reasonable Coq Committee Member in Program Committee within the CPP-track
Paweł WieczorekWieczorek, Paweł University of WrocławPoland A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
James R. WilcoxWilcox, James R. University of WashingtonUnited States Œuf: Minimizing the Coq Extraction TCB
Y Akihisa YamadaYamada, Akihisa Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Nathaniel YazdaniYazdani, Nathaniel University of Washington, SeattleUnited States Adapting Proof Automation to Adapt Proofs
Z Santiago Zanella-BéguelinZanella-Béguelin, Santiago Microsoft Research, n.n. A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations