CPP 2017 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (81)

A Reynald AffeldtAffeldt, Reynald AIST, Japan Formal foundations of 3D geometry for modeling robot manipulators Committee Member in Program Committee within the CPP-track
Guillaume AllaisAllais, Guillaume Radboud University NijmegenFrance Type-and-scope safe programs and their proofs
Thorsten AltenkirchAltenkirch, Thorsten University of Nottingham Committee Member in Program Committee within the CPP-track
Sidney AmaniAmani, Sidney UNSW, Australia COMPLX: a verification framework for concurrent imperative programs
June AndronickAndronick, June Data61,CSIRO (formerly NICTA) and UNSWAustralia COMPLX: a verification framework for concurrent imperative programs
Jesús AransayAransay, Jesús Universidad de la Rioja, Spain Committee Member in Program Committee within the CPP-track
Andrea AspertiAsperti, Andrea University of Bologna, Italy Committee Member in Program Committee within the CPP-track
B Clark BarrettBarrett, Clark Stanford UniversityUnited States Committee Member in Program Committee within the CPP-track
Andrej BauerBauer, Andrej University of LjubljanaSlovenia The HoTT library: a formalization of homotopy type theory in Coq
Yves BertotBertot, Yves INRIAFrance Co-chair in Program Committee within the CPP-track
Nikolaj BjørnerBjørner, Nikolaj Microsoft Research Committee Member in Program Committee within the CPP-track
Brandon BohrerBohrer, Brandon Formally verified differential dynamic logic
Sylvie BoldoBoldo, Sylvie A Coq Formal Proof of the Lax–Milgram theorem
Maksym BortinBortin, Maksym COMPLX: a verification framework for concurrent imperative programs
Simon BoulierBoulier, Simon The Next 700 Syntactical models of type theory
Ana BoveBove, Ana Chalmers University of Technology, Sweden Committee Member in Program Committee within the CPP-track
James BrotherstonBrotherston, James Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic
C James ChapmanChapman, James Type-and-scope safe programs and their proofs
François ClémentClément, François A Coq Formal Proof of the Lax–Milgram theorem
Jesper CockxCockx, Jesper iMinds, BelgiumBelgium Lifting proof-relevant unification to higher dimensions
Cyril CohenCohen, Cyril Formal foundations of 3D geometry for modeling robot manipulators
D Delphine DemangeDemange, Delphine IRISA Committee Member in Program Committee within the CPP-track
Joseph DeviettiDevietti, Joseph University of Pennsylvania Verifying dynamic race detection
Dominique DevrieseDevriese, Dominique iMinds - Distrinet, KU LeuvenBelgium Lifting proof-relevant unification to higher dimensions
Jose DivasónDivasón, Jose A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
F Florian FaissoleFaissole, Florian A Coq Formal Proof of the Lax–Milgram theorem
Xinyu FengFeng, Xinyu University of Science and Technology of China Mechanized verification of preemptive OS kernels
Anthony FoxFox, Anthony University of Cambridge, UK Verified compilation of CakeML to multiple machine-code targets
G Gaetan GilbertGilbert, Gaetan Formalising Real Numbers in Homotopy Type Theory
Jason GrossGross, Jason MIT CSAILUnited States The HoTT library: a formalization of homotopy type theory in Coq
H Marieke HuismanHuisman, Marieke University of TwenteNetherlands Committee Member in Program Committee within the CPP-track
Reiner HähnleHähnle, Reiner Technical University of Darmstadt Committee Member in Program Committee within the CPP-track
Johannes HölzlHölzl, Johannes Technische Universität MünchenGermany Markov Processes in Isabelle/HOL
J Jan JakubuvJakubuv, Jan BliStrTune: Hierarchical Invention of Theorem Proving Strategies
Sebastiaan JoostenJoosten, Sebastiaan A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
K Jonas KaiserKaiser, Jonas Equivalence of System F and λ2 in Coq based on context morphism lemmas
Cezary KaliszykKaliszyk, Cezary University of Innsbruck Committee Member in Program Committee within the CPP-track
Robbert KrebbersKrebbers, Robbert Delft University of Technology, NetherlandsNetherlands Committee Member in Program Committee within the CPP-track
Ramana KumarKumar, Ramana Verified compilation of CakeML to multiple machine-code targets
Ondřej KunčarKunčar, Ondřej Technische Universität München, Germany Committee Member in Program Committee within the CPP-track
L Peter Lefanu LumsdaineLefanu Lumsdaine, Peter The HoTT library: a formalization of homotopy type theory in Coq
Mohsen LesaniLesani, Mohsen University of California, Riverside Committee Member in Program Committee within the CPP-track
Corey LewisLewis, Corey COMPLX: a verification framework for concurrent imperative programs
M Assia MahboubiMahboubi, Assia INRIAFrance Committee Member in Program Committee within the CPP-track
William ManskyMansky, William University of Pennsylvania Verifying dynamic race detection
Vincent MartinMartin, Vincent A Coq Formal Proof of the Lax–Milgram theorem
Erik Martin-DorelMartin-Dorel, Erik IRIT, Université Paul SabatierFrance A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations
Saki MatsumotoMatsumoto, Saki Formalization of Karp-Miller Tree Construction on Petri Nets
Micaela MayeroMayero, Micaela A Coq Formal Proof of the Lax–Milgram theorem
Conor McBrideMcBride, Conor Type-and-scope safe programs and their proofs
James McKinnaMcKinna, James University of Edinburgh Type-and-scope safe programs and their proofs
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology, Sweden Verified compilation of CakeML to multiple machine-code targets
N Michael NorrishNorrish, Michael Data61 at CSIRO, AustraliaAustralia Committee Member in Program Committee within the CPP-track
P Lawrence PaulsonPaulson, Lawrence University of CambridgeUnited Kingdom Porting the HOL Light Analysis Library: Some Lessons
Yuanfeng PengPeng, Yuanfeng University of Pennsylvania Verifying dynamic race detection
André PlatzerPlatzer, André Formally verified differential dynamic logic
François PottierPottier, François Verifying a hash table and its iterators in higher-order separation logic
Pierre-Marie PédrotPédrot, Pierre-Marie The Next 700 Syntactical models of type theory
R Vincent RahliRahli, Vincent SnT Formally verified differential dynamic logic Committee Member in Program Committee within the CPP-track
Tom RidgeRidge, Tom University of Leicester, UK Committee Member in Program Committee within the CPP-track
Christine RizkallahRizkallah, Christine University of Pennsylvania, USAUnited States COMPLX: a verification framework for concurrent imperative programs
Pierre RouxRoux, Pierre A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations
Reuben RoweRowe, Reuben University College LondonUnited Kingdom Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic
S Shogo SekineSekine, Shogo Formalization of Karp-Miller Tree Construction on Petri Nets
Michael ShulmanShulman, Michael The HoTT library: a formalization of homotopy type theory in Coq
Gert SmolkaSmolka, Gert Saarland University Equivalence of System F and λ2 in Coq based on context morphism lemmas
Matthieu SozeauSozeau, Matthieu InriaFrance The HoTT library: a formalization of homotopy type theory in Coq
Bas SpittersSpitters, Bas The HoTT library: a formalization of homotopy type theory in Coq
T Nicolas TabareauTabareau, Nicolas Inria, France The Next 700 Syntactical models of type theory
Yong Kiam TanTan, Yong Kiam *IHPC at ASTAR, Singapore** Verified compilation of CakeML to multiple machine-code targets
Tobias TebbiTebbi, Tobias Equivalence of System F and λ2 in Coq based on context morphism lemmas
René ThiemannThiemann, René University of Innsbruck A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
Joseph TuongTuong, Joseph COMPLX: a verification framework for concurrent imperative programs
U Josef UrbanUrban, Josef BliStrTune: Hierarchical Invention of Theorem Proving Strategies
V Viktor VafeiadisVafeiadis, Viktor MPI-SWS, GermanyGreece Co-chair in Program Committee within the CPP-track
Freek VerbeekVerbeek, Freek Open University of the Netherlands, The Netherlands Committee Member in Program Committee within the CPP-track
Marcus VoelpVoelp, Marcus Formally verified differential dynamic logic
Ivana VukoticVukotic, Ivana Formally verified differential dynamic logic
Y Akihisa YamadaYamada, Akihisa A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
Mitsuharu YamamotoYamamoto, Mitsuharu Formalization of Karp-Miller Tree Construction on Petri Nets
Z Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Verifying dynamic race detection Committee Member in Program Committee within the CPP-track