POPL 2017 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (681)

A Martin AbadiAbadi, Martin Google Committee Member in Program Committee within the POPL -track
Iago AbalAbal, Iago IT University of Copenhagen Effective Bug Finding in C Programs with Shape and Effect Abstraction
Andreas AbelAbel, Andreas Gothenburg University Committee Member in Program Committee within the TTT-track
Erika AbrahamAbraham, Erika RWTH Aachen UniversityGermany Committee Member in Program committee for VMCAI 2017
Nathanael L. AckermanAckerman, Nathanael L. Harvard University On computable representations of exchangeable data Exchangeable random process and data abstraction
Reynald AffeldtAffeldt, Reynald AIST, Japan Formal foundations of 3D geometry for modeling robot manipulators Committee Member in Program Committee within the CPP -track
Danel AhmanAhman, Danel University of EdinburghEstonia Dijkstra Monads for Free
Amal AhmedAhmed, Amal Northeastern University Committee Member in Organizing Committee within the SCM-track
Aditya AkellaAkella, Aditya University of Wisconsin-Madison Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks
Ahmad Salim Al-SibahiAl-Sibahi, Ahmad Salim IT University of Copenhagen, DenmarkDenmark Abstract Interpretation of High-Level Transformations
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin - Madison Synthesizing Data-parallel Programs
Bader AlBassamAlBassam, Bader Purdue University Videos in Organizing Committee for POPL 2017
Elvira AlbertAlbert, Elvira Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
Jonathan AldrichAldrich, Jonathan Carnegie Mellon UniversityUnited States Designing extensible, domain-specific languages for mathematical diagrams Hazelnut: A Bidirectionally Typed Structure Editor Calculus
Jade AlglaveAlglave, Jade University College LondonFrance Ogre and Pythia, An invariance proof method for weak consistency models
Guillaume AllaisAllais, Guillaume Radboud University NijmegenFrance agdARGS - Declarative Hierarchical Command Line Interfaces Type-and-scope safe programs and their proofs
Thorsten AltenkirchAltenkirch, Thorsten University of Nottingham Committee Member in Program Committee within the CPP -track
Khulood AlyahyaAlyahya, Khulood Can we machine-learn programming language semantics?
Sidney AmaniAmani, Sidney UNSW, Australia COMPLX: a verification framework for concurrent imperative programs
Nada AminAmin, Nada EPFLSwitzerland Session Chair of Logic and Programming (part of POPL ) Young Researcher Panel Session Invited posters Type Soundness Proofs with Definitional Interpreters LMS-Verify: Abstraction Without Regret for Verified Systems Programming Committee Member in Speaker within the PLMW-track ERC member in External Review Committee within the POPL -track
Abhishek AnandAnand, Abhishek CertiCoq: A verified compiler for Coq
June AndronickAndronick, June Data61,CSIRO (formerly NICTA) and UNSWAustralia COMPLX: a verification framework for concurrent imperative programs ERC member in External Review Committee within the POPL -track
Carlo AngiuliAngiuli, Carlo Carnegie Mellon University Computational Higher-Dimensional Type Theory
Sergio AntoyAntoy, Sergio Kiel University Improving Non-deterministic Computations in Functional Logic Programs
Tomoyuki AotaniAotani, Tomoyuki Tokyo Institute of Technology CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL
Andrew W. AppelAppel, Andrew W. Princeton CertiCoq: A verified compiler for Coq
Jesús AransayAransay, Jesús Universidad de la Rioja, Spain Committee Member in Program Committee within the CPP -track
Kazuyuki AsadaAsada, Kazuyuki University of Tokyo A Functional Reformulation of UnCAL Graph-Transformations: Or, Graph Transformation as Graph Reduction
Izumi AsakuraAsakura, Izumi Tokyo Institute of Technology, JapanJapan CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL
Andrea AspertiAsperti, Andrea University of Bologna, Italy Committee Member in Program Committee within the CPP -track
Mounir AssafAssaf, Mounir Stevens Institute of Technology Hypercollecting Semantics and its Application to Static Analysis of Information Flow
Mohamed Faouzi AtigAtig, Mohamed Faouzi Uppsala UniversitySweden Committee Member in Program committee for VMCAI 2017
Robert AtkeyAtkey, Robert University of Strathclyde Program Chair in Organizing Committee within the Off the Beaten Track-track
Jeremy AvigadAvigad, Jeremy Carnegie Mellon University On computable representations of exchangeable data
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur University of Pennsylvania, USAUnited States A Semantic Account of Metric Preservation Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
B David BaeldeBaelde, David LSV, ENS CachanFrance Publicity Chair in Organizing Committee for POPL 2017
Thibaut BalabonskiBalabonski, Thibaut Université Paris-Sud Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Clark BarrettBarrett, Clark Stanford UniversityUnited States Partitioned Memory Models for Program Analysis. Committee Member in Program Committee within the CPP -track
Gilles BartheBarthe, Gilles IMDEA Coupling proofs are probabilistic product programs Relational Cost Analysis
Don BatoryBatory, Don University of Texas, AustinUnited States Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
Mark BattyBatty, Mark University of KentUnited Kingdom Mixed-size Concurrency: ARM, POWER, C/C++11, and SC Automatically Comparing Memory Consistency Models
Andrej BauerBauer, Andrej University of LjubljanaSlovenia The HoTT library: a formalization of homotopy type theory in Coq Committee Member in Program Committee within the TTT-track
Maciej BendkowskiBendkowski, Maciej Jagiellonian University Boltzmann Samplers for Closed Simply-Typed Lambda Terms
Josh BerdineBerdine, Josh Facebook Committee Member in Program Committee within the POPL -track
Daniil BerezunBerezun, Daniil JetBrains, Russia Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation (Invited Talk)
Martin BergerBerger, Martin Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
Lennart BeringerBeringer, Lennart Committee Member in Program Committee within the CoqPL-track
Yves BertotBertot, Yves INRIAFrance Co-chair in Program Committee within the CPP -track
Pierre BessièreBessière, Pierre CNRS/ISIR The semantics of subroutines and iteration in the Bayesian programming language ProBT
Frédéric BessonBesson, Frédéric Software Fault Isolation avec CompCert ppsimpl: a reflexive Coq tactic for canonising goals
Karthikeyan BhargavanBhargavan, Karthikeyan INRIA ERC member in External Review Committee within the POPL -track
Aggelos BiboudisBiboudis, Aggelos University of AthensGreece Invited posters Stream Fusion, to Completeness
Lars BirkedalBirkedal, Lars Aarhus University Session Chair of Semantic Foundations (part of POPL ) Logical Relations in Iris A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic Interactive Proofs in Higher-Order Concurrent Separation Logic ERC member in External Review Committee within the POPL -track
Aleš BizjakBizjak, Aleš Aarhus UniversityDenmark Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Nikolaj BjørnerBjørner, Nikolaj Microsoft Research Committee Member in Program Committee within the CPP -track ERC member in External Review Committee within the POPL -track
Alan BlackwellBlackwell, Alan University of CambridgeUnited Kingdom Keynote talk: Varieties of Programming Experience
Sandrine BlazyBlazy, Sandrine University of Rennes 1, FranceFrance Session Chair of Midday Session (part of CoqPL) Structuring Abstract Interpreters through State and Value Abstractions Program Co-Chair in Program Committee within the CoqPL-track
Guy E. BlellochBlelloch, Guy E. Carnegie Mellon University Parallel Functional Arrays
Roderick BloemBloem, Roderick Institute of Software Technology, Graz University of Technology Committee Member in Program committee for VMCAI 2017 Synthesizing Non-Vacuous Systems
François BobotBobot, François CEA Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins
Brandon BohrerBohrer, Brandon Formally verified differential dynamic logic
Sylvie BoldoBoldo, Sylvie A Coq Formal Proof of the Lax–Milgram theorem
Johannes BorgströmBorgström, Johannes Uppsala University Committee Member in Program Committee within the POPL -track
Maksym BortinBortin, Maksym COMPLX: a verification framework for concurrent imperative programs
Vincent BotbolBotbol, Vincent CEA LIST + LIP6 Université Pierre & Marie Curie Static Analysis of Communicating Process using Symbolic Transducers
Ahmed BouajjaniBouajjani, Ahmed IRIF, Université Paris DiderotFrance Co-chair in Program committee for VMCAI 2017 Committee Member in Organizing Committee for VMCAI 2017 Session Chair of Model Checking and Synthesis (part of VMCAI ) Session Chair of Invited talk 2 (part of VMCAI ) On Verifying Causal Consistency Program Co-Chair in Program Chairs within the VMCAI -track
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
Nathan BowlerBowler, Nathan Universität Hamburg Commutativity logic for probabilistic trace equivalence: complete or not?
William J. BowmanBowman, William J. Northeastern UniversityUnited States Toward Type-Preserving Compilation of Coq
Claus BrabrandBrabrand, Claus IT University of Copenhagen, Denmark Effective Bug Finding in C Programs with Shape and Effect Abstraction
Hadrien BrideBride, Hadrien Femto-ST / Université de Franche-Comté Reduction of Workflow Nets for Generalised Soundness Verification
Ian BriggsBriggs, Ian School of Computing, University of Utah Rigorous Floating-point Mixed Precision Tuning
James BrotherstonBrotherston, James Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic
Kevin J. BrownBrown, Kevin J. Stanford University Functional Parallels of Sequential Imperatives
Matt BrownBrown, Matt UCLA Typed Self-Evaluation via Intensional Type Functions
Florian BruseBruse, Florian University of Kassel On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
Lucas BrutschyBrutschy, Lucas ETH ZurichSwitzerland Serializability for Eventual Consistency: Criterion, Analysis and Applications
Mihai BudiuBudiu, Mihai VMware Research Group ERC member in External Review Committee within the POPL -track
François BérengerBérenger, François INRIA/CNRS/ENS/PSL* Semantic-Directed Clumping of Disjunctive Abstract States
David BühlerBühler, David CEA LIST Structuring Abstract Interpreters through State and Value Abstractions
C Yufei CaiCai, Yufei University of Tübingen, Germany Building inference algorithms from monad transformers
Jose CalderonCalderon, Jose Galois, Inc.United States Laziness Boxes You In
Michael CarbinCarbin, Michael MITUnited States Committee Member in Program Committee within the PPS-track
Giuseppe CastagnaCastagna, Giuseppe Paris Diderot University & CNRSItaly Committee Member in Steering Committee for POPL 2017 General Chair in Organizing Committee for POPL 2017 Speaker of Opening (part of POPL ) Session Chair of Invited speaker (part of POPL )
Emmanuel ChaillouxChailloux, Emmanuel LIP6 - UPMCFrance Associated Events Chair in Organizing Committee for POPL 2017 Static Analysis of Communicating Process using Symbolic Transducers
Supratik ChakrabortyChakraborty, Supratik IIT BombayIndia Matching multiplications in Bit-Vector formulas
Bor-Yuh Evan ChangChang, Bor-Yuh Evan University of Colorado Boulder Big Code Semantic-Directed Clumping of Disjunctive Abstract States
Stephen ChangChang, Stephen Northeastern University Type Systems as Macros
James ChapmanChapman, James Type-and-scope safe programs and their proofs
Krishnendu ChatterjeeChatterjee, Krishnendu IST Austria Stochastic Invariants for Probabilistic Termination ERC member in External Review Committee within the POPL -track
Avik ChaudhuriChaudhuri, Avik FacebookUnited States Session Chair of Type Systems 1 (part of POPL ) Fast and Precise Type Checking for JavaScript: Are you in Flow? Committee Member in Program Committee within the POPL -track
Liqian ChenChen, Liqian Block-wise abstract interpretation by combining abstract domains with SMT
Ikram CheriguiCherigui, Ikram ENS Paris A Semantic Account of Metric Preservation
Alvin CheungCheung, Alvin University of Washington Cosette: A Solver for SQL Equivalences
Wei-Fan ChiangChiang, Wei-Fan School of Computing, University of Utah Rigorous Floating-point Mixed Precision Tuning
Wei-Ngan ChinChin, Wei-Ngan National University of Singapore Committee Member in Program committee for VMCAI 2017
Adam ChlipalaChlipala, Adam MITUnited States Session Chair of Concurrency 3 (part of POPL ) Fiat: A New Take on Domain-Specific Languages by Programming with Specifications A Program Optimization for Automatic Database Result Caching Committee Member in Program Committee within the POPL -track
Hana ChocklerChockler, Hana Synthesizing Non-Vacuous Systems
Stephen ChongChong, Stephen Harvard University Artifact Evaluation Co-Chair in Organizing Committee for POPL 2017 Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
David Thrane ChristiansenChristiansen, David Thrane Indiana UniversityUnited States Idris, Inside-Out: A Tutorial on Extending Idris in Idris Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Guerric ChupinChupin, Guerric ENSTA ParisTech Funky Grooves: Declarative Programming of Full-Fledged Musical Applications
Matteo CiminiCimini, Matteo Indiana University, USA Session Chair of Poster Session (part of POPL Student Research Competition) Automatically Generating the Dynamic Semantics of Gradually Typed Languages Committee Member in Selection Committee within the POPL Student Research Competition-track
Florence ClercClerc, Florence McGill University Mathematical structures of probabilistic programming
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
Ernie CohenCohen, Ernie Amazon Web Services Verified Concurrent Code: Tricks of the Trade Reducing probabilistic choice to nondeterministic choice
Nathan CollinsCollins, Nathan Galois, Inc. GraPPa: spanning the expressivity vs. efficiency continuum
Sylvain ConchonConchon, Sylvain LRI, Université Paris-SudFrance Local Chair in Organizing Committee for POPL 2017
George A. ConstantinidesConstantinides, George A. Imperial College London, UK Automatically Comparing Memory Consistency Models
Byron CookCook, Byron Amazon Committee Member in Program committee for VMCAI 2017 Abstract Interpretation in Amazon
Joe CorneliCorneli, Joe Bootstrapping the next generation of mathematical social machines
Robert CornishCornish, Robert University of Oxford Efficient exact inference in discrete Anglican programs
Loïc CorrensonCorrenson, Loïc Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins
Agostino CortesiCortesi, Agostino Università Ca' Foscari VeneziaItaly Committee Member in Steering Committee for VMCAI 2017
Stefania CostantiniCostantini, Stefania Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Univ. dell'Aquila DALI for Cognitive Robotics: Principles and Prototype Implementation
Camille CotiCoti, Camille LIPN, Université Paris 13France Session Chair of Concurrency 1 (part of VMCAI )
Patrick CousotCousot, Patrick New York University Committee Member in Steering Committee for VMCAI 2017 Keynote: the Next 40 years of Abstract Interpretation Ogre and Pythia, An invariance proof method for weak consistency models 40 Years of Abstract Interpretation — An Interview with Patrick Cousot
Keenan CraneCrane, Keenan Designing extensible, domain-specific languages for mathematical diagrams
Karl CraryCrary, Karl Carnegie Mellon University Modules, Abstraction, and Parametric Polymorphism
Pascal CuoqCuoq, Pascal Trust-in-Soft Detecting Strict Aliasing Violations in the Wild
Marco Cusumano-TownerCusumano-Towner, Marco MIT-CSAIL Encapsulating models and approximate inference programs in probabilistic modules
D Loris D'AntoniD'Antoni, Loris University of Wisconsin–MadisonItaly Student Interaction Activity Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks Monadic second-order logic on finite sequences Committee Member in Program Committee within the PLMW-track ERC member in External Review Committee within the POPL -track
Vijay D'SilvaD'Silva, Vijay Google Complete Abstractions and Subclassical Modal Logics
Vijay D'SilvaD'Silva, Vijay Google Inc. Independence Abstractions and Models of Concurrency
Deepak D'SouzaD'Souza, Deepak Committee Member in Program committee for VMCAI 2017 Detecting All High-Level Dataraces in an RTOS Kernel.
Fredrik DahlqvistDahlqvist, Fredrik University College London Mathematical structures of probabilistic programming
Ugo Dal LagoDal Lago, Ugo University of Bologna, France How Far Apart Should Those Programs Be? The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
Mila Dalla PredaDalla Preda, Mila University of Verona, Italy ERC member in External Review Committee within the POPL -track
Vincent DanosDanos, Vincent ENS Paris/CNRS Systems biology Mathematical structures of probabilistic programming
David DaraisDarais, David University of Maryland, USAUnited States Videos in Organizing Committee for POPL 2017
Eva DarulovaDarulova, Eva MPI-SWSGermany Student Interaction Activity Committee Member in Program Committee within the PLMW-track
Ankush DasDas, Ankush Carnegie Mellon UniversityUnited States Towards Automatic Resource Bound Analysis for OCaml
Giovanni De GasperisDe Gasperis, Giovanni Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica DALI for Cognitive Robotics: Principles and Prototype Implementation
Leonardo de Mourade Moura, Leonardo Microsoft Research, Redmond The Lean Theorem Prover
Luc De RaedtDe Raedt, Luc KU Leuven Probabilistic logic programs: unifying program trace and possible world semantics
Ivo Gabe de Wolffde Wolff, Ivo Gabe Utrecht University Refining types using type guards in TypeScript
Benjamin DelawareDelaware, Benjamin Purdue University Session Chair of Verification and Synthesis (part of POPL ) ERC member in External Review Committee within the POPL -track
Pantazis DeligiannisDeligiannis, Pantazis Microsoft ResearchUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Delphine DemangeDemange, Delphine IRISA Committee Member in Program Committee within the CPP -track ERC member in External Review Committee within the POPL -track
Alin DeutschDeutsch, Alin Automatic Verification of Database-Centric Workflows
Joseph DeviettiDevietti, Joseph University of Pennsylvania Verifying dynamic race detection
Dominique DevrieseDevriese, Dominique iMinds - Distrinet, KU LeuvenBelgium Fully-Abstract Compilation of Parametric Polymorphism into Dynamic Sealing Lifting proof-relevant unification to higher dimensions Committee Member in Organizing Committee within the SCM-track
Işıl DilligDillig, Işıl UT Austin Abductive Reasoning in Deductive Verification Component-Based Synthesis for Complex APIs Committee Member in Speaker within the PLMW-track ERC member in External Review Committee within the POPL -track
Dimitar DimitrovDimitrov, Dimitar ETH Zurich, Switzerland Serializability for Eventual Consistency: Criterion, Analysis and Applications
Jose DivasónDivasón, Jose A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
Ryan DoengesDoenges, Ryan University of WashingtonUnited States Verification of Implementations of Distributed Systems Under Churn
Stephen DolanDolan, Stephen Polymorphism, subtyping and type inference in MLsub
Alastair F. DonaldsonDonaldson, Alastair F. Imperial College LondonUnited Kingdom Dynamic Race Detection For C++11
Samuel DrewsDrews, Samuel University of Wisconsin-Madison FairSquare: A Static Analysis Tool for Algorithmic Fairness
Derek DreyerDreyer, Derek MPI-SWS Session Chair of Type Systems 3 (part of POPL ) How to Give Talks That People Can Follow A Promising Semantics for Relaxed-Memory Concurrency Committee Member in Speaker within the PLMW-track Committee Member in Program Committee within the POPL -track
Cezara DrăgoiDrăgoi, Cezara INRIA, ENS, CNRSFrance Committee Member in Program committee for VMCAI 2017
Gilles DuboscqDuboscq, Gilles Practical Partial Evaluation for Language Implementation with Graal & Truffle
Andrej DudenhefnerDudenhefner, Andrej Technical University Dortmund Intersection Type Calculi of Bounded Dimension
Besik DunduaDundua, Besik Institute of Applied Mathematics, Tbilisi State University An Overview of PRhoLog
Jana DunfieldDunfield, Jana University of British ColumbiaCanada Sums of Uncertainty: Refinements go gradual
R. Kent DybvigDybvig, R. Kent Cisco, Indiana University ERC member in External Review Committee within the POPL -track
E ma ee, ma Synthesizing Non-Vacuous Systems
Gabriel EbnerEbner, Gabriel Vienna University of TechnologyAustria The Lean Theorem Prover
Markus EgerEger, Markus Programming with Epistemic Logic
E. Allen EmersonEmerson, E. Allen Committee Member in Steering Committee for VMCAI 2017
Constantin EneaEnea, Constantin LIAFA, Université Paris Diderot Session Chair of Symbolic analysis and invariant synthesis (part of VMCAI ) On Verifying Causal Consistency
Sebastian ErdwegErdweg, Sebastian TU DelftNetherlands Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
F Claudia FaggianFaggian, Claudia The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
Florian FaissoleFaissole, Florian Synthetic topology in HoTT for probabilistic programming A Coq Formal Proof of the Lax–Milgram theorem Synthetic topology in homotopy type theory for probabilistic programming
Andrew FarmerFarmer, Andrew FacebookUnited States Committee Member in Programme Committee for PEPM 2017 Session Chair of Programming languages (part of PEPM) Committee Member in Programme Committee within the PEPM-track
Azadeh FarzanFarzan, Azadeh University of Toronto ERC member in External Review Committee within the POPL -track
Yotam M. Y. FeldmanFeldman, Yotam M. Y. Tel Aviv UniversityIsrael Property Directed Reachability for Proving Absence of Concurrent Modification Errors
Xinyu FengFeng, Xinyu University of Science and Technology of China Mechanized verification of preemptive OS kernels
Yu FengFeng, Yu University of Texas at Austin, USAChina Component-Based Synthesis for Complex APIs
Christian FerdinandFerdinand, Christian AbsInt Abstract Interpretation in Absint
Jerome FeretFeret, Jerome INRIA ParisFrance Session Chair of Industrial Panel 2 & Systems Biology (part of N40AI) Committee Member in Organizer within the N40AI-track
Pietro FerraraFerrara, Pietro IBM ResearchItaly Using Abstract Interpretation to Correct Synchronization Faults
Jasmin FisherFisher, Jasmin Microsoft Research Verification of Cancer Programs
Kathleen FisherFisher, Kathleen Tufts University Session Chair of Functional Programming with Effects (part of POPL ) Time management, family and quality of life Programming Language Ideas Escape the Lab: Declarative Data Description Languages for Managing Ad hoc Data Committee Member in Speaker within the PLMW-track Committee Member in Program Committee within the POPL -track
Cormac FlanaganFlanagan, Cormac University of California, Santa CruzIreland ERC member in External Review Committee within the POPL -track
Matthew FlattFlatt, Matthew University of UtahUnited States Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
Shaked FlurFlur, Shaked University of Cambridge Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
Nate FosterFoster, Nate Cornell UniversityUnited States Session Chair of Session III (part of RDP) Session Chair of Welcome (part of RDP) Discussion Welcome Cantor Meets Scott: Semantic Foundations for Probabilistic Networks Organizing Chair in Program Committee within the RDP-track
Jonathan FowlerFowler, Jonathan University of Nottingham Failing Faster: Overlapping Patterns for Property-Based Testing
Anthony FoxFox, Anthony University of Cambridge, UK Verified compilation of CakeML to multiple machine-code targets
Cameron FreerFreer, Cameron Gamalon and BorelianUnited States Session Chair of Session 1 (part of PPS) On computable representations of exchangeable data Exchangeable random process and data abstraction Chair in Program Committee within the PPS-track
Levin FritzFritz, Levin Utrecht University Cost versus Precision for Approximate Typing for Python
Jonathan FruhmanFruhman, Jonathan CUNY Brooklyn College Canonicalizing High-Level Constructs in Picat
Asya FrumkinFrumkin, Asya Tel Aviv University Property Directed Reachability for Proving Absence of Concurrent Modification Errors
Weili FuFu, Weili University of Edinburgh Provenance for Configuration Language Security
G Marco GaboardiGaboardi, Marco SUNY Buffalo, USAItaly Session Chair of Probabilistic Programming (part of POPL ) Preventing False Discoveries in Adaptive Data Analysis: a Programming Language approach A Semantic Account of Metric Preservation Relational Cost Analysis Committee Member in Program Committee within the POPL -track
John P. GallagherGallagher, John P. Roskilde University Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
Emilio Jesús Gallego AriasGallego Arias, Emilio Jesús MINES ParisTechFrance Session Chair of Opening Session (part of CoqPL) Program Co-Chair in Program Committee within the CoqPL-track
Diane Gallois-WongGallois-Wong, Diane Inria Paris, ENS Paris Beginner's Luck: A Language for Property-Based Generators
Ronald GarciaGarcia, Ronald University of British Columbia Session Chair of Gradual Typing and Contracts (part of POPL ) Committee Member in Program Committee within the POPL -track
Deepak GargGarg, Deepak MPI-SWS, GermanyGermany Relational Cost Analysis Committee Member in Organizing Committee within the SCM-track
Ilias GarnierGarnier, Ilias University of Edinburgh Mathematical structures of probabilistic programming
Kimball GermaneGermane, Kimball University of Utah A Posteriori Environment Analysis with Pushdown Delta CFA
Zoubin GhahramaniGhahramani, Zoubin University of Cambridge Building inference algorithms from monad transformers
Dan GhicaGhica, Dan University of BirminghamUnited Kingdom Can we machine-learn programming language semantics?
Roberto GiacobazziGiacobazzi, Roberto University of Verona, Italy Committee Member in Program committee for VMCAI 2017 Session Chair of Invited speaker (part of POPL ) Session Chair of Opening (part of N40AI) Session Chair of Abstract Interpretation (part of VMCAI ) 40 Years of Abstract Interpretation — An Interview with Patrick Cousot Committee Member in Organizer within the N40AI-track
Nick GiannarakisGiannarakis, Nick Princeton University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jeremy GibbonsGibbons, Jeremy University of Oxford, UK Committee Member in Steering Committee for POPL 2017
Gaetan GilbertGilbert, Gaetan Formalising Real Numbers in Homotopy Type Theory
Robert GlückGlück, Robert Committee Member in Programme Committee for PEPM 2017 Session Chair of Types (part of PEPM) Reversible computing from a programming language perspective Committee Member in Programme Committee within the PEPM-track
Laure GonnordGonnord, Laure University of Lyon & LIP, FranceFrance Committee Member in Program committee for VMCAI 2017 Committee Member in Organizing Committee for VMCAI 2017 Session Chair of Numerical domains (part of VMCAI )
Ganesh GopalakrishnanGopalakrishnan, Ganesh University of Utah Rigorous Floating-point Mixed Precision Tuning
Andrew D. GordonGordon, Andrew D. Microsoft Research and University of EdinburghUnited Kingdom Committee Member in Steering Committee for POPL 2017 Program Chair in Organizing Committee for POPL 2017 Speaker of Opening (part of POPL ) Session Chair of Invited speaker (part of POPL ) Session Chair of Business meeting (part of POPL ) Session Chair of Type Systems 2 (part of POPL ) SIGPLAN business meeting PC Chair report Chair in Program Committee within the POPL -track
Kathryn E. GrayGray, Kathryn E. University of Cambridge Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
Michael GreenbergGreenberg, Michael Pomona College Understanding the POSIX Shell as a Programming Language
Ben GreenmanGreenman, Ben Northeastern UniversityUnited States Type Systems as Macros
Benjamin GregoireGregoire, Benjamin INRIA Coupling proofs are probabilistic product programs ERC member in External Review Committee within the POPL -track
Radu GrigoreGrigore, Radu University of KentUnited Kingdom Java generics are Turing complete
Jason GrossGross, Jason MIT CSAILUnited States The HoTT library: a formalization of homotopy type theory in Coq
Dan GrossmanGrossman, Dan University of WashingtonUnited States Reasoning about inference in probabilistic programs ERC member in External Review Committee within the POPL -track
Orna GrumbergGrumberg, Orna Technion – Israel Institute of Technology Committee Member in Program committee for VMCAI 2017
Katarzyna GrygielGrygiel, Katarzyna Jagiellonian University Boltzmann Samplers for Closed Simply-Typed Lambda Terms
Yijia GuGu, Yijia Northeastern University Stabilizing Floating-Point Programs using Provenance Analysis
Rachid GuerraouiGuerraoui, Rachid On Verifying Causal Consistency
Ashutosh GuptaGupta, Ashutosh Matching multiplications in Bit-Vector formulas
Arie GurfinkelGurfinkel, Arie University of WaterlooCanada System verification IC3 - Flipping the E in ICE
Henning GüntherGünther, Henning Technische Universität Wien Dynamic Reductions for Model Checking Concurrent Software.
H Jurriaan HageHage, Jurriaan Utrecht University Committee Member in Programme Committee for PEPM 2017 Session Chair of Transformation (part II) (part of PEPM) Lightweight Soundness for Towers of Language Extensions Cost versus Precision for Approximate Typing for Python Predicting Resource Consumption of Higher-Order Workflows Refining types using type guards in TypeScript Committee Member in Programme Committee within the PEPM-track
Ernst Moritz HahnHahn, Ernst Moritz State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
Matthew HammerHammer, Matthew University of Colorado, BoulderUnited States Running Incomplete Programs Hazelnut: A Bidirectionally Typed Structure Editor Calculus
Jad HamzaHamza, Jad LIAFA, Université Paris Diderot On Verifying Causal Consistency
Michael HanusHanus, Michael Kiel UniversityGermany Improving Non-deterministic Computations in Functional Logic Programs
Robert HarperHarper, Robert Parallel Functional Arrays Computational Higher-Dimensional Type Theory
William HarrisHarris, William Complexity Verification Using Guided Theorem Enumeration
Nicholas HayHay, Nicholas Vicarious The extended semantics for probabilistic programming languages
Jules HedgesHedges, Jules University of Oxford Selection Equilibria of Higher-Order Games
Fritz HengleinHenglein, Fritz DIKU, Denmark PEG Parsing in Less Space Using Progressive Tabling and Dynamic Analysis
Hugo HerbelinHerbelin, Hugo Session Chair of Second Afternoon Session (part of TTT) Coq's Prolog and application to defining semi-automatic tactics
Michael HicksHicks, Michael University of Maryland at College Park, USA Committee Member in Steering Committee for POPL 2017 What is research and how to do it? Thinking globally and acting locally. Security Committee Member in Speaker within the PLMW-track
Michael HiltonHilton, Michael Oregon State University, USAUnited States Hazelnut: A Bidirectionally Typed Structure Editor Calculus
Jochen HoenickeHoenicke, Jochen Universität FreiburgGermany Thread Modularity at Many Levels: a Pearl in Compositional Verification
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Towards Automatic Resource Bound Analysis for OCaml Relational Cost Analysis
Martin HofmannHofmann, Martin LMU, Munich, Germany ERC member in External Review Committee within the POPL -track
Lukáš HolíkHolík, Lukáš Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Cătălin HriţcuHriţcu, Cătălin Inria Paris Session Chair of Security and Privacy (part of POPL ) What is Secure Compilation? Part II (Short talk) Beginner's Luck: A Language for Property-Based Generators Dijkstra Monads for Free Committee Member in Program Committee within the POPL -track Committee Member in Organizing Committee within the SCM-track
Martin HruskaHruska, Martin Brno University of Technology Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Justin HsuHsu, Justin A Semantic Account of Metric Preservation Coupling proofs are probabilistic product programs
Zhenjiang HuHu, Zhenjiang National Institute of InformaticsJapan Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
Daniel HuangHuang, Daniel Harvard University An application of computable distributions to the semantics of probabilistic programs: part 2
John HughesHughes, John Chalmers University of Technology Beginner's Luck: A Language for Property-Based Generators
Marieke HuismanHuisman, Marieke University of TwenteNetherlands Committee Member in Program Committee within the CPP -track
Chung-Kil HurHur, Chung-Kil Seoul National UniversityKorea, South A Promising Semantics for Relaxed-Memory Concurrency ERC member in External Review Committee within the POPL -track
Graham HuttonHutton, Graham University of NottinghamUnited Kingdom Failing Faster: Overlapping Patterns for Property-Based Testing
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 Committee Member in Program Committee within the PPS-track
I Atsushi IgarashiIgarashi, Atsushi Kyoto UniversityJapan Verification of Code Generators via Higher-Order Model Checking Stateful Manifest Contracts
Yuu IgarashiIgarashi, Yuu Kyoto University A gradually typed polymorphic lambda calculus
Danko IlikIlik, Danko Trusted LabsFrance The exp-log normal form of types: Decomposing extensional equality and representing terms compactly
Radu IosifIosif, Radu VERIMAG, CNRS, Université Grenoble-Alpes Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
J Bart JacobsJacobs, Bart iMinds - Distrinet, KU LeuvenBelgium Committee Member in Program Committee within the POPL -track
Khurram A. JaferyJafery, Khurram A. University of British Columbia Sums of Uncertainty: Refinements go gradual
Suresh JagannathanJagannathan, Suresh DARPAUnited States Committee Member in Steering Committee for POPL 2017
Rahul JainJain, Rahul Tata Institute of Fundamental Research Matching multiplications in Bit-Vector formulas
Jan JakubuvJakubuv, Jan BliStrTune: Hierarchical Invention of Theorem Proving Strategies
Jan Martin JansenJansen, Jan Martin Netherlands Defence Academy Predicting Resource Consumption of Higher-Order Workflows
Ranjit JhalaJhala, Ranjit University of California, San Diego POPL 2018 presentation Committee Member in Program Committee within the POPL -track
Limin JiaJia, Limin Carnegie Mellon UniversityChina Committee Member in Program Committee within the POPL -track
Jiahong JiangJiang, Jiahong Block-wise abstract interpretation by combining abstract domains with SMT
Moa JohanssonJohansson, Moa Chalmers University of Technology Keynote talk: Reasoning about Functional Programs: Exploring, Testing and Inductive Proofs.
Neil D. JonesJones, Neil D. University of Copenhagen, Danmark Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation (Invited Talk)
Sebastiaan JoostenJoosten, Sebastiaan A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
Dejan JovanovićJovanović, Dejan SRI InternationalUnited States Committee Member in Program committee for VMCAI 2017 Solving Nonlinear Integer Arithmetic with MCSat
Ralf JungJung, Ralf MPI-SWS, GermanyGermany Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
K Jonas KaiserKaiser, Jonas Equivalence of System F and λ2 in Abella 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
Yukiyoshi KameyamaKameyama, Yukiyoshi University of Tsukuba, JapanJapan Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
Benjamin Lucien KaminskiKaminski, Benjamin Lucien RWTH Aachen University A weakest pre-expectation semantics for mixed-sign expectations
Jeehoon KangKang, Jeehoon Seoul National UniversityKorea, South A Promising Semantics for Relaxed-Memory Concurrency
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen University A weakest pre-expectation semantics for mixed-sign expectations
Shin-ya KatsumataKatsumata, Shin-ya Kyoto University A Semantic Account of Metric Preservation
Tatsuya KatsushimaKatsushima, Tatsuya Tohoku University, Japan Language-integrated Query with Ordering, Grouping and Outer Joins (poster)
Chantal KellerKeller, Chantal LRI, Université Paris-SudFrance ERC member in External Review Committee within the POPL -track
Steven KeuchelKeuchel, Steven Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding
Heidy KhlaafKhlaaf, Heidy University College London Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Daniel KiferKifer, Daniel Dept. of Computer Science and Engineering, Penn State University LightDP: Towards Automating Differential Privacy Proofs
Angelika KimmigKimmig, Angelika KU Leuven Probabilistic logic programs: unifying program trace and possible world semantics
Zachary KincaidKincaid, Zachary Princeton UniversityUnited States Young Researcher Panel Session Committee Member in Speaker within the PLMW-track Committee Member in Program Committee within the POPL -track
Oleg KiselyovKiselyov, Oleg Language-integrated Query with Ordering, Grouping and Outer Joins (poster) Invited posters Metropolis-Hastings for mixtures of conditional distributions Stream Fusion, to Completeness
Bartek KlinKlin, Bartek University of Warsaw Learning nominal automata
Markus KlinikKlinik, Markus Radboud University Nijmegen Predicting Resource Consumption of Higher-Order Workflows
Felix KlockKlock, Felix A Declarative DSL for Customized Rendering of Text-Based Art
Ilya KlyuchnikovKlyuchnikov, Ilya Committee Member in Programme Committee for PEPM 2017
Alex KnauthKnauth, Alex Northeastern University Type Systems as Macros
Naoki KobayashiKobayashi, Naoki University of Tokyo, Japan Verification of Code Generators via Higher-Order Model Checking On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic ERC member in External Review Committee within the POPL -track
Christoph E. KochKoch, Christoph E. Building performance-sensitive systems in high-level languages
Ekaterina KomendantskayaKomendantskaya, Ekaterina Committee Member in Program Committee within the Off the Beaten Track-track
Igor KonnovKonnov, Igor TU WienAustria Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
Eryk KopczynskiKopczynski, Eryk LOIS: syntax and semantics
Konstantin KorovinKorovin, Konstantin University of Manchester Committee Member in Program committee for VMCAI 2017
Eric KoskinenKoskinen, Eric Yale University Using Abstract Interpretation to Correct Synchronization Faults
Olga KouchnarenkoKouchnarenko, Olga Femto-ST / Université de Franche-Comté Reduction of Workflow Nets for Generalised Soundness Verification
Laura KovacsKovacs, Laura Chalmers University of Technology Committee Member in Program committee for VMCAI 2017 Coming to Terms with Quantified Reasoning
Dexter KozenKozen, Dexter Cornell UniversityUnited States Cantor Meets Scott: Semantic Foundations for Probabilistic Networks Committee Member in Program Committee within the POPL -track
Robbert KrebbersKrebbers, Robbert Delft University of Technology, NetherlandsNetherlands Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq Logical Relations in Iris Invited Talk -- Demonstration of the Iris separation logic in Coq Interactive Proofs in Higher-Order Concurrent Separation Logic Committee Member in Program Committee within the CPP -track Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track ERC member in External Review Committee within the POPL -track
Daniel KroeningKroening, Daniel University of Oxford Independence Abstractions and Models of Concurrency
Morten Krogh-JespersenKrogh-Jespersen, Morten Aarhus University A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
Sumith KulalKulal, Sumith IIT BombayIndia Contract-based Resource Verification for Higher-order Functions with Memoization
Ananya KumarKumar, Ananya Parallel Functional Arrays
Praveen KumarKumar, Praveen Cornell UniversityUnited States Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
Ramana KumarKumar, Ramana Verified compilation of CakeML to multiple machine-code targets
Viktor KunčakKunčak, Viktor EPFL, Switzerland Contract-based Resource Verification for Higher-order Functions with Memoization
Ondřej KunčarKunčar, Ondřej Technische Universität München, Germany Committee Member in Program Committee within the CPP -track
Lindsey KuperKuper, Lindsey Intel Labs General Chair in Organizing Committee within the Off the Beaten Track-track
Temur KutsiaKutsia, Temur An Overview of PRhoLog
L Alfons LaarmanLaarman, Alfons Vienna University of Technology Dynamic Reductions for Model Checking Concurrent Software.
Ori LahavLahav, Ori MPI-SWS A Promising Semantics for Relaxed-Memory Concurrency
Shuvendu K. LahiriLahiri, Shuvendu K. Microsoft Research Committee Member in Program committee for VMCAI 2017
Akash LalLal, Akash Microsoft Research IndiaIndia Committee Member in Program committee for VMCAI 2017 Committee Member in Program Committee within the POPL -track
Leonidas LampropoulosLampropoulos, Leonidas University of Pennsylvania Beginner's Luck: A Language for Property-Based Generators
Julien LangeLange, Julien Imperial College London Fencing off Go: Liveness and Safety for Channel-Based Programming
Victor LanvinLanvin, Victor ENS Paris-Saclay Gradual Set-Theoretic Types
Raphaël LaurentLaurent, Raphaël ProbaYes The semantics of subroutines and iteration in the Bayesian programming language ProBT
Julia LawallLawall, Julia Inria/LIP6 Interactive data representation migration: Exploiting program dependence to aid program transformation
Marijana LazićLazić, Marijana TU WienAustria A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
Tristan Le GallLe Gall, Tristan CEA LIST Static Analysis of Communicating Process using Symbolic Transducers
Peter Lefanu LumsdaineLefanu Lumsdaine, Peter The HoTT library: a formalization of homotopy type theory in Coq
Nicolás LehmannLehmann, Nicolás Gradual Refinement Types
Daan LeijenLeijen, Daan Microsoft ResearchUnited States Type Directed Compilation of Row-Typed Algebraic Effects
Ondřej LengálLengál, Ondřej Brno University of Technology Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Xavier LeroyLeroy, Xavier Inria ERC member in External Review Committee within the POPL -track
Mohsen LesaniLesani, Mohsen University of California, Riverside Committee Member in Program Committee within the CPP -track ERC member in External Review Committee within the POPL -track
Paul Blain LevyLevy, Paul Blain Commutativity logic for probabilistic trace equivalence: complete or not? Contextual isomorphisms
Corey LewisLewis, Corey COMPLX: a verification framework for concurrent imperative programs
Ondřej LhotákLhoták, Ondřej University of Waterloo, Canada Property Directed Reachability for Proving Absence of Concurrent Modification Errors
Huiqing LiLi, Huiqing University of Kent Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
Huisong LiLi, Huisong INRIA/CNRS/ENS/PSL* Semantic-Directed Clumping of Disjunctive Abstract States
Hongjin LiangLiang, Hongjin University of Science and Technology of China Committee Member in Program Committee within the CoqPL-track
Tomer LibalLibal, Tomer INRIA Saclay and LIX Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Christopher LidburyLidbury, Christopher Imperial College London Dynamic Race Detection For C++11
Yuliya LierlerLierler, Yuliya University of Nebraska Session Chair of Opening remarks (part of PADL) Committee Member in Organizing Committee within the PADL-track
Sam LindleyLindley, Sam University of Edinburgh Do be do be do ERC member in External Review Committee within the POPL -track
Peng LiuLiu, Peng Purdue University Using Abstract Interpretation to Correct Synchronization Faults
Xinxin LiuLiu, Xinxin Institute of software, Chinese academy of sciences Analyzing divergence in bisimulation semantics
Y. Annie LiuLiu, Y. Annie Stony Brook UniversityUnited States Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
Francesco LogozzoLogozzo, Francesco FacebookUnited States Session Chair of Program Analysis (part of POPL ) Abstract Interpretation in Facebook ERC member in External Review Committee within the POPL -track Committee Member in Organizer within the N40AI-track
Nuno P. LopesLopes, Nuno P. Microsoft Research ERC member in External Review Committee within the POPL -track
Etienne LozesLozes, Etienne ENS Cachan On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
M Ravichandhran MadhavanMadhavan, Ravichandhran EPFLSwitzerland Contract-based Resource Verification for Higher-order Functions with Memoization
P. MadhusudanMadhusudan, P. University of Illinois at Urbana-ChampaignUnited States ERC member in External Review Committee within the POPL -track
Nicolas MagaudMagaud, Nicolas Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations
Stephen MagillMagill, Stephen Laziness Boxes You In
Assia MahboubiMahboubi, Assia INRIAFrance Session Chair of First Morning Session (part of TTT) Committee Member in Program Committee within the CPP -track Committee Member in Program Committee within the TTT-track
Kenji MaillardMaillard, Kenji Inria Paris, ENS Paris, and Microsoft Research Dijkstra Monads for Free
Geoffrey MainlandMainland, Geoffrey Drexel University A Domain-Specific Language for Software-Defined Radio
Rupak MajumdarMajumdar, Rupak MPI-SWS Committee Member in Steering Committee for POPL 2017 Committee Member in Program committee for VMCAI 2017 Thread Modularity at Many Levels: a Pearl in Compositional Verification
Gregory MalechaMalecha, Gregory UCSD Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting
Sharad MalikMalik, Sharad Princeton University IC3 - Flipping the E in ICE
Roman ManevichManevich, Roman Ben-Gurion University of the NegevIsrael ERC member in External Review Committee within the POPL -track
Cyprien ManginMangin, Cyprien Equations: a tool for dependent pattern-matching
Vikash MansinghkaMansinghka, Vikash Massachusetts Institute of Technology Encapsulating models and approximate inference programs in probabilistic modules
William ManskyMansky, William University of Pennsylvania Verifying dynamic race detection
Theofrastos MantadelisMantadelis, Theofrastos Universidade do Porto Using Iterative Deepening for Probabilistic Logic Inference
Luc MarangetMaranget, Luc INRIA Rocquencourt Mixed-size Concurrency: ARM, POWER, C/C++11, and SC ERC member in External Review Committee within the POPL -track
Koar MarntirosianMarntirosian, Koar Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding
Chris MartensMartens, Chris Carnegie Mellon University Programming with Epistemic Logic Committee Member in Program Committee within the Off the Beaten Track-track
Ursula MartinMartin, Ursula Bootstrapping the next generation of mathematical social machines
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
Ruben MartinsMartins, Ruben Component-Based Synthesis for Complex APIs
Guido MartínezMartínez, Guido CIFASIS-CONICET, ArgentinaArgentina Dijkstra Monads for Free
Alexandre MaréchalMaréchal, Alexandre Efficient Elimination of Redundancies in Polyhedra using Raytracing
Isabella MastroeniMastroeni, Isabella University of Verona, ItalyItaly Session Chair of Abstract Interpretation (part of POPL ) Committee Member in Program Committee within the POPL -track
Hidehiko MasuharaMasuhara, Hidehiko Tokyo Institute of Technology CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL
Kazutaka MatsudaMatsuda, Kazutaka A Functional Reformulation of UnCAL Graph-Transformations: Or, Graph Transformation as Graph Reduction
Saki MatsumotoMatsumoto, Saki Formalization of Karp-Miller Tree Construction on Petri Nets
Tsubasa MatsushitaMatsushita, Tsubasa Shibaura Institute of Technology Detecting code clones with gaps by function applications
Micaela MayeroMayero, Micaela A Coq Formal Proof of the Lax–Milgram theorem
Emmanuel MazerMazer, Emmanuel CNRS/LIG The semantics of subroutines and iteration in the Bayesian programming language ProBT
Damiano MazzaMazza, Damiano CNRSFrance ERC member in External Review Committee within the POPL -track
Conor McBrideMcBride, Conor Type-and-scope safe programs and their proofs Do be do be do
Kathryn S McKinleyMcKinley, Kathryn S Microsoft Research Reasoning about inference in probabilistic programs
James McKinnaMcKinna, James University of Edinburgh Type-and-scope safe programs and their proofs
Craig McLaughlinMcLaughlin, Craig The University of Edinburgh Do be do be do
Kamel MekhnachaMekhnacha, Kamel ProbaYes The semantics of subroutines and iteration in the Bayesian programming language ProBT
Guillaume MelquiondMelquiond, Guillaume Inria Committee Member in Program Committee within the CoqPL-track
Eric MertensMertens, Eric Galois, Inc. GraPPa: spanning the expressivity vs. efficiency continuum
Mira MeziniMezini, Mira TU DarmstadtGermany ERC member in External Review Committee within the POPL -track
Matthew MightMight, Matthew University of Utah; Harvard Medical School; The White HouseUnited States A Posteriori Environment Analysis with Pushdown Delta CFA
Mae MilanoMilano, Mae Cornell University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Dale MillerMiller, Dale INRIA Saclay and LIX Proof checking and logic programming
Antoine MinéMiné, Antoine UPMC, FranceFrance Session Chair of Industrial Panel 1 (part of N40AI) Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions Committee Member in Organizer within the N40AI-track
Michael MisloveMislove, Michael Tulane Probabilistic programming and a domain theoretic approach to Skorohod's theorem
Joshua MoermanMoerman, Joshua Radboud University Learning nominal automata
Alberto MomiglianoMomigliano, Alberto A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method
Raphaël MonatMonat, Raphaël Ecole Normale Supérieure de Lyon Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions
David MonniauxMonniaux, David CNRS, VERIMAGFrance Chair in Program committee for VMCAI 2017 Committee Member in Organizing Committee for VMCAI 2017 Session Chair of Concurrency 2 (part of VMCAI ) Session Chair of Invited talk 1 (part of VMCAI ) Program Co-Chair in Program Chairs within the VMCAI -track
Greg MorrisettMorrisett, Greg Cornell University CertiCoq: A verified compiler for Coq An application of computable distributions to the semantics of probabilistic programs: part 2
Suvam MukherjeeMukherjee, Suvam Indian Institute of Science Detecting All High-Level Dataraces in an RTOS Kernel.
Madhavan MukundMukund, Madhavan Chennai Mathematical InstituteIndia Committee Member in Program committee for VMCAI 2017
Andrzej MurawskiMurawski, Andrzej University of Warwick, UK ERC member in External Review Committee within the POPL -track
Anca MuschollMuscholl, Anca Université de Bordeaux / LaBRI Reachability for dynamic parametric processes
Alan MycroftMycroft, Alan University of Cambridge Polymorphism, subtyping and type inference in MLsub
Andrew MyersMyers, Andrew Cornell University Session Chair of Compiler Optimisation (part of POPL ) POPL 2018 presentation Committee Member in Program Committee within the POPL -track
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology, Sweden Verified compilation of CakeML to multiple machine-code targets
Todd MytkowiczMytkowicz, Todd Reasoning about inference in probabilistic programs
Anders MörtbergMörtberg, Anders Inria Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom
Peter MüllerMüller, Peter ETH ZurichSwitzerland Serializability for Eventual Consistency: Criterion, Analysis and Applications ERC member in External Review Committee within the POPL -track
N Santosh NagarakatteNagarakatte, Santosh Rutgers University, USAUnited States ERC member in External Review Committee within the POPL -track
Keiko NakataNakata, Keiko Germany Session Chair of Second Morning Session (part of TTT) Committee Member in Program Committee within the TTT-track
Chandrakana NandiNandi, Chandrakana University of Washington, USAIndia Reasoning about inference in probabilistic programs
Krishna NarasimhanNarasimhan, Krishna Goethe UniversityIndia Interactive data representation migration: Exploiting program dependence to aid program transformation
David NaumannNaumann, David Stevens Institute of Technology Can relational logic facilitate secure compilation? (Short talk) Hypercollecting Semantics and its Application to Static Analysis of Information Flow
Giulio NazziconeNazzicone, Giulio Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica DALI for Cognitive Robotics: Principles and Prototype Implementation
Frank NevenNeven, Frank Parallel-Correctness and Transferability for Conjunctive Queries
Max S. NewNew, Max S. Northeastern University Gradual Type Precision as Retraction
Nicholas NgNg, Nicholas Imperial College LondonUnited Kingdom Fencing off Go: Liveness and Safety for Channel-Based Programming
Kim NguyễnNguyễn, Kim LRI, Université Paris-Sud Student Research Competition Chair in Organizing Committee for POPL 2017 Session Chair of Poster Session (part of POPL Student Research Competition) Session Chair of Student Competition Award (part of POPL Student Research Competition) Student Research Competition Chair in Selection Committee within the POPL Student Research Competition-track
Kyndylan NienhuisNienhuis, Kyndylan University of Cambridge Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
Vivek NigamNigam, Vivek Federal University of Paraiba ERC member in External Review Committee within the POPL -track
Henrik NilssonNilsson, Henrik Funky Grooves: Declarative Programming of Full-Fledged Musical Applications
Michael NorrishNorrish, Michael Data61 at CSIRO, AustraliaAustralia Committee Member in Program Committee within the CPP -track
Petr NovotnýNovotný, Petr IST AustriaAustria Stochastic Invariants for Probabilistic Termination
O Paulo OlivaOliva, Paulo Queen Mary University of London Selection Equilibria of Higher-Order Games
Cyrus OmarOmar, Cyrus Carnegie Mellon UniversityUnited States Running Incomplete Programs Hazelnut: A Bidirectionally Typed Structure Editor Calculus
Klaus OstermannOstermann, Klaus University of Tübingen, GermanyGermany Building inference algorithms from monad transformers
Long OuyangOuyang, Long Stanford University Support and influence analysis for visualizing posteriors of probabilistic programs
Scott OwensOwens, Scott University of KentUnited Kingdom ERC member in External Review Committee within the POPL -track ERC member in External Review Committee within the POPL -track
Or OzeriOzeri, Or Tel Aviv university Conjunctive Abstract Interpretation using Paramodulation
P Oded PadonPadon, Oded Tel Aviv UniversityIsrael Property Directed Reachability for Proving Absence of Concurrent Modification Errors Conjunctive Abstract Interpretation using Paramodulation Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Michele PaganiPagani, Michele IRIF, Université Paris DiderotItaly Session Chair of Quantum (part of POPL ) Committee Member in Program Committee within the POPL -track
Scott PakinPakin, Scott Programming Quantum Annealers
Nick PalladinosPalladinos, Nick Nessos Information Technologies, SA Invited posters Stream Fusion, to Completeness
Karl PalmskogPalmskog, Karl Verification of Implementations of Distributed Systems Under Churn
Jens PalsbergPalsberg, Jens University of California, Los Angeles Typed Self-Evaluation via Intensional Type Functions
Zoe ParaskevopoulouParaskevopoulou, Zoe Princeton University, USAUnited States CertiCoq: A verified compiler for Coq Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Victor PatentasuPatentasu, Victor Can we machine-learn programming language semantics?
Marco PatrignaniPatrignani, Marco MPI-SWS, Germany What is Secure Compilation? Part I Committee Member in Organizing Committee within the SCM-track
Daniel PattersonPatterson, Daniel Northeastern University Linking Types: Secure compilation of multi-language programs Linking Types: Specifying Safe Interoperability and Equivalences
Lawrence PaulsonPaulson, Lawrence University of CambridgeUnited Kingdom Porting the HOL Light Analysis Library: Some Lessons
Jennifer PaykinPaykin, Jennifer QWIRE: A Core Language for Quantum Circuits
Alison PeasePease, Alison Bootstrapping the next generation of mathematical social machines
Yuanfeng PengPeng, Yuanfeng University of Pennsylvania Verifying dynamic race detection
Michael PerinPerin, Michael Efficient Elimination of Redundancies in Polyhedra using Raytracing
Tomas PetricekPetricek, Tomas Alan Turing InstituteUnited Kingdom Committee Member in Program Committee within the Off the Beaten Track-track
Tommaso PetruccianiPetrucciani, Tommaso DIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, FranceItaly Student Volunteers in Organizing Committee for POPL 2017
Fabien PeureuxPeureux, Fabien Femto-ST / Université de Franche-Comté + Smartesting S&S Reduction of Workflow Nets for Generalised Soundness Verification
Avi PfefferPfeffer, Avi Charles River Analytics Committee Member in Program Committee within the PPS-track
Frank PfenningPfenning, Frank Carnegie Mellon University ERC member in External Review Committee within the POPL -track
Brigitte PientkaPientka, Brigitte McGill University Mechanizing Meta-Theory in Beluga A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method Committee Member in Speaker within the PLMW-track
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States The Curse of Knowledge Beginner's Luck: A Language for Property-Based Generators Committee Member in Speaker within the PLMW-track Committee Member in Program Committee within the CoqPL-track
Rinus PlasmeijerPlasmeijer, Rinus Radboud University Nijmegen Predicting Resource Consumption of Higher-Order Workflows
André PlatzerPlatzer, André Formally verified differential dynamic logic
Gordon PlotkinPlotkin, Gordon Towards a metric semantics for probabilistic programming (invited talk) Dijkstra Monads for Free Committee Member in Program Committee within the PPS-track
Andreas PodelskiPodelski, Andreas University of Freiburg, GermanyGermany Committee Member in Program committee for VMCAI 2017 Committee Member in Steering Committee for VMCAI 2017 Session Chair of Model-checking and bug finding (part of VMCAI ) Session Chair of Decision procedures (part of VMCAI ) Session Chair of Invited talk 3 (part of VMCAI ) Thread Modularity at Many Levels: a Pearl in Compositional Verification
Piotr PolesiukPolesiuk, Piotr IxFree: Step-Indexed Logical Relations in Coq
Nadia PolikarpovaPolikarpova, Nadia MIT CSAIL, USAUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Randy PollackPollack, Randy Harvard University CertiCoq: A verified compiler for Coq
François PottierPottier, François Verifying a hash table and its iterators in higher-order separation logic
Damien PousPous, Damien CNRS Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track ERC member in External Review Committee within the POPL -track
Jonathan ProtzenkoProtzenko, Jonathan Microsoft ResearchUnited States Security preserving compilation of low-level programs embedded in F* Young Researcher Panel Session Dijkstra Monads for Free Committee Member in Speaker within the PLMW-track
Christopher PultePulte, Christopher University of Cambridge Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
Pierre-Marie PédrotPédrot, Pierre-Marie The Next 700 Syntactical models of type theory
Markus PüschelPüschel, Markus ETH ZurichSwitzerland Committee Member in Programme Committee for PEPM 2017 Fast Polyhedra Abstract Domain Committee Member in Programme Committee within the PEPM-track
Corina S. PăsăreanuPăsăreanu, Corina S. NASA Ames Research Center Committee Member in Program committee for VMCAI 2017
R Vincent RahliRahli, Vincent SnT Formally verified differential dynamic logic Committee Member in Program Committee within the CPP -track
Sriram RajamaniRajamani, Sriram Microsoft Research Committee Member in Steering Committee for POPL 2017
Zvonimir RakamaricRakamaric, Zvonimir University of UtahUnited States Rigorous Floating-point Mixed Precision Tuning
G. RamalingamRamalingam, G. Microsoft Research ERC member in External Review Committee within the POPL -track
Steven RamsayRamsay, Steven University of Oxford Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Norman RamseyRamsey, Norman Exact Bayesian Inference by Symbolic Disintegration
Robert RandRand, Robert University of PennsylvaniaUnited States QWIRE: A Core Language for Quantum Circuits
Francesco RanzatoRanzato, Francesco University of PadovaItaly Session Chair of System Verification and Patrick Cousot's Keynote (part of N40AI) Committee Member in Organizer within the N40AI-track
Jean-François RaskinRaskin, Jean-François Université Libre de Bruxelles Committee Member in Program committee for VMCAI 2017
Ulrik Terp RasmussenRasmussen, Ulrik Terp DIKU, University of CopenhagenDenmark PEG Parsing in Less Space Using Progressive Tabling and Dynamic Analysis
Aseem RastogiRastogi, Aseem Microsoft Research IndiaIndia Dijkstra Monads for Free Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track ERC member in External Review Committee within the POPL -track
Jakob RathRath, Jakob Vienna University of Technology Integrating Answer Set Programming with Object-oriented Languages
Christoph RedlRedl, Christoph Vienna University of Technology Integrating Answer Set Programming with Object-oriented Languages Extending Answer Set Programs with Interpreted Functions as First-class Citizens
Jakob RehofRehof, Jakob Technical University Dortmund Intersection Type Calculi of Bounded Dimension
Christoph ReichenbachReichenbach, Christoph Goethe University Interactive data representation migration: Exploiting program dependence to aid program transformation
Giselle ReisReis, Giselle Carnegie Mellon University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Klaus Reisenberger-HagmayerReisenberger-Hagmayer, Klaus Johannes Kepler University Linz An Overview of PRhoLog
Thomas RepsReps, Thomas University of Wisconsin - Madison and Grammatech Inc.United States Committee Member in Steering Committee for VMCAI 2017 Sound Bit-Precise Numerical Domains Component-Based Synthesis for Complex APIs
Andrew ReynoldsReynolds, Andrew EPFL Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
Tamara RezkRezk, Tamara INRIA Committee Member in Organizing Committee within the SCM-track
Tom RidgeRidge, Tom University of Leicester, UK Committee Member in Program Committee within the CPP -track
Noam RinetzkyRinetzky, Noam Tel Aviv UniversityIsrael Conjunctive Abstract Interpretation using Paramodulation
Nicholas RiouxRioux, Nicholas Northeastern UniversityUnited States Naturality despite Nontermination: A Logical Relation for Linear Types and Polymorphism
Xavier RivalRival, Xavier INRIA/CNRS/ENS ParisFrance Session Chair of Security, Big Code and Synthesis (part of N40AI) Semantic-Directed Clumping of Disjunctive Abstract States Committee Member in Organizer within the N40AI-track
Christine RizkallahRizkallah, Christine University of Pennsylvania, USAUnited States Cogent: Where we Stand and What Comes Next (Short talk) COMPLX: a verification framework for concurrent imperative programs
Simon RobillardRobillard, Simon Chalmers University of TechnologySweden Coming to Terms with Quantified Reasoning
Ricardo RochaRocha, Ricardo Using Iterative Deepening for Probabilistic Logic Inference
Jared RoeschRoesch, Jared University of Washington, USAUnited States The Lean Theorem Prover
Adam RogalewiczRogalewicz, Adam Brno University of Technology Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Wren RomanoRomano, Wren Google Inc.United States Committee Member in Program Committee within the Off the Beaten Track-track
Tiark RompfRompf, Tiark Purdue UniversityUnited States Functional Parallels of Sequential Imperatives Invited posters Type Soundness Proofs with Definitional Interpreters LMS-Verify: Abstraction Without Regret for Verified Systems Programming
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
Daniel RoyRoy, Daniel On computable representations of exchangeable data Exchangeable random process and data abstraction Committee Member in Program Committee within the PPS-track ERC member in External Review Committee within the POPL -track
Stuart RussellRussell, Stuart University of California, Berkeley The extended semantics for probabilistic programming languages
Jason M. RuteRute, Jason M. Pennsylvania State University On computable representations of exchangeable data
Andrey RybalchenkoRybalchenko, Andrey Microsoft ResearchUnited Kingdom ERC member in External Review Committee within the POPL -track
Yann Régis-GianasRégis-Gianas, Yann IRIF, Université Paris Diderot Multimedia and Communication Chair in Organizing Committee for POPL 2017
S Arunkumar SS, Arunkumar Indian Institute of Science Detecting All High-Level Dataraces in an RTOS Kernel.
Marek S. BaranowskiS. Baranowski, Marek University of UtahUnited States Rigorous Floating-point Mixed Precision Tuning
Mooly SagivSagiv, Mooly Tel Aviv UniversityIsrael Session Chair of Session II (part of RDP) Session Chair of Welcome (part of RDP) Discussion Welcome Property Directed Reachability for Proving Absence of Concurrent Modification Errors Conjunctive Abstract Interpretation using Paramodulation Organizing Chair in Program Committee within the RDP-track Committee Member in Program Committee within the POPL -track
Burak SahinSahin, Burak Georgia Institute of Technology Complexity Verification Using Guided Theorem Enumeration
Roopsha SamantaSamanta, Roopsha Purdue University Young Researcher Panel Session Committee Member in Speaker within the PLMW-track
Matteo SammartinoSammartino, Matteo University College London Learning nominal automata Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Adrian SampsonSampson, Adrian Cornell UniversityUnited States Reasoning about inference in probabilistic programs
Dave SandsSands, Dave Chalmers University of Technology ERC member in External Review Committee within the POPL -track
Sriram SankaranarayananSankaranarayanan, Sriram University of Colorado, Boulder Committee Member in Program committee for VMCAI 2017
Susmit SarkarSarkar, Susmit University of St. Andrews, UK Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
Isao SasanoSasano, Isao Shibaura Institute of Technology Detecting code clones with gaps by function applications
Ryosuke SatoSato, Ryosuke University of Tokyo, Japan Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
Tetsuya SatoSato, Tetsuya Kyoto University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Olivier Savary BelangerSavary Belanger, Olivier Princeton UniversityCanada CertiCoq: A verified compiler for Coq
Gabriel SchererScherer, Gabriel Northeastern UniversityUnited States Full Abstraction for Language Design (Short talk) Deciding equivalence with sums and the empty type
Chad ScherrerScherrer, Chad Galois, Inc. Session Chair of Session 2 (part of PPS) GraPPa: spanning the expressivity vs. efficiency continuum An exponential family basis for probabilistic programming
Sven ScheweSchewe, Sven University of Liverpool Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
David SchmidtSchmidt, David Committee Member in Steering Committee for VMCAI 2017
Alan SchmittSchmitt, Alan Inria Session Chair of Morning Session (part of CoqPL)
Sven-Bodo ScholzScholz, Sven-Bodo Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
Tom SchrijversSchrijvers, Tom KU Leuven Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding ProbLog and applicative probabilistic programming
Ulrik Pagh SchultzSchultz, Ulrik Pagh University of Southern Denmark Programme Co-Chair in Programme Committee for PEPM 2017 Session Chair of Keynote (part of PEPM) Session Chair of Tutorial (Idris, Inside-Out) and Poster Session (part of PEPM) Session Chair of Tutorial: reversible computing (part of PEPM) PC Co-Chair in Programme Committee within the PEPM-track
Ziv ScullyScully, Ziv Carnegie Mellon UniversityUnited States A Program Optimization for Automatic Database Result Caching
Helmut SeidlSeidl, Helmut Technische Universität München Reachability for dynamic parametric processes
Shogo SekineSekine, Shogo Formalization of Karp-Miller Tree Construction on Petri Nets
Taro SekiyamaSekiyama, Taro Stateful Manifest Contracts
Yassamine SeladjiSeladji, Yassamine University of Tlemcen Finding Relevant Templates via the Principal Component Analysis
Cristina SerbanSerban, Cristina VERIMAG, CNRS, Université Grenoble-Alpes Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
Ilya SergeySergey, Ilya University College LondonUnited Kingdom Committee Member in Programme Committee for PEPM 2017 Session Chair of Concurrency 1 (part of POPL ) Committee Member in Programme Committee within the PEPM-track Committee Member in Program Committee within the POPL -track
Alejandro SerranoSerrano, Alejandro Utrecht University Lightweight Soundness for Towers of Language Extensions
Peter SewellSewell, Peter University of Cambridge Mixed-size Concurrency: ARM, POWER, C/C++11, and SC Committee Member in Program Committee within the PiP-track
Ali SezginSezgin, Ali University of Cambridge Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
Chung-chieh ShanShan, Chung-chieh Indiana University, USA Committee Member in Programme Committee for PEPM 2017 Session Chair of Session 5 (part of PPS) Session Chair of Transformation (part I) (part of PEPM) Exact Bayesian Inference by Symbolic Disintegration Committee Member in Programme Committee within the PEPM-track Chair in Program Committee within the PPS-track
Tushar SharmaSharma, Tushar University of Wisconsin - Madison, USA Sound Bit-Precise Numerical Domains
Mary SheeranSheeran, Mary Committee Member in Program Committee within the Off the Beaten Track-track
Sharon ShohamShoham, Sharon Tel Aviv universityIsrael IC3 - Flipping the E in ICE Property Directed Reachability for Proving Absence of Concurrent Modification Errors Committee Member in Program Committee within the POPL -track
Evguenia ShpritsShprits, Evguenia University of Mannheim Selection Equilibria of Higher-Order Games
Michael ShulmanShulman, Michael The HoTT library: a formalization of homotopy type theory in Coq
Jeremy G. SiekSiek, Jeremy G. Indiana University Bloomington Automatically Generating the Dynamic Semantics of Gradually Typed Languages Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System The State of the Art in Gradual Typing
Julien SignolesSignoles, Julien CEA LIST Session Chair of Poster Session (part of POPL Student Research Competition) Hypercollecting Semantics and its Application to Static Analysis of Information Flow Committee Member in Selection Committee within the POPL Student Research Competition-track
Alexandra SilvaSilva, Alexandra University College LondonUnited Kingdom Session Chair of Logic (part of POPL ) Student Interaction Activity Learning nominal automata Cantor Meets Scott: Semantic Foundations for Probabilistic Networks Committee Member in Program Committee within the PLMW-track Committee Member in Program Committee within the PPS-track ERC member in External Review Committee within the POPL -track
Gagandeep SinghSingh, Gagandeep ETH Zurich, SwitzerlandIndia Fast Polyhedra Abstract Domain
Rishabh SinghSingh, Rishabh Microsoft ResearchIndia Committee Member in Program Committee within the POPL -track
Satnam SinghSingh, Satnam Facebook Session Chair of ACM and SIGPLAN Awards (part of POPL )
KC SivaramakrishnanSivaramakrishnan, KC University of CambridgeUnited Kingdom Committee Member in Program Committee within the Off the Beaten Track-track
Lau SkorstengaardSkorstengaard, Lau Enforcing Well-Bracketed Control Flow on a Capability Machine using Local Capabilities
Yannis SmaragdakisSmaragdakis, Yannis University of Athens Invited posters Stream Fusion, to Completeness
Gert SmolkaSmolka, Gert Saarland University Equivalence of System F and λ2 in Abella Equivalence of System F and λ2 in Coq based on context morphism lemmas
Steffen SmolkaSmolka, Steffen Cornell University Cantor Meets Scott: Semantic Foundations for Probabilistic Networks Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Sunbeom SoSo, Sunbeom Korea University Synthesizing Imperative Programs from Examples for Introductory Programming Assignments
Ana SokolovaSokolova, Ana University of Salzburg Dynamic Reductions for Model Checking Concurrent Software.
Armando Solar-LezamaSolar-Lezama, Armando MIT CSAILUnited States Committee Member in Program committee for VMCAI 2017
Alexey SolovyevSolovyev, Alexey School of Computing, University of Utah Rigorous Floating-point Mixed Precision Tuning
Tyler SorensenSorensen, Tyler Imperial College LondonUnited Kingdom Automatically Comparing Memory Consistency Models
Marcelo SousaSousa, Marcelo University of Oxford Complete Abstractions and Subclassical Modal Logics Independence Abstractions and Models of Concurrency
Matthieu SozeauSozeau, Matthieu InriaFrance Session Chair of Afternoon Session (part of CoqPL) Session with the Coq Development Team Equations: a tool for dependent pattern-matching CertiCoq: A verified compiler for Coq The HoTT library: a formalization of homotopy type theory in Coq Committee Member in Program Committee within the CoqPL-track
Luca SpalazziSpalazzi, Luca Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Francesco SpegniSpegni, Francesco Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Bas SpittersSpitters, Bas Session Chair of First Afternoon Session (part of TTT) Synthetic topology in HoTT for probabilistic programming The HoTT library: a formalization of homotopy type theory in Coq Synthetic topology in homotopy type theory for probabilistic programming
Akhilesh SrikanthSrikanth, Akhilesh Georgia Institute of Technology Complexity Verification Using Guided Theorem Enumeration
Siddharth SrivastavaSrivastava, Siddharth UTRC Berkeley The extended semantics for probabilistic programming languages
Sam StatonStaton, Sam University of Oxford Session Chair of Session 3 (part of PPS) Exchangeable random process and data abstraction Committee Member in Program Committee within the POPL -track
Guy L. Steele Jr.Steele Jr., Guy L. Oracle LabsUnited States Committee Member in Program Committee within the PPS-track
George StelleStelle, George Programming Quantum Annealers
Marielle StoelingaStoelinga, Marielle University of Twente Committee Member in Program committee for VMCAI 2017
Ofer StrichmanStrichman, Ofer Technion Synthesizing Non-Vacuous Systems
Pierre-Yves StrubStrub, Pierre-Yves École PolytechniqueFrance Coupling proofs are probabilistic product programs Committee Member in Program Committee within the CoqPL-track
Zhendong SuSu, Zhendong University of California, DavisUnited States Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability
Kausik SubramanianSubramanian, Kausik University of Wisconsin-Madison Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks
Eijiro SumiiSumii, Eijiro Tohoku University Committee Member in Program Committee within the POPL -track
Joshua SunshineSunshine, Joshua Carnegie Mellon University Designing extensible, domain-specific languages for mathematical diagrams
Takashi SuwaSuwa, Takashi University of Tokyo, JapanJapan Verification of Code Generators via Higher-Order Model Checking
Kasper SvendsenSvendsen, Kasper Aarhus University A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States Research: The Industrial Culture Dijkstra Monads for Free Committee Member in Speaker within the PLMW-track
Wouter SwierstraSwierstra, Wouter University of Utrecht Committee Member in Program Committee within the Off the Beaten Track-track
Cameron SwordsSwords, Cameron Indiana University Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System
Michał SzynwelskiSzynwelski, Michał University of Warsaw Learning nominal automata
T Nicolas TabareauTabareau, Nicolas Inria, France Invited Talk -- Managing Logical and Computational Complexity using Program Transformations The Next 700 Syntactical models of type theory ERC member in External Review Committee within the POPL -track
Walid TahaTaha, Walid Halmstad University Session Chair of Opening remarks (part of PADL) Committee Member in Organizing Committee within the PADL-track
Yong Kiam TanTan, Yong Kiam *IHPC at ASTAR, Singapore** Verified compilation of CakeML to multiple machine-code targets
Éric TanterTanter, Éric University of Chile, Chile Gradual Refinement Types
Paul TarauTarau, Paul University of North TexasUnited States Boltzmann Samplers for Closed Simply-Typed Lambda Terms
Thorsten TarrachTarrach, Thorsten Austrian Institute of TechnologyAustria Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Takaaki TateishiTateishi, Takaaki IBM Research - Tokyo Verification Challenges in Applications of Blockchain for Business Collaboration
Zachary TatlockTatlock, Zachary University of Washington, SeattleUnited States Verification of Implementations of Distributed Systems Under Churn
Tobias TebbiTebbi, Tobias Equivalence of System F and λ2 in Coq based on context morphism lemmas
Tachio TerauchiTerauchi, Tachio JAIST ERC member in External Review Committee within the POPL -track
David ThibodeauThibodeau, David McGill University, Canada A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method
Peter ThiemannThiemann, Peter University of FreiburgGermany Committee Member in Steering Committee for POPL 2017 ERC member in External Review Committee within the POPL -track
René ThiemannThiemann, René University of Innsbruck A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
Amin TimanyTimany, Amin imec - Distrinet, KU LeuvenBelgium Logical Relations in Iris Interactive Proofs in Higher-Order Concurrent Separation Logic
Ben L. TitzerTitzer, Ben L. Google ERC member in External Review Committee within the POPL -track
Sam Tobin-HochstadtTobin-Hochstadt, Sam Indiana UniversityUnited States ERC member in External Review Committee within the POPL -track
Aaron TombTomb, Aaron Galois, Inc.United States Abstract Interpretation at Galois Invited Talk -- Type Theory in the Software Analysis Workbench
Bernardo ToninhoToninho, Bernardo Imperial College London Fencing off Go: Liveness and Safety for Channel-Based Programming
Szymon ToruńczykToruńczyk, Szymon Computation with Atoms LOIS: syntax and semantics
Éric TotelTotel, Éric CentraleSupélec Hypercollecting Semantics and its Application to Static Analysis of Information Flow
Mirco TribastoneTribastone, Mirco IMT Institute for Advanced Studies Lucca, Italy ERC member in External Review Committee within the POPL -track
Omer TrippTripp, Omer IBM Thomas J. Watson Research CenterIsrael Using Abstract Interpretation to Correct Synchronization Faults
Frédéric TronelTronel, Frédéric CentraleSupélec Hypercollecting Semantics and its Application to Static Analysis of Information Flow
Takeshi TsukadaTsukada, Takeshi University of Tokyo, Japan Verification of Code Generators via Higher-Order Model Checking
Joseph TuongTuong, Joseph COMPLX: a verification framework for concurrent imperative programs
Aaron TuronTuron, Aaron MPI-SWS Rust: from POPL to practice
Andrea TurriniTurrini, Andrea State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
U Sebastian UllrichUllrich, Sebastian Karlsruhe Institute of TechnologyGermany The Lean Theorem Prover
Josef UrbanUrban, Josef BliStrTune: Hierarchical Invention of Theorem Proving Strategies
V Viktor VafeiadisVafeiadis, Viktor MPI-SWS, GermanyGreece A Promising Semantics for Relaxed-Memory Concurrency Co-chair in Program Committee within the CPP -track ERC member in External Review Committee within the POPL -track
Benoit ValironValiron, Benoit LRI, CentraleSupelec, Univ. Paris SaclayFrance Student Activity Chair in Organizing Committee for POPL 2017 The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
Guy Van den BroeckVan den Broeck, Guy University of California, Los Angeles Committee Member in Program Committee within the PPS-track
Tijs van der Stormvan der Storm, Tijs CWINetherlands Committee Member in Programme Committee for PEPM 2017 Committee Member in Programme Committee within the PEPM-track
David Van HornVan Horn, David University of Maryland, College Park Committee Member in Program Committee within the POPL -track
Alexander VandenbrouckeVandenbroucke, Alexander KU Leuven, Belgium ProbLog and applicative probabilistic programming
Andrea VandinVandin, Andrea IMT School for Advanced Studies Lucca, ItalyItaly Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Margus VeanesVeanes, Margus Microsoft Research Monadic second-order logic on finite sequences
Martin VechevVechev, Martin ETH Zurich Machine Learning and Programming Languages: latest directions and research opportunities Fast Polyhedra Abstract Domain Serializability for Eventual Consistency: Criterion, Analysis and Applications Committee Member in Speaker within the PLMW-track ERC member in External Review Committee within the POPL -track
Helmut VeithVeith, Helmut TU WienAustria A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
Joost VennekensVennekens, Joost KU Leuven Lowering the learning curve for declarative programming: a Python API for the IDP system
Freek VerbeekVerbeek, Freek Open University of the Netherlands, The Netherlands Committee Member in Program Committee within the CPP -track
Victor VianuVianu, Victor UC San DiegoUnited States Session Chair of Session I (part of RDP) Session Chair of Welcome (part of RDP) Session Chair of Session IV (part of RDP) Discussion Welcome Organizing Chair in Program Committee within the RDP-track
Jan VitekVitek, Jan Northeastern UniversitySwitzerland Committee Member in Steering Committee for POPL 2017
Michael VitousekVitousek, Michael Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System
Yakir VizelVizel, Yakir IC3 - Flipping the E in ICE
Marcus VoelpVoelp, Marcus Formally verified differential dynamic logic
Tomáš VojnarVojnar, Tomáš Brno University of Technology Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Andrei VoronkovVoronkov, Andrei University of Manchester Coming to Terms with Quantified Reasoning
Ian VoyseyVoysey, Ian Carnegie Mellon University Running Incomplete Programs Hazelnut: A Bidirectionally Typed Structure Editor Calculus
Milena Vujosevic JanicicVujosevic Janicic, Milena Modelling Program Behaviour within Software Verification Tool LAV
Ivana VukoticVukotic, Ivana Formally verified differential dynamic logic
Dimitrios VytiniotisVytiniotis, Dimitrios Microsoft Research, Cambridge Student Interaction Activity Committee Member in Program Committee within the PLMW-track
W Thomas WahlWahl, Thomas Northeastern University Stabilizing Floating-Point Programs using Provenance Analysis
David WalkerWalker, David Princeton UniversityUnited States Committee Member in Steering Committee for POPL 2017 Industrial Relations Chair in Organizing Committee for POPL 2017
Igor WalukiewiczWalukiewicz, Igor CNRS, LaBRI Reachability for dynamic parametric processes
Ji WangWang, Ji Block-wise abstract interpretation by combining abstract domains with SMT
Peng WangWang, Peng MIT CSAIL Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Wei WangWang, Wei Google, Inc.China Partitioned Memory Models for Program Analysis.
Yuepeng WangWang, Yuepeng University of Texas at Austin Component-Based Synthesis for Complex APIs
Matthew WeaverWeaver, Matthew Princeton University CertiCoq: A verified compiler for Coq
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States The Influence of Dependent Types
Georg WeissenbacherWeissenbacher, Georg Technische Universität Wien Dynamic Reductions for Model Checking Concurrent Software.
Shu-chun WengWeng, Shu-chun Yale University Towards Automatic Resource Bound Analysis for OCaml
Edwin WestbrookWestbrook, Edwin Galois, Inc. Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting GraPPa: spanning the expressivity vs. efficiency continuum
John WickersonWickerson, John Imperial College LondonUnited Kingdom Automatically Comparing Memory Consistency Models
Josef WidderWidder, Josef TU WienAustria Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
Thomas WiesWies, Thomas New York University Partitioned Memory Models for Program Analysis.
James R. WilcoxWilcox, James R. University of WashingtonUnited States Verification of Implementations of Distributed Systems Under Churn
Todd WilsonWilson, Todd California State University Fresno Computational Higher-Dimensional Type Theory
Daniel Winograd-CortWinograd-Cort, Daniel University of Pennsylvania Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Viktor WinschelWinschel, Viktor ETH Zürich Selection Equilibria of Higher-Order Games
Frank WoodWood, Frank University of Oxford Efficient exact inference in discrete Anglican programs
Doug WoosWoos, Doug University of WashingtonUnited States Verification of Implementations of Distributed Systems Under Churn
Xiaodi WuWu, Xiaodi University of Oregon, USAUnited States Invariants of Quantum Programs: Characterisations and Generation
Xueguang WuWu, Xueguang Block-wise abstract interpretation by combining abstract domains with SMT
Yi WUWU, Yi UC BerkeleyUnited States The extended semantics for probabilistic programming languages
Andrzej WąsowskiWąsowski, Andrzej IT University of Copenhagen, Denmark Effective Bug Finding in C Programs with Shape and Effect Abstraction
X Li-yao XiaXia, Li-yao ENS Paris A Monadic Framework for Bidirectional Programming Beginner's Luck: A Language for Property-Based Generators
Anton XueXue, Anton Yale University A Symbolic Execution Framework for Haskell
Y Eran YahavYahav, Eran TechnionIsrael Program synthesis ERC member in External Review Committee within the POPL -track
Boris YakobowskiYakobowski, Boris CEA - LISTFrance Committee Member in Program committee for VMCAI 2017 Session Chair of Program Analysis (part of VMCAI ) Structuring Abstract Interpreters through State and Value Abstractions Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins
Jeremy YallopYallop, Jeremy University of Cambridge, UK Programme Co-Chair in Programme Committee for PEPM 2017 Session Chair of Tutorial (Idris, Inside-Out) and Poster Session (part of PEPM) Session Chair of Tutorial: Partial Evaluation for Language Implementation (part of PEPM) PC Co-Chair in Programme Committee within the PEPM-track
Akihisa YamadaYamada, Akihisa A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
Mitsuharu YamamotoYamamoto, Mitsuharu Formalization of Karp-Miller Tree Construction on Petri Nets
Hongseok YangYang, Hongseok University of Oxford Session Chair of Session 6 (part of PPS) Efficient exact inference in discrete Anglican programs Exchangeable random process and data abstraction ERC member in External Review Committee within the POPL -track
Jean YangYang, Jean Carnegie Mellon University Artifact Evaluation Co-Chair in Organizing Committee for POPL 2017 Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Katherine YeYe, Katherine Designing extensible, domain-specific languages for mathematical diagrams
Mingsheng YingYing, Mingsheng University of Technology Sydney, Australia Invariants of Quantum Programs: Characterisations and Generation
Shenggang YingYing, Shenggang University of Technology Sydney, Australia Invariants of Quantum Programs: Characterisations and Generation
Nobuko YoshidaYoshida, Nobuko Imperial College London, UK Session Chair of Concurrency 2 (part of POPL ) Fencing off Go: Liveness and Safety for Channel-Based Programming Committee Member in Program Committee within the POPL -track
Akira YoshimizuYoshimizu, Akira Univ.Tokyo The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
Tingting YuYu, Tingting Analyzing divergence in bisimulation semantics
Z Philipp ZahnZahn, Philipp University of St. Gallen Selection Equilibria of Higher-Order Games
Jakub ZalewskiZalewski, Jakub Student Volunteers in Organizing Committee for POPL 2017
Francesco Zappa NardelliZappa Nardelli, Francesco InriaItaly Committee Member in Program Committee within the POPL -track
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Verifying dynamic race detection QWIRE: A Core Language for Quantum Circuits Committee Member in Program Committee within the CPP -track ERC member in External Review Committee within the POPL -track
Noam ZeilbergerZeilberger, Noam INRIA ERC member in External Review Committee within the POPL -track
Danfeng ZhangZhang, Danfeng Pennsylvania State UniversityUnited States LightDP: Towards Automating Differential Privacy Proofs
Lijun ZhangZhang, Lijun Institute of Software, Chinese Academy of Sciences Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
Qirun ZhangZhang, Qirun University of California, DavisUnited States Session Chair of Poster Session (part of POPL Student Research Competition) Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability Committee Member in Selection Committee within the POPL Student Research Competition-track
Wenhui ZhangZhang, Wenhui Institute of software, Chinese academy of sciences Analyzing divergence in bisimulation semantics
Neng-Fa ZhouZhou, Neng-Fa CUNY Brooklyn College and Graduate Center Canonicalizing High-Level Constructs in Picat
Djordje ZikelicZikelic, Djordje University of Cambridge Stochastic Invariants for Probabilistic Termination
Beta ZilianiZiliani, Beta FAMAF, UNC (Argentina) / CONICET (Argentina)Argentina Introducing MetaCoq: A Safe Tactic Language for Coq
Théo ZimmermannZimmermann, Théo IRIF, Université Paris DiderotFrance Coq's Prolog and application to defining semi-automatic tactics
Elena ZuccaZucca, Elena University of Genova ERC member in External Review Committee within the POPL -track
Lenore ZuckZuck, Lenore Committee Member in Steering Committee for VMCAI 2017
Damien ZuffereyZufferey, Damien MIT ERC member in External Review Committee within the POPL -track
Ç Ezgi ÇiçekÇiçek, Ezgi MPI-SWS, Germany Relational Cost Analysis Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ś Adam ŚcibiorŚcibior, Adam University of Cambridge Building inference algorithms from monad transformers

POPL 2017 Contributors

Results (681)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia