CPP 2016 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (61)

A Thomas AndersonAnderson, Thomas University of Washington Planning for Change in a Formal Verification of the Raft Consensus Protocol
Steve AntonAnton, Steve University of Washington Planning for Change in a Formal Verification of the Raft Consensus Protocol
Jeremy AvigadAvigad, Jeremy Carnegie Mellon University Program Co-Chair in Program Committee within the CPP-track
B Sophie BernardBernard, Sophie INRIA Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
Yves BertotBertot, Yves INRIAFrance Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
Mark BickfordBickford, Mark Cornell University A Nominal Exploration of Intuitionism
Sandrine BlazyBlazy, Sandrine IRISA / University of Rennes 1 Formal Verification of Control-flow Graph Flattening Committee Member in Program Committee within the CPP-track
C Arthur CharguéraudCharguéraud, Arthur Higher-order Representation Predicates in Separation Logic
Adam ChlipalaChlipala, Adam MITUnited States Program Co-Chair in Program Committee within the CPP-track
Cyril CohenCohen, Cyril Formalization of a Newton series representation of polynomials
Thierry CoquandCoquand, Thierry Chalmers University of Technology, Sweden Committee Member in Program Committee within the CPP-track
Lukasz CzajkaCzajka, Lukasz University of Innsbruck Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
D Leonardo de Mourade Moura, Leonardo Microsoft Research, Redmond Dependent Type Practice
Boris DjalalDjalal, Boris INRIA Formalization of a Newton series representation of polynomials
E Michael D. ErnstErnst, Michael D. University of Washington Planning for Change in a Formal Verification of the Raft Consensus Protocol
F Amy FeltyFelty, Amy University of Ottawa A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Harvey FriedmanFriedman, Harvey Ohio State University Perspectives on Formal Verfication
Nathan FultonFulton, Nathan Carnegie Mellon University A Logic of Proofs for Differential Dynamic Logic
H John HarrisonHarrison, John Intel Committee Member in Program Committee within the CPP-track
Chris HawblitzelHawblitzel, Chris Microsoft Research Committee Member in Program Committee within the CPP-track
Cătălin HriţcuHriţcu, Cătălin INRIA ParisFrance Committee Member in Program Committee within the CPP-track
Brian HuffmanHuffman, Brian Galois Committee Member in Program Committee within the CPP-track
K Cezary KaliszykKaliszyk, Cezary University of Innsbruck Mizar Environment for Isabelle
Evgenii KotelnikovKotelnikov, Evgenii Chalmers University of Technology The Vampire and the FOOL
Laura KovacsKovacs, Laura Chalmers University of Technology The Vampire and the FOOL Committee Member in Program Committee within the CPP-track
L Peter LammichLammich, Peter Technische Universität München Refinement Based Verification of Imperative Data Structures Committee Member in Program Committee within the CPP-track
Richard LethinLethin, Richard A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
Wenda LiLi, Wenda University of CambridgeChina A Modular, Efficient Formalisation of Real Algebraic Numbers
Hongjin LiangLiang, Hongjin University of Science and Technology of China Committee Member in Program Committee within the CPP-track
Dan LicataLicata, Dan Wesleyan University Committee Member in Program Committee within the CPP-track
M Panagiotis ManoliosManolios, Panagiotis Northeastern University Committee Member in Program Committee within the CPP-track
Benoit MeisterMeister, Benoit A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
Dale MillerMiller, Dale INRIA Saclay and LIX Committee Member in Program Committee within the CPP-track
Paul MountcastleMountcastle, Paul A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
Dominic MulliganMulligan, Dominic Cambridge University Committee Member in Program Committee within the CPP-track
P Joachim ParrowParrow, Joachim Uppsala University Bisimulation Up-to Techniques for Psi-calculi
Lawrence PaulsonPaulson, Lawrence Cambridge University A Modular, Efficient Formalisation of Real Algebraic Numbers Committee Member in Program Committee within the CPP-track
André PlatzerPlatzer, André A Logic of Proofs for Differential Dynamic Logic
Johannes Å. PohjolaPohjola, Johannes Å. Uppsala University Bisimulation Up-to Techniques for Psi-calculi
Andrei PopescuPopescu, Andrei Middlesex University, London Committee Member in Program Committee within the CPP-track
Karol PąkPąk, Karol University of Bialystok, Institute of Computer Science Mizar Environment for Isabelle
R Vincent RahliRahli, Vincent SnT A Nominal Exploration of Intuitionism
Tahina RamananandroRamananandro, Tahina A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
Giles RegerReger, Giles University of Manchester The Vampire and the FOOL
Laurence RideauRideau, Laurence INRIA Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
S Claudio Sacerdoti CoenSacerdoti Coen, Claudio University of Bologna Committee Member in Program Committee within the CPP-track
Sigurd SchneiderSchneider, Sigurd Saarland University Axiomatic Semantics for Compiler Verification
Steven SchäferSchäfer, Steven Axiomatic Semantics for Compiler Verification
Gert SmolkaSmolka, Gert Saarland University Axiomatic Semantics for Compiler Verification
Michel St-MartinSt-Martin, Michel University of Ottawa A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Pierre-Yves StrubStrub, Pierre-Yves IMDEA Software InstituteSpain Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
T Zachary TatlockTatlock, Zachary University of Washington, SeattleUnited States Planning for Change in a Formal Verification of the Raft Consensus Protocol Committee Member in Program Committee within the CPP-track
René ThiemannThiemann, René University of Innsbruck Formalizing Jordan Normal Forms in Isabelle/HOL
Cesare TinelliTinelli, Cesare University of Iowa Committee Member in Program Committee within the CPP-track
Alix TrieuTrieu, Alix ENS Rennes Formal Verification of Control-flow Graph Flattening
U Josef UrbanUrban, Josef Mizar Environment for Isabelle
V Floris van Doornvan Doorn, Floris Carnegie Mellon University Constructing the Propositional Truncation using Non-recursive HITs
Andrei VoronkovVoronkov, Andrei University of Manchester The Vampire and the FOOL
W James R. WilcoxWilcox, James R. University of WashingtonUnited States Planning for Change in a Formal Verification of the Raft Consensus Protocol
Doug WoosWoos, Doug University of WashingtonUnited States Planning for Change in a Formal Verification of the Raft Consensus Protocol
Y Akihisa YamadaYamada, Akihisa Formalizing Jordan Normal Forms in Isabelle/HOL