CPP 2019 Contributors -

Filter

Role Type

Contributing to

Number of Roles

Country

Results (74)

A Mauricio Ayala-RinconAyala-Rincon, Mauricio University of BrasíliaBrazil Committee Member in Program Committee within the CPP-track
B Véronique BenzakenBenzaken, Véronique LRI, Université Paris-SudFrance A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL A Verified Prover Based on Ordered Resolution
Sandrine BlazyBlazy, Sandrine Univ Rennes- IRISAFrance Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
Ana BoveBove, Ana Chalmers University of Technology, Sweden Committee Member in Program Committee within the CPP-track
C Kaustuv ChaudhuriChaudhuri, Kaustuv Inria, FranceFrance A Proof-Theoretic Approach to Certifying Skolemization
Evelyne ContejeanContejean, Evelyne A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra
D Benjamin DelawareDelaware, Benjamin Purdue University A Verified Protocol Buffer Compiler
Aaron DutleDutle, Aaron Committee Member in Program Committee within the CPP-track
E Manuel EberlEberl, Manuel Technische Universität MünchenGermany Verified Solving and Asymptotics of Linear Recurrences
F Bertram FelgenhauerFelgenhauer, Bertram A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Amy FeltyFelty, Amy University of OttawaCanada A Linear Logical Framework in Hybrid
Yannick ForsterForster, Yannick Saarland UniversityGermany On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
G Georges GonthierGonthier, Georges Inria Session Chair of Research Papers: Formalization of Mathematics and Computer Algebra (part of CPP)
Elsa GunterGunter, Elsa University of IllinoisUnited States Dynamic Class Initialization Semantics: a Jinja Extension
H Chris HawblitzelHawblitzel, Chris Microsoft Research Session Chair of Research Papers: Program Verification (part of CPP) Committee Member in Program Committee within the CPP-track
Aquinas HoborHobor, Aquinas Committee Member in Program Committee within the CPP-track
Wolf HonoreHonore, Wolf From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Rémi HutinHutin, Rémi IRISA / ENS RennesFrance Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
Johannes HölzlHölzl, Johannes Vrije Universiteit AmsterdamNetherlands Committee Member in Program Committee within the CPP-track
I Fabian ImmlerImmler, Fabian Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
K Jonas KaiserKaiser, Jonas Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
Chantal KellerKeller, Chantal LRI, Université Paris-SudFrance Committee Member in Program Committee within the CPP-track
Dominik KirstKirst, Dominik Saarland UniversityGermany On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Gerwin KleinKlein, Gerwin UNSW, Australia Committee Member in Program Committee within the CPP-track
Nicolas KohKoh, Nicolas From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
L Dominique Larchey-WendlingLarchey-Wendling, Dominique CNRS, LORIAFrance Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Robert Y. LewisLewis, Robert Y. Vrije Universiteit AmsterdamNetherlands A Formal Proof of Hensel's Lemma over the p-adic Integers
Wenda LiLi, Wenda University of Cambridge Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem
Yao LiLi, Yao University of PennsylvaniaUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Yishuai LiLi, Yishuai University of PennsylvaniaUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Daniel R. LicataLicata, Daniel R. Wesleyan UniversityUnited States Committee Member in Program Committee within the CPP-track
Alexander LochmannLochmann, Alexander Certified ACKBO
M Assia MahboubiMahboubi, Assia INRIAFrance Session Chair of Research Papers: Proof Theory, Theory of Programming Languages (part of CPP) Session Chair of Keynote 2 and Research Paper (part of CPP) Business Meeting Program Co-Chair in Program Committee within the CPP-track
Matteo ManighettiManighetti, Matteo Inria & École PolytechniqueFrance A Proof-Theoretic Approach to Certifying Skolemization
Susannah ManskyMansky, Susannah Dynamic Class Initialization Semantics: a Jinja Extension
William ManskyMansky, William University of Illinois at ChicagoUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Jean Everson MartinaMartina, Jean Everson UFSC - Universidade Federal de Santa CatarinaBrazil Committee Member in Program Committee within the CPP-track
Aart MiddeldorpMiddeldorp, Aart A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Dale MillerMiller, Dale INRIA Saclay and LIXFrance A Proof-Theoretic Approach to Certifying Skolemization
Toby MurrayMurray, Toby University of Melbourne, AustraliaAustralia Committee Member in Program Committee within the CPP-track
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology, SwedenSweden Session Chair of Keynote 1 and Research Paper (part of CPP) Business Meeting Program Co-Chair in Program Committee within the CPP-track
P Lawrence PaulsonPaulson, Lawrence University of CambridgeUnited Kingdom Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
André PlatzerPlatzer, André Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the CPP-track
Andrei PopescuPopescu, Andrei Middlesex University, LondonUnited Kingdom Session Chair of Research Papers: Rewriting, Automated Reasoning (part of CPP) Committee Member in Program Committee within the CPP-track
Turaga PrathameshPrathamesh, Turaga A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
R Franziska RappRapp, Franziska A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Binoy RavindranRavindran, Binoy Virginia Tech Formally Verified Big Step Semantics out of x86-64 Binaries
Giselle ReisReis, Giselle Carnegie Mellon University Committee Member in Program Committee within the CPP-track
Ian RoessleRoessle, Ian Virginia Tech, USA Formally Verified Big Step Semantics out of x86-64 Binaries
S Anders SchlichtkrullSchlichtkrull, Anders Technical University of Denmark A Verified Prover Based on Ordered Resolution
Steven SchäferSchäfer, Steven Saarland UniversityGermany Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Zhong ShaoShao, Zhong Yale UniversityUnited States Session Chair of Research Papers: Formalization of Mathematics and Computer Algebra (part of CPP)
Anna SlobodovaSlobodova, Anna Committee Member in Program Committee within the CPP-track
Gert SmolkaSmolka, Gert Saarland University On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Matthieu SozeauSozeau, Matthieu InriaFrance Eliminating Reflection from Type Theory
Simon SpiesSpies, Simon Saarland UniversityGermany Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Kathrin StarkStark, Kathrin Saarland University, GermanyGermany Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Christian SternagelSternagel, Christian University of Innsbruck, AustriaAustria Certified ACKBO Committee Member in Program Committee within the CPP-track
T Nicolas TabareauTabareau, Nicolas Inria Session Chair of Research Papers: Program Verification (part of CPP)
Nicolas TabareauTabareau, Nicolas InriaFrance Eliminating Reflection from Type Theory
Enrico TassiTassi, Enrico INRIAFrance Committee Member in Program Committee within the CPP-track
Zachary TatlockTatlock, Zachary University of Washington, SeattleUnited States Committee Member in Program Committee within the CPP-track
Dmitriy TraytelTraytel, Dmitriy ETH ZurichSwitzerland A Verified Prover Based on Ordered Resolution
V Freek VerbeekVerbeek, Freek Open University of the Netherlands, The Netherlands Formally Verified Big Step Semantics out of x86-64 Binaries
W Bow-Yaw WangWang, Bow-Yaw Committee Member in Program Committee within the CPP-track
Tjark WeberWeber, Tjark Uppsala UniversitySweden Committee Member in Program Committee within the CPP-track
Theo WinterhalterWinterhalter, Theo Gallinette / Inria / LS2NFrance Eliminating Reflection from Type Theory
X Li-yao XiaXia, Li-yao University of Pennsylvania From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Y Qianchuan YeYe, Qianchuan Purdue University A Verified Protocol Buffer Compiler
Z Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Bohua ZhanZhan, Bohua Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL