POPL 2019 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (741)

A Andreas AbelAbel, Andreas Gothenburg UniversitySweden Session Chair of Dependent Types (part of POPL Research Papers) [T5] Correct-by-Construction Programming in Agda Committee Member in Program Committee within the POPL Research Papers-track
Erika AbrahamAbraham, Erika RWTH Aachen UniversityGermany Hybrid Systems Reachability Analysis Committee Member in Program Committee within the PADL-track
Luca AcetoAceto, Luca Reykjavik University Adventures in Monitorability: From Branching to Linear Time and Back Again
Antonis AchilleosAchilleos, Antonis Reykjavik University Adventures in Monitorability: From Branching to Linear Time and Back Again
Sara AchourAchour, Sara MITUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Michael D. AdamsAdams, Michael D. University of UtahUnited States Session Chair of Program Analysis I (part of POPL Research Papers) Demand Control-Flow Analysis Committee Member in Program Committee within the POPL Research Papers-track
Alejandro AguirreAguirre, Alejandro IMDEA Software Institute, Spain Formal Verification of Higher-Order Probabilistic Programs
Danel AhmanAhman, Danel University of LjubljanaSlovenia Committee Member in Program Committee within the POPL Research Papers-track
Amal AhmedAhmed, Amal Northeastern University, USAUnited States Gradual Type Theory Committee Member in Organizing Committee within the PriSC-track
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin-Madison Session Chair of Machine Learning and Linear Algebra (part of POPL Research Papers) Program Synthesis with Equivalence Reduction Trace Abstraction Modulo Probability Committee Member in Program Committee within the POPL Research Papers-track
Elvira AlbertAlbert, Elvira Committee Member in Program Committee within the PEPM-track
Karim AliAli, Karim University of Alberta Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems
Miltiadis AllamanisAllamanis, Miltiadis Microsoft Research, CambridgeUnited Kingdom Committee Member in Program Committee within the VMCAI-track
Uri AlonAlon, Uri TechnionIsrael code2vec: Learning Distributed Representations of Code
María AlpuenteAlpuente, María U.P. ValenciaSpain Committee Member in Program Committee within the PEPM-track
Thorsten AltenkirchAltenkirch, Thorsten University of Nottingham Constructing Quotient Inductive-Inductive Types
Rajeev AlurAlur, Rajeev University of PennsylvaniaUnited States Modular Quantitative Monitoring
Madhur AmilkanthwarAmilkanthwar, Madhur Facile : A Domain Specific Language and Compiler for Program Analysis and Optimization
Nada AminAmin, Nada University of CambridgeUnited Kingdom Committee Member in Program Committee within the Off the Beaten Track-track
Oana-Fabiana AndreescuAndreescu, Oana-Fabiana Internet of Trust Inferring Frame Conditions with Static Correlation Analysis
June AndronickAndronick, June Data61,CSIRO (formerly NICTA) and UNSWAustralia Committee Member in Program Committee within the POPL Research Papers-track
Étienne AndréAndré, Étienne LIPN, CNRS UMR 7030, Université Paris 13France Parametric Timed Broadcast Protocols Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking
Timos AntonopoulosAntonopoulos, Timos Yale University Committee Member in Program Committee within the VMCAI-track
Joaquin AriasArias, Joaquin Universidad Politécnica de Madrid and IMDEA Software InstituteSpain Incremental Evaluation of Lattice-Based Aggregates in Logic Programming Using Modular TCLP
Alasdair ArmstrongArmstrong, Alasdair University of Cambridge ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Kenichi AsaiAsai, Kenichi Ochanomizu UniversityJapan Extracting a Call-by-Name Partial Evaluator from a Proof of Termination
Aslan AskarovAskarov, Aslan Aarhus University Session Chair of Session 4 (part of PriSC) Modular Security Guarantees for Low-Level Languages with Stack Traversal
Alexander Asp BockAsp Bock, Alexander Static Partitioning of Spreadsheets for Parallel Execution
Robert AtkeyAtkey, Robert University of Strathclyde General Co-Chair in Organizing Committee within the Off the Beaten Track-track Committee Member in Program Committee within the POPL Research Papers-track
Mauricio Ayala-RinconAyala-Rincon, Mauricio University of BrasíliaBrazil Committee Member in Program Committee within the CPP-track
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Carnegie Mellon University, USAUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
B Domagoj BabicBabic, Domagoj Google, Inc.United States Committee Member in Program Committee within the VMCAI-track
Casper Bach PoulsenBach Poulsen, Casper Delft University of Technology Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Kyungmin BaeBae, Kyungmin Pohang University of Science and Technology (POSTECH)South Korea Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation
Alexander BakstBakst, Alexander Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Paolo BaldanBaldan, Paolo University of PadovaItaly Model Checking True Concurrency Properties Fixpoint Games on Continuous Lattices
Marcello BalducciniBalduccini, Marcello Saint Joseph's University, USA Committee Member in Program Committee within the PADL-track
Thomas BallBall, Thomas Microsoft ResearchUnited States Microsoft Research: Engage, Verify, Open
Clément BallabrigaBallabriga, Clément Static Analysis of Binary Code with Memory Indirections Using Polyhedra
Stephanie BalzerBalzer, Stephanie Carnegie Mellon University, USAUnited States Panel: Grad School and Beyond [T6] Session-Typed Concurrent Programming Panelist in Panelists within the PLMW-track Committee Member in Program Committee within the BEAT-track
Gilles BartheBarthe, Gilles IMDEA Software InstituteSpain Formal Verification of Higher-Order Probabilistic Programs Committee Member in Program Committee within the PriSC-track
Antranig BasmanBasman, Antranig Committee Member in Program Committee within the Off the Beaten Track-track
Kevin BatzBatz, Kevin RWTH Aachen University Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
Thomas BauereissBauereiss, Thomas University of Cambridge ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Christoph BaumannBaumann, Christoph KTH Confidentiality-Preserving Refinement
Atılım Güneş BaydinBaydin, Atılım Güneş Department of Engineering Science, University of Oxford Committee Member in Program Committee within the LAFI-track
Elias BenussiBenussi, Elias Imperial College London Effpi: Concurrent Programming with Dependent Behavioural Types
Véronique BenzakenBenzaken, Véronique LRI, Université Paris-SudFrance A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra
Josh BerdineBerdine, Josh Facebook Committee Member in Program Committee within the VMCAI-track
Lars BergstromBergstrom, Lars Mozilla Research Committee Member in Program Committee within the PADL-track
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Giovanni BernardiBernardi, Giovanni Université Paris DiderotFrance From Testing Preorders to Flaky Tests
Marco BernardoBernardo, Marco University of Urbino ULTraS at Work: Compositionality and Equational Characterization of Behavioral Metaequivalences
Jean-Philippe BernardyBernardy, Jean-Philippe University of Gothenburg Committee Member in Program Committee within the POPL Research Papers-track
Pramod BhatotiaBhatotia, Pramod University of Edinburgh Committee Member in Program Committee within the PriSC-track
Gavin BiermanBierman, Gavin Oracle LabsUnited Kingdom Committee Member in Program Committee within the POPL Research Papers-track
Dariusz BiernackiBiernacki, Dariusz University of Wrocław Abstracting Algebraic Effects
Lars BirkedalBirkedal, Lars Aarhus University POPL 2020 Announcement StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities Iron: Managing Obligations in Higher-Order Concurrent Separation Logic Committee Member in Program Committee within the PriSC-track
Aleš BizjakBizjak, Aleš Aarhus UniversityDenmark Iron: Managing Obligations in Higher-Order Concurrent Separation Logic Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL A Verified Prover Based on Ordered Resolution Bindings as Bounded Natural Functors
Sandrine BlazyBlazy, Sandrine Univ Rennes- IRISAFrance Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
Roderick BloemBloem, Roderick Institute of Software Technology, Graz University of Technology Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs
François BobotBobot, François CEA Exploiting Pointer Analysis in Memory Models for Deductive Verification
Laura BocchiBocchi, Laura University of KentUnited Kingdom Committee Member in Program Committee within the BEAT-track
Eric BoddenBodden, Eric Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems
Rastislav BodikBodik, Rastislav University of WashingtonUnited States Committee Member in Steering Committee for POPL 2019
Martin BodinBodin, Martin Imperial College LondonUnited Kingdom Skeletal Semantics and their Interpretations Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Filippo BonchiBonchi, Filippo University of Pisa Diagrammatic Algebra: From Linear to Concurrent Systems
Ahmed BouajjaniBouajjani, Ahmed IRIF, Université Paris DiderotFrance Committee Member in Program Committee within the VMCAI-track
Mehdi BouazizBouaziz, Mehdi Facebook LondonUnited Kingdom [T8] Building Your Own Modular Static Analyser with Infer
Quentin BouillaguetBouillaguet, Quentin Exploiting Pointer Analysis in Memory Models for Deductive Verification
Rémy BoutonnetBoutonnet, Rémy Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis
Ana BoveBove, Ana Chalmers University of Technology, Sweden Committee Member in Program Committee within the CPP-track
Jonathan BowenBowen, Jonathan London South Bank UniversityUnited Kingdom (Un)Encrypted Computing and Indistinguishability Obfuscation
William J. BowmanBowman, William J. University of British ColumbiaCanada Committee Member in Program Committee within the PriSC-track
Edwin BradyBrady, Edwin University of St. Andrews, UKUnited Kingdom Committee Member in Program Committee within the PADL-track
Martin BrainBrain, Martin Application of Abstract Interpretation to the Automotive Electronic Control System
Mario BravettiBravetti, Mario Università di BolognaItaly Getting Rid of Null-Dereferences – Behavioural Types to the Rescue
Jason BreckBreck, Jason University of Wisconsin - Madison Closed Forms for Numerical Loops Refinement of Path Expressions for Static Analysis
Peter BreuerBreuer, Peter Hecusys LLCUnited Kingdom (Un)Encrypted Computing and Indistinguishability Obfuscation
David BromanBroman, David KTH Royal Institute of TechnologySweden Composing Syntactical Constructs to Create Domain-Specific Languages
Denis BuenoBueno, Denis euforia: Complete Software Model Checking with Uninterpreted Functions
Matteo BusiBusi, Matteo Università di Pisa - Dipartimento di Informatica Translation Validation for Security Properties
C Luís CairesCaires, Luís NOVA-LINCS, FCT NOVA / Universidade Nova de LisboaPortugal A Concurrent Functional Language with Session Types and Control Effects Based on Linear Logic
Georgiana CaltaisCaltais, Georgiana University of Konstanz Causal Reasoning for Safety
Brian CampbellCampbell, Brian University of Edinburgh ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Mauricio CanoCano, Mauricio Two Declarative Approaches for Session-Based Concurrency
Qinxiang CaoCao, Qinxiang Shanghai Jiao Tong UniversityChina Session Chair of Contributed Talks 3 & Coq Developers (part of CoqPL) Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs
Xinya CaoCao, Xinya Nankai University, China Method Name Suggestion with Hierarchical Attention Networks
Manuel CarroCarro, Manuel IMDEA Software Institute and T.U. of Madrid (UPM)Spain Incremental Evaluation of Lattice-Based Aggregates in Logic Programming Using Modular TCLP Committee Member in Program Committee within the PADL-track
Giuseppe CastagnaCastagna, Giuseppe CNRS - Université Paris Diderot, FranceFrance Committee Member in Steering Committee for POPL 2019 Gradual Typing: A New Perspective
Simon CastellanCastellan, Simon Probabilistic Programming Inference via Intensional Semantics
Simon CastellanCastellan, Simon Imperial College London, UK Two sides of the same coin: Session Types and Game Semantics
Ilaria CastellaniCastellani, Ilaria INRIA Sophia Antipolis, FranceFrance Session Chair of Session Types (part of OPCT) Global Types with Internal Delegation Committee Member in Organizing Committee within the OPCT-track
Valentina CastiglioniCastiglioni, Valentina Inria Saclay - Ile de France A Metric Semantics for Coordination Languages
David Castro-PerezCastro-Perez, David Imperial College LondonUnited Kingdom Distributed Programming using Role-Parametric Session Types in Go
Sunjay CauligiCauligi, Sunjay UCSD CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Evan CavalloCavallo, Evan Carnegie Mellon University Higher Inductive Types in Cubical Computational Type Theory
Pavol CernyCerny, Pavol University of Colorado BoulderSlovakia Type-directed Bounding of Collections in Reactive Programs
Andrea CeroneCerone, Andrea Imperial College London A Uniform Framework of Transactional Consistency Models for Protocol Verification and Program Analysis
Soham ChakrabortyChakraborty, Soham Max Planck Institute for Software Systems Grounding Thin-Air Reads with Event Structures
Bor-Yuh Evan ChangChang, Bor-Yuh Evan University of Colorado Boulder Type-directed Bounding of Collections in Reactive Programs
Krishnendu ChatterjeeChatterjee, Krishnendu IST Austria Termination of Nondeterministic Probabilistic Programs Efficient Parameterized Algorithms for Data Packing
Kaustuv ChaudhuriChaudhuri, Kaustuv Inria, FranceFrance A Proof-Theoretic Approach to Certifying Skolemization
Swarat ChaudhuriChaudhuri, Swarat Rice University Committee Member in Program Committee within the POPL Research Papers-track
Liqian ChenChen, Liqian National University of Defense TechnologyChina Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Taolue ChenChen, Taolue Birkbeck, University of London Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Zilin ChenChen, Zilin Data61, CSIRO and UNSWAustralia A Data Layout Description Language for Cogent
Wei-Ngan ChinChin, Wei-Ngan National University of Singapore Automatic Program Repair using Formal Verification and Expression Templates
David ChisnallChisnall, David University of Cambridge Committee Member in Program Committee within the PriSC-track
Amit ChopraChopra, Amit Lancaster University, UK [T2] Engineering Distributed Systems via Protocols and Commitments
Ravi ChughChugh, Ravi University of Chicago Live Functional Programming with Typed Holes
Luke ChurchChurch, Luke Session Chair of Afternoon Talks (part of Off the Beaten Track) Session Chair of Keynote (part of Off the Beaten Track) Design Critique and Discussion Chair in Program Committee within the Off the Beaten Track-track
Pierre ClairambaultClairambault, Pierre CNRS & ENS LyonFrance Game Semantics for Quantum Programming
Rance CleavelandCleaveland, Rance University of Maryland NSF funding for PL
Jesper CockxCockx, Jesper Chalmers \| University of GothenburgSweden Definitional Proof-Irrelevance without K [T5] Correct-by-Construction Programming in Agda Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tiago CogumbreiroCogumbreiro, Tiago University of Massachusetts BostonUnited States Hardware Interactions as Behavioural Types
Alexander CollinsCollins, Alexander NVIDIA Probabilistic Programming with CuPPL
Breandan ConsidineConsidine, Breandan Université de MontréalUnited States Kotlin∇: Differentiable Functional Programming with Algebraic Data Types
Evelyne ContejeanContejean, Evelyne A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra
William CookCook, William University of Texas at Austin Committee Member in Program Committee within the PEPM-track
Stefania CostantiniCostantini, Stefania Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Univ. dell'Aquila Committee Member in Program Committee within the PADL-track
Patrick CousotCousot, Patrick A^2 I: Abstract^2 Interpretation
Patrick M. CousotCousot, Patrick M. Session Chair of Abstract Interpretation (1) (part of VMCAI) Committee Member in Program Committee within the VMCAI-track
Karl CraryCrary, Karl Carnegie Mellon University Fully Abstract Module Compilation
Ryan CulpepperCulpepper, Ryan Czech Technical UniversityCzech Republic Committee Member in Program Committee within the LAFI-track
Marco Cusumano-TownerCusumano-Towner, Marco MIT-CSAIL Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
John CyphertCyphert, John University of Wisconsin - Madison Closed Forms for Numerical Loops Refinement of Path Expressions for Static Analysis
D Emanuele D'OsualdoD'Osualdo, Emanuele Imperial College London, UKUnited Kingdom Compositional Reasoning for Termination of Fine-grained Concurrent Programs
Ugo Dal LagoDal Lago, Ugo University of Bologna, Italy / Inria, FranceItaly The Geometry of Bayesian Programming Invited Talk: On Type-Based Complexity Analysis of Programs and Processes Intersection Types and Runtime Errors in the Pi-Calculus [T7] Higher-Order Probabilistic Programming
Mads DamDam, Mads KTH Confidentiality-Preserving Refinement
Nils Anders DanielssonDanielsson, Nils Anders University of Gothenburg, Chalmers University of Technology Committee Member in Program Committee within the POPL Research Papers-track
Olivier DanvyDanvy, Olivier Yale-NUS College, SingaporeSingapore Committee Member in Program Committee within the CoqPL-track
Ornela DardhaDardha, Ornela University of GlasgowUnited Kingdom Committee Member in Program Committee within the PADL-track
Ankush DasDas, Ankush Carnegie Mellon UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tamino DauthDauth, Tamino Karlsruhe University of Applied Sciences, Germany Futures and Promises in Haskell and Scala Advanced Futures and Promises in C++ (poster)
Brooks DavisDavis, Brooks SRI International Exploring C Semantics and Pointer Provenance
Wolfgang De MeuterDe Meuter, Wolfgang Vrije Universiteit Brussel Effect-driven Flow Analysis
Rocco De NicolaDe Nicola, Rocco Attribute Based Communication for Collective Adaptive Systems
Coen De RooverDe Roover, Coen Vrije Universiteit BrusselBelgium Effect-driven Flow Analysis
Marc De VismeDe Visme, Marc ENS Lyon Intersection Types and Runtime Errors in the Pi-Calculus Game Semantics for Quantum Programming
Søren DeboisDebois, Søren IT University of Copenhagen Towards Legally Compliant Governmental Case Work with Dynamic Condition Response Graphs
Normann DeckerDecker, Normann Flat Model Checking for Counting LTL using Quantifier-free Presburger Arithmetic
Pierpaolo DeganoDegano, Pierpaolo Università di Pisa - Dipartimento di Informatica Translation Validation for Security Properties
Benoit DelahayeDelahaye, Benoit Parametric Timed Broadcast Protocols
Benjamin DelawareDelaware, Benjamin Purdue University Artifact Evaluation Co-Chair in Organizing Committee for POPL 2019 Session Chair of Type Abstraction and Effects (part of POPL Research Papers) A Verified Protocol Buffer Compiler Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Program Committee within the POPL Research Papers-track
Dominique DevrieseDevriese, Dominique Vrije Universiteit Brussel, BelgiumBelgium Session Chair of Session 2 (part of PriSC) StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities Committee Member in Organizing Committee within the PriSC-track PC Co-Chair in Program Committee within the PriSC-track Committee Member in Selection Committee within the POPL Student Research Competition-track
Mariangiola DezaniDezani, Mariangiola Università di TorinoItaly Global Types with Internal Delegation
Cinzia Di GiustoDi Giusto, Cinzia Laboratoire I3S Multiparty Reactive Sessions
Matthew Di MeglioDi Meglio, Matthew UNSW A Data Layout Description Language for Cogent
Daniel DietschDietsch, Daniel University of Freiburg Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Thomas Dinsdale-YoungDinsdale-Young, Thomas WIP: Formalizing the Concordium Consensus Protocol in Coq
Craig DisselkoenDisselkoen, Craig University of California San Diego Trestle: Bridging the Performance and Safety Divide in WebAssembly
Marko DokoDoko, Marko MPI-SWS, Germany On Library Correctness under Weak Memory Consistency
Dana Drachsler CohenDrachsler Cohen, Dana ETH ZurichSwitzerland Committee Member in Program Committee within the PEPM-track
Iulia DragomirDragomir, Iulia Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
Samuel DrewsDrews, Samuel University of Wisconsin-Madison Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Cezara DrăgoiDrăgoi, Cezara INRIA, ENS, CNRSFrance Session Chair of Networks and Concurrency (part of VMCAI) Committee Member in Program Committee within the VMCAI-track
Andrej DudenhefnerDudenhefner, Andrej Technical University Dortmund Principality and Approximation under Dimensional Bound
Jana DunfieldDunfield, Jana Queen's University, Kingston, OntarioCanada Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
Aaron DutleDutle, Aaron Committee Member in Program Committee within the CPP-track
David Kristjanson DuvenaudDuvenaud, David Kristjanson University of Toronto Committee Member in Program Committee within the LAFI-track
Sara DécovaDécova, Sara Exceptional Asynchronous Session Types: Session Types without Tiers
Maxime DénèsDénès, Maxime INRIA Session with the Coq Development Team
E Harley D. Eades IIIEades III, Harley D. Augusta UniversityUnited States [T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning
Manuel EberlEberl, Manuel Technische Universität MünchenGermany Verified Solving and Asymptotics of Linear Recurrences
Søren Eller ThomsenEller Thomsen, Søren Aarhus UniversityDenmark WIP: Formalizing the Concordium Consensus Protocol in Coq
Michael EmmiEmmi, Michael SRI InternationalUnited States Session Chair of Program Analysis II (part of POPL Research Papers) Weak-Consistency Specification via Visibility Relaxation Committee Member in Program Committee within the POPL Research Papers-track
Constantin EneaEnea, Constantin Université Paris DiderotFrance Session Chair of Invited Talk 1 (part of VMCAI) Weak-Consistency Specification via Visibility Relaxation Co-chair in Organizing Committee within the VMCAI-track Program Co-Chair in Program Committee within the VMCAI-track
Esra ErdemErdem, Esra Sabanci University, Turkey Personalized Course Schedule Planning using Answer Set Programming Committee Member in Program Committee within the PADL-track
Martin ErwigErwig, Martin Oregon State UniversityUnited States Committee Member in Program Committee within the POPL Research Papers-track Steering Committee Member in Steering Committee within the PEPM-track
Javier EsparzaEsparza, Javier Committee Member in Program Committee within the VMCAI-track
Gregory EssertelEssertel, Gregory Purdue University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
F Wolfgang FaberFaber, Wolfgang Alpen-Adria-Universität, Austria Committee Member in Program Committee within the PADL-track
Claudia FaggianFaggian, Claudia IRIFFrance Probabilistic Lambda Calculus: Beyond Deterministic Evaluation
Frantisek FarkaFarka, Frantisek Proof Carrying Plans
Grigory FedyukovichFedyukovich, Grigory Princeton UniversityUnited States Session Chair of Software Verification (part of VMCAI) Lazy but Effective Functional Synthesis
Bertram FelgenhauerFelgenhauer, Bertram A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Amy FeltyFelty, Amy University of OttawaCanada A Linear Logical Framework in Hybrid
Jerome FeretFeret, Jerome INRIA ParisFrance Committee Member in Program Committee within the VMCAI-track
Carla FerreiraFerreira, Carla Universidade Nova Lisboa IPA: Invariant-preserving Applications for Weakly Consistent Replicated Databases
Robby FindlerFindler, Robby Northwestern University, USAUnited States A Calculus for Esterel: If can, can. If no can, no can.
Spencer P. FlorenceFlorence, Spencer P. Northwestern University, USA A Calculus for Esterel: If can, can. If no can, no can.
Shaked FlurFlur, Shaked University of Cambridge ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Julien ForgetForget, Julien Static Analysis of Binary Code with Memory Indirections Using Polyhedra
Yannick ForsterForster, Yannick Saarland UniversityGermany On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Nate FosterFoster, Nate Cornell UniversityUnited States Committee Member in Program Committee within the POPL Research Papers-track
Cédric FournetFournet, Cédric Microsoft Research Committee Member in Program Committee within the PriSC-track
Paulin FournierFournier, Paulin Parametric Timed Broadcast Protocols
Simon FowlerFowler, Simon The University of EdinburghUnited Kingdom Exceptional Asynchronous Session Types: Session Types without Tiers
Gereon FoxFox, Gereon Syntactic Partial Order Compression for Probabilistic Reachability
Adrian FrancalanzaFrancalanza, Adrian University of MaltaMalta Session Chair of Session 4 (part of BEAT) Getting Rid of Null-Dereferences – Behavioural Types to the Rescue A Foundation for Runtime Enforcement Adventures in Monitorability: From Branching to Linear Time and Back Again Committee Member in Program Committee within the BEAT-track
Cameron FreerFreer, Cameron Remine and BorelianUnited States Committee Member in Steering Committee within the LAFI-track
Jon FrenchFrench, Jon University of Cambridge ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Laurent FribourgFribourg, Laurent Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking
Aymeric FromherzFromherz, Aymeric Carnegie Mellon University A Verified, Efficient Embedding of a Verifiable Assembly Language
Hongfei FuFu, Hongfei IST Austria Termination of Nondeterministic Probabilistic Programs
G Marco GaboardiGaboardi, Marco University at Buffalo, SUNYUnited States Workshops Co-Chair in Organizing Committee for POPL 2019 Formal Verification of Higher-Order Probabilistic Programs Committee Member in Tutorials Evaluation Committee within the POPL TutorialFest-track
John P. GallagherGallagher, John P. Roskilde University Committee Member in Program Committee within the PEPM-track
Emilio Jesús Gallego AriasGallego Arias, Emilio Jesús INRIAFrance Coq User Interfaces: Past, Present, and Future (Keynote)
Letterio GallettaGalletta, Letterio IMT School for Advanced Studies Translation Validation for Security Properties
Ronald GarciaGarcia, Ronald University of British Columbia Type-Driven Gradual Security with References
Philippa GardnerGardner, Philippa Imperial College London Session Chair of Cyberphysical Systems, Hybrid Systems (part of OPCT) Panel: How to Do Good PL Research JaVerT 2.0: Compositional Symbolic Execution for JavaScript Skeletal Semantics and their Interpretations Panelist in Panelists within the PLMW-track
Tal GarfinkelGarfinkel, Tal Stanford University Trestle: Bridging the Performance and Safety Divide in WebAssembly
Deepak GargGarg, Deepak Max Planck Institute for Software SystemsGermany Session Chair of Session 1 (part of PriSC) Panel: How to Do Good PL Research From Fine- to Coarse-Grained Dynamic Information Flow Control and Back Formal Verification of Higher-Order Probabilistic Programs Panelist in Panelists within the PLMW-track Committee Member in Organizing Committee within the PriSC-track PC Co-Chair in Program Committee within the PriSC-track
Jacques GarrigueGarrigue, Jacques Nagoya UniversityJapan Committee Member in Program Committee within the POPL Research Papers-track
Marco GavanelliGavanelli, Marco Universita di FerraraItaly Committee Member in Program Committee within the PADL-track
Martin GebserGebser, Martin University of Potsdam, Germany Committee Member in Program Committee within the PADL-track
Timon GehrGehr, Timon An Abstract Domain for Certifying Neural Networks
Alex GerdesGerdes, Alex University of Gothenburg, SwedenSweden Committee Member in Program Committee within the PADL-track
Kimball GermaneGermane, Kimball University of Utah Relatively Complete Pushdown Analysis of Escape Continuations Demand Control-Flow Analysis
Lorenzo GheriGheri, Lorenzo Middlesex University London Bindings as Bounded Natural Functors
Khalil GhorbalGhorbal, Khalil Committee Member in Program Committee within the VMCAI-track
Roberto GiacobazziGiacobazzi, Roberto University of Verona and IMDEA Software InstituteItaly Session Chair of Session 4 (part of PEPM) A^2 I: Abstract^2 Interpretation Committee Member in Program Committee within the PEPM-track Committee Member in Program Committee within the VMCAI-track
Nick GiannarakisGiannarakis, Nick Princeton University A Verified, Efficient Embedding of a Verifiable Assembly Language
Paola GianniniGiannini, Paola Universita' del Piemonte OrientaleItaly Session Chair of Session 3 (part of BEAT) Global Types with Internal Delegation Committee Member in Program Committee within the BEAT-track
Jeremy GibbonsGibbons, Jeremy Department of Computer Science, University of OxfordUnited Kingdom Committee Member in Steering Committee for POPL 2019
Gaetan GilbertGilbert, Gaetan Definitional Proof-Irrelevance without K
Klaus v. GleissenthallGleissenthall, Klaus v. University of California at San Diego, USA Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Milos GligoricGligoric, Milos University of Texas at AustinUnited States Verifying Finality for Blockchain Systems
Robert GlückGlück, Robert University of CopenhagenDenmark Committee Member in Program Committee within the PEPM-track
Amir Kafshdar GoharshadyGoharshady, Amir Kafshdar IST AustriaAustria Efficient Parameterized Algorithms for Data Packing
Sophia GoldGold, Sophia Tezos Session Chair of C (part of LAFI) Committee Member in Program Committee within the LAFI-track
Victor B. F. GomesGomes, Victor B. F. University of Cambridge, UK Exploring C Semantics and Pointer Provenance
Laure GonnordGonnord, Laure University of Lyon & LIP, FranceFrance Static Analysis of Binary Code with Memory Indirections Using Polyhedra
Georges GonthierGonthier, Georges Inria Session Chair of Research Papers: Formalization of Mathematics and Computer Algebra (part of CPP)
Kiran GopinathanGopinathan, Kiran University College LondonUnited Kingdom Towards Mechanising Probabilistic Properties of a Blockchain
Andrew D. GordonGordon, Andrew D. Microsoft Research and University of EdinburghUnited Kingdom Committee Member in Steering Committee for POPL 2019 Session Chair of Session Types II (part of POPL Research Papers) Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic Committee Member in Steering Committee within the LAFI-track
Maria I. GorinovaGorinova, Maria I. The University of Edinburgh Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic
Nikos GorogiannisGorogiannis, Nikos [T8] Building Your Own Modular Static Analyser with Infer A True Positives Theorem for a Static Race Detector
Marc GourjonGourjon, Marc Hamburg University of Technology and NXP Semiconductors Germany GmbH Towards Secure Compilation of Power Side-Channel Countermeasures
Daniel GratzerGratzer, Daniel Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Kathryn E. GrayGray, Kathryn E. University of Cambridge ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Michael GreenbergGreenberg, Michael Pomona College Publicity Chair in Organizing Committee for POPL 2019 Session Chair of Verified Compilation and Concurrency (part of POPL Research Papers) Session Chair of Morning Papers (part of Off the Beaten Track) Teaching Discrete Mathematics to Early Undergraduates with Software Foundations General Co-Chair in Organizing Committee within the Off the Beaten Track-track Committee Member in Program Committee within the POPL Research Papers-track
Benjamin GregoireGregoire, Benjamin INRIA PriSC Keynote - Jasmin: A Compiler and Framework for High-Assurance and High-Speed Cryptography
Alberto GriggioGriggio, Alberto Fondazione Bruno KesslerItaly Committee Member in Program Committee within the VMCAI-track
Radu GrigoreGrigore, Radu University of KentUnited Kingdom Committee Member in Program Committee within the POPL Research Papers-track
Dan GrossmanGrossman, Dan University of WashingtonUnited States Concerto: A Framework for Combined Concrete and Abstract Interpretation
Vinod GroverGrover, Vinod NVIDIAUnited States Probabilistic Programming with CuPPL
Samuel GruetterGruetter, Samuel Massachusetts Institute of Technology Counterexamples for Coq Conjectures
Ronghui GuGu, Ronghui Columbia University, USAUnited States Committee Member in Program Committee within the CoqPL-track
Roberto GuancialeGuanciale, Roberto KTH Confidentiality-Preserving Refinement
Khilan GudkaGudka, Khilan University of Cambridge Protecting C++ Applications Using CHERI
Elsa GunterGunter, Elsa University of IllinoisUnited States Dynamic Class Initialization Semantics: a Jinja Extension
Chenkai GuoGuo, Chenkai Nankai University, China Method Name Suggestion with Hierarchical Attention Networks
Aarti GuptaGupta, Aarti Princeton University Lazy but Effective Functional Synthesis
Gopal GuptaGupta, Gopal An ASP-based Approach to Representing and Querying Textual Knowledge
Arie GurfinkelGurfinkel, Arie University of WaterlooCanada Lazy but Effective Functional Synthesis
H Thomas H. HildebrandtH. Hildebrandt, Thomas Session Chair of Causality, Reversibility (part of OPCT) Towards Legally Compliant Governmental Case Work with Dynamic Condition Response Graphs
Stefan HaarHaar, Stefan Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics
Jurriaan HageHage, Jurriaan Utrecht University Committee Member in Program Committee within the PADL-track
Matthew HagueHague, Matthew Royal Holloway, University of London CSS Minification via Constraint Solving Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Nicolas HalbwachsHalbwachs, Nicolas Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis
Kevin HamlenHamlen, Kevin University of Texas at Dallas, USA Committee Member in Program Committee within the PADL-track
Matthew HammerHammer, Matthew NoneUnited States Live Functional Programming with Typed Holes Committee Member in Program Committee within the Off the Beaten Track-track Committee Member in Program Committee within the POPL Research Papers-track
Kevin HammondHammond, Kevin University of St. Andrews, UK Proof Carrying Plans
Jad HamzaHamza, Jad LIAFA, Université Paris Diderot Minimal Synthesis of String To String Functions From Examples
Helle Hvid HansenHansen, Helle Hvid Delft University of Technology A (Co)algebraic Approach to Hennessy-Milner Theorems for Weakly Expressive Logics
Michael HanusHanus, Michael Kiel UniversityGermany Improving Residuation in Declarative Programs
Mark HarmanHarman, Mark Facebook and University College LondonUnited Kingdom Automated Fault-Finding and Fixing at Facebook
Robert HarperHarper, Robert Higher Inductive Types in Cubical Computational Type Theory A Separation Logic for Concurrent Randomized Programs
Ichiro HasuoHasuo, Ichiro National Institute of Informatics, JapanJapan Committee Member in Program Committee within the POPL Research Papers-track
Chris HawblitzelHawblitzel, Chris Microsoft Research Session Chair of Research Papers: Program Verification (part of CPP) A Verified, Efficient Embedding of a Verifiable Assembly Language Committee Member in Program Committee within the CPP-track
Matthew HeimerdingerHeimerdinger, Matthew Indiana University Verified Equational Reasoning on a Little Language of Measures
Fritz HengleinHenglein, Fritz Department of Computer Science, University of Copenhagen (DIKU)Denmark Committee Member in Steering Committee for POPL 2019 General Chair in Organizing Committee for POPL 2019 Welcome Steering Committee Member in Steering Committee within the PEPM-track
Hugo HerbelinHerbelin, Hugo Committee Member in Program Committee within the POPL Research Papers-track
Holger HermannsHermanns, Holger Saarland UniversityGermany Syntactic Partial Order Compression for Probabilistic Reachability
Manuel HermenegildoHermenegildo, Manuel IMDEA Software Institute and T.U. of Madrid (UPM) Session Chair of Session 1 (part of PEPM) Session Chair of (part of PEPM) Welcome to PEPM19 Program Co-Chair in Program Committee within the PEPM-track
Michael HicksHicks, Michael University of Maryland, College ParkUnited States Chair in Steering Committee for POPL 2019 Session Chair of Type Inference I (part of POPL Research Papers) Technical Talk: What Is Programming Languages Research? Quantitative Robustness Analysis of Quantum Programs LWeb: Information Flow Security for Multi-Tier Web Applications Speaker in Speakers within the PLMW-track Committee Member in Selection Committee within the POPL Student Research Competition-track
Kesha HietalaHietala, Kesha University of Maryland Quantitative Robustness Analysis of Quantum Programs
Alasdair HillHill, Alasdair Proof Carrying Plans
Nick HippenHippen, Nick Automatic Program Rewriting in Non-Ground Answer Set Programs
Tom HirschowitzHirschowitz, Tom Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 ChambéryFrance Familial Monads and Structural Operational Semantics
Aquinas HoborHobor, Aquinas Committee Member in Program Committee within the CPP-track
Jochen HoenickeHoenicke, Jochen Universität FreiburgGermany Solving and Interpolating Constant Arrays Based on Weak Equivalences
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Session Chair of Reasoning about Probabilistic Programs (part of POPL Research Papers) Invited Talk: Resource-Aware Session Types Type-Guided Worst-Case Input Generation Committee Member in Program Committee within the POPL Research Papers-track
Joshua HollandHolland, Joshua University of Southampton Diagrammatic Algebra: From Linear to Concurrent Systems
Steven HoltzenHoltzen, Steven University of California, Los AngelesUnited States Session Chair of B (part of LAFI) Factorized Exact Inference for Discrete Probabilistic Programs Committee Member in Program Committee within the LAFI-track
Chih-Duo HongHong, Chih-Duo University of OxfordTaiwan CSS Minification via Constraint Solving
Jaemin HongHong, Jaemin KAIST, South KoreaSouth Korea Polymorphic Symmetric Multiple Dispatch with Variance
Wolf HonoreHonore, Wolf From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Ross HorneHorne, Ross Computer Science and Communications Research Unit, University of Luxembourg Global Types with Internal Delegation
Naohiko HoshinoHoshino, Naohiko Kyoto University The Geometry of Bayesian Programming
Farzin HoushmandHoushmand, Farzin University of California, RiversideUnited States Hamsaz: Replication Coordination Analysis and Synthesis
Cătălin HriţcuHriţcu, Cătălin Inria Paris Artifact Evaluation Co-Chair in Organizing Committee for POPL 2019 Committee Member in Organizing Committee within the PriSC-track Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Justin HsuHsu, Justin University of Wisconsin-Madison, USAUnited States Session Chair of Probabilistic Programming and Semantics (part of POPL Research Papers) Session Chair of Probabilistic Systems (part of VMCAI) Trace Abstraction Modulo Probability Formal Verification of Higher-Order Probabilistic Programs Organizer in Organizing Committee within the PLMW-track Committee Member in Program Committee within the POPL Research Papers-track
Raymond HuHu, Raymond Imperial College London Distributed Programming using Role-Parametric Session Types in Go
Zhenjiang HuHu, Zhenjiang National Institute of InformaticsJapan Committee Member in Program Committee within the POPL Research Papers-track
Christian HumerHumer, Christian Oracle Labs, SwitzerlandSwitzerland Applying Futamura Projections to Compose Languages and Tools in GraalVM (Invited Talk)
Shih-Han HungHung, Shih-Han University of Maryland Quantitative Robustness Analysis of Quantum Programs
Chung-Kil HurHur, Chung-Kil Seoul National UniversityKorea, South Session Chair of Session 3 (part of PriSC) Committee Member in Program Committee within the PriSC-track
Rémi HutinHutin, Rémi IRISA / ENS RennesFrance Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
Richard HuybersHuybers, Richard A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization
Johannes HölzlHölzl, Johannes Vrije Universiteit AmsterdamNetherlands Committee Member in Program Committee within the CPP-track
Hans HüttelHüttel, Hans Department of Computer Science, Aalborg UniversityDenmark Getting Rid of Null-Dereferences – Behavioural Types to the Rescue Processes as Names?
I Atsushi IgarashiIgarashi, Atsushi Kyoto University, JapanJapan Session Chair of Session 3 (part of PEPM) Panel: How to Do Good PL Research Welcome to PEPM19 Gradual Session Types in Imperative Style Dynamic Type Inference for Gradual Hindley–Milner Typing Panelist in Panelists within the PLMW-track Program Co-Chair in Program Committee within the PEPM-track
Yosikazu ImaiImai, Yosikazu Application of Abstract Interpretation to the Automotive Electronic Control System
Fabian ImmlerImmler, Fabian Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
Jeevana Priya InalaInala, Jeevana Priya MITUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Anna IngolfsdottirIngolfsdottir, Anna Reykjavik University Adventures in Monitorability: From Branching to Linear Time and Back Again
Naoki IwayamaIwayama, Naoki University of Tokyo, Japan Combining Higher-Order Model Checking with Refinement Type Inference
J Suresh JagannathanJagannathan, Suresh Purdue University Committee Member in Program Committee within the POPL Research Papers-track
Barry JayJay, Barry University of Technology Sydney A Simpler Lambda Calculus
Alan JeffreyJeffrey, Alan Mozilla ResearchUnited States Committee Member in Program Committee within the PriSC-track Committee Member in Program Committee within the POPL Research Papers-track
Thomas P. JensenJensen, Thomas P. INRIA Rennes Session Chair of Session 2 (part of PEPM) Inferring Frame Conditions with Static Correlation Analysis Skeletal Semantics and their Interpretations Committee Member in Program Committee within the PEPM-track
Ranjit JhalaJhala, Ranjit University of California, San DiegoUnited States Committee Member in Steering Committee for POPL 2019 Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Tao JiJi, Tao National University of Defense TechnologyChina Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Patricia JohannJohann, Patricia Appalachian State University Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the POPL Research Papers-track
Moa JohanssonJohansson, Moa Chalmers University of TechnologySweden PADL Opening and Welcome PC Co-Chair in Organizing Committee within the PADL-track
Matthew JohnsonJohnson, Matthew Google Brain Committee Member in Program Committee within the LAFI-track
Sung-Shik JongmansJongmans, Sung-Shik Open University of the Netherlands Distributed Programming using Role-Parametric Session Types in Go Committee Member in Program Committee within the BEAT-track
José Julio AlferesJulio Alferes, José NOVA LINCS -- Universidade Nova de LisboaPortugal PADL Opening and Welcome PC Co-Chair in Organizing Committee within the PADL-track
Kristoffer Just Arndal AndersenJust Arndal Andersen, Kristoffer Aarhus UniversityDenmark Distributed Protocol Combinators
K Jonas KaiserKaiser, Jonas Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
Benjamin Lucien KaminskiKaminski, Benjamin Lucien RWTH Aachen University; University College London Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom A Domain Theory for Statistical Probabilistic Programming Co-chair in Program Committee within the LAFI-track
Jeehoon KangKang, Jeehoon Seoul National UniversityKorea, South Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ambrus KaposiKaposi, Ambrus University of Nottingham Constructing Quotient Inductive-Inductive Types
Anja KarlKarl, Anja Institute of Applied Information Processing and Communications, Graz University of TechnologyAustria Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Bayes meets Dijkstra: Verifying Bayes Networks by Program Verification Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
Alex KavvosKavvos, Alex Wesleyan UniversityUnited States Modalities, Cohesion, and Information Flow
Yoshiumi KawamuraKawamura, Yoshiumi Application of Abstract Interpretation to the Automotive Electronic Control System
Stephen KellKell, Stephen University of Kent De-escalating Software (Keynote) Exploring C Semantics and Pointer Provenance
Chantal KellerKeller, Chantal LRI, Université Paris-SudFrance Committee Member in Program Committee within the CPP-track
Gabriele KellerKeller, Gabriele Utrecht UniversityAustralia A Data Layout Description Language for Cogent Committee Member in Program Committee within the PriSC-track
Muhammed Kerem KahramanKerem Kahraman, Muhammed Personalized Course Schedule Planning using Answer Set Programming
Rami Gökhan KıcıKıcı, Rami Gökhan University of California at San Diego, USA Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Zachary KincaidKincaid, Zachary Princeton UniversityUnited States Workshops Co-Chair in Organizing Committee for POPL 2019 A Practical Algorithm for Structure Embedding Closed Forms for Numerical Loops Refinement of Path Expressions for Static Analysis Committee Member in Tutorials Evaluation Committee within the POPL TutorialFest-track
Dominik KirstKirst, Dominik Saarland UniversityGermany On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Oleg KiselyovKiselyov, Oleg Generating Mutually Recursive Definitions
Gerwin KleinKlein, Gerwin UNSW, Australia Committee Member in Program Committee within the CPP-track
Hsiang-Shang ‘Josh’ KoKo, Hsiang-Shang ‘Josh’ National Institute of Informatics, JapanTaiwan Website Chair in Organizing Committee for POPL 2019 Steering Committee Member in Steering Committee within the PEPM-track
Kaede KobayashiKobayashi, Kaede Kyoto University Gradual Session Types in Imperative Style
Naoki KobayashiKobayashi, Naoki University of Tokyo, Japan Combining Higher-Order Model Checking with Refinement Type Inference Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking
Nicolas KohKoh, Nicolas From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Wen KokkeKokke, Wen University of EdinburghUnited Kingdom Better Late Than Never: A Fully Abstract Semantics for Classical Processes
Juraj KolčákKolčák, Juraj LSV, CNRS & ENS Cachan, University Paris SaclaySlovakia Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University, UK Proof Carrying Plans Committee Member in Program Committee within the PADL-track
Dimitrios KouzapasKouzapas, Dimitrios University of Cyprus Behavioral Types as a Semantic Foundation for the GDPR Notion of Purpose
András KovácsKovács, András Eötvös Loránd University Constructing Quotient Inductive-Inductive Types
Robbert KrebbersKrebbers, Robbert Delft University of TechnologyNetherlands Session Chair of Synthesis (part of POPL Research Papers) Session Chair of Contributed Talks 4 (part of CoqPL) Iron: Managing Obligations in Higher-Order Concurrent Separation Logic Committee Member in Program Committee within the POPL Research Papers-track Co-chair in Organizing Committee within the CoqPL-track
Jan KretinskyKretinsky, Jan Committee Member in Program Committee within the VMCAI-track
Neel KrishnaswamiKrishnaswami, Neel Computer Laboratory, University of Cambridge Panel: How to Do Good PL Research ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types Panelist in Panelists within the PLMW-track
Joachim KristensenKristensen, Joachim DIKU, University of CopenhagenDenmark F a Language for Music Composition
Jean KrivineKrivine, Jean CNRSFrance A Calculus of Branching Processes
K Narayan KumarKumar, K Narayan Chennai Mathematical InstituteIndia Committee Member in Program Committee within the VMCAI-track
Ramana KumarKumar, Ramana DeepMindUnited Kingdom Committee Member in Program Committee within the PADL-track
Viktor KunčakKunčak, Viktor EPFL, Switzerland Minimal Synthesis of String To String Functions From Examples Committee Member in Program Committee within the PEPM-track
Barbara KönigKönig, Barbara University of Duisburg-Essen Session Chair of Algebra, Coalgebra, Model Checking (part of OPCT) Fixpoint Games on Continuous Lattices
L Alfons LaarmanLaarman, Alfons Leiden UniversityNetherlands A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization
Elizabeth LabradaLabrada, Elizabeth University of Chile Gradual Parametricity, Revisited
Ori LahavLahav, Ori Tel Aviv University Session Chair of Concurrency (part of POPL Research Papers) Session Chair of Software Verification and Synthesis (part of VMCAI) On the Semantics of Snapshot Isolation Bridging the Gap Between Programming Languages and Hardware Weak Memory Models On Library Correctness under Weak Memory Consistency Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the POPL Research Papers-track Committee Member in Program Committee within the VMCAI-track
Leonidas LampropoulosLampropoulos, Leonidas University of PennsylvaniaGreece [T1] QuickChick: Property-Based Testing in Coq
Victor LanvinLanvin, Victor IRIF, Université Paris Diderot, FranceFrance Gradual Typing: A New Perspective
Dominique Larchey-WendlingLarchey-Wendling, Dominique CNRS, LORIAFrance Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Ken Friis LarsenLarsen, Ken Friis DIKU, University of CopenhagenDenmark F a Language for Music Composition
Julia LawallLawall, Julia Inria/LIP6 Committee Member in Program Committee within the PEPM-track
Jia LeeLee, Jia Pohang University of Science and Technology (POSTECH) Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation
Karoliina LehtinenLehtinen, Karoliina University of Kiel and University of Liverpool Adventures in Monitorability: From Branching to Linear Time and Back Again
Nicola LeoneLeone, Nicola University of Calabria, Italy Committee Member in Program Committee within the PADL-track
Mohsen LesaniLesani, Mohsen University of California, Riverside Hamsaz: Replication Coordination Analysis and Synthesis
Stéphane LescuyerLescuyer, Stéphane Prove & Run Inferring Frame Conditions with Static Correlation Analysis
Michael LeuschelLeuschel, Michael University of Düsseldorf Committee Member in Program Committee within the PEPM-track
Omer LevyLevy, Omer University of Washington, USA code2vec: Learning Distributed Representations of Code
Robert Y. LewisLewis, Robert Y. Vrije Universiteit AmsterdamNetherlands A Formal Proof of Hensel's Lemma over the p-adic Integers
Wenda LiLi, Wenda University of Cambridge Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem
Yao LiLi, Yao University of PennsylvaniaUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Yishuai LiLi, Yishuai University of PennsylvaniaUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Hongjin LiangLiang, Hongjin Nanjing University, ChinaChina Committee Member in Program Committee within the POPL Research Papers-track
Percy LiangLiang, Percy Stanford University FrAngel: Component-Based Synthesis with Control Structures
Dan LicataLicata, Dan Wesleyan UniversityUnited States Gradual Type Theory Committee Member in Program Committee within the CPP-track
Vilem-Benjamin LiepeltLiepelt, Vilem-Benjamin University of Kent, UKUnited Kingdom [T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning
Yuliya LierlerLierler, Yuliya University of Nebraska Automatic Program Rewriting in Non-Ground Answer Set Programs Strong Equivalence and Program's Structure in Arguing Essential Equivalence
Didier LimeLime, Didier Parametric Timed Broadcast Protocols
Anthony Widjaja LinLin, Anthony Widjaja Oxford UniversityUnited Kingdom CSS Minification via Constraint Solving Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations Committee Member in Program Committee within the VMCAI-track
Sam LindleyLindley, Sam University of Edinburgh, UKUnited Kingdom Exceptional Asynchronous Session Types: Session Types without Tiers
Giuseppe LipariLipari, Giuseppe Static Analysis of Binary Code with Memory Indirections Using Polyhedra
Y. Annie LiuLiu, Y. Annie Stony Brook UniversityUnited States Committee Member in Program Committee within the PEPM-track
Malte LochauLochau, Malte Independence, Concurrency and Abstraction in Graph-Rewriting Processes
Alexander LochmannLochmann, Alexander Certified ACKBO
Nuno P. LopesLopes, Nuno P. Microsoft Research Session Chair of Program Synthesis (part of VMCAI) Semantics for Compiler IRs: Undefined Behavior is not Evil! Fast BGP Simulation of Large Datacenters Invited Speaker in Invited Speakers within the VMCAI-track
Michele LoretiLoreti, Michele University of CamerinoItaly Designing Resilient Large Scaled CPS: Models, Languages and Tools
Kenny Zhuo Ming LuLu, Kenny Zhuo Ming Nanyang Polytechnic, Singapore Control Flow Obfuscation via CPS Transformation
Tianhan LuLu, Tianhan University of Colorado Boulder Type-directed Bounding of Collections in Reactive Programs
Georgy LukyanovLukyanov, Georgy Newcastle University, UKUnited Kingdom Towards a Coq Formalisation of Build Systems
Bas LuttikLuttik, Bas Eindhoven University of Technology Revised Semantics for Sequential Composition in the Presence of Successful Termination (Tentative)
Hugo LópezLópez, Hugo IT University of Copenhagen, Denmark & DCR Solutions A/SColombia Towards Legally Compliant Governmental Case Work with Dynamic Condition Response Graphs
M P. MadhusudanMadhusudan, P. University of Illinois at Urbana-ChampaignUnited States Session Chair of Model Checking (part of POPL Research Papers) Decidable Verification of Uninterpreted Programs Committee Member in Program Committee within the POPL Research Papers-track
Assia MahboubiMahboubi, Assia INRIAFrance Session Chair of Research Papers: Proof Theory, Theory of Programming Languages (part of CPP) Session Chair of Keynote 2 and Research Paper (part of CPP) Business Meeting Program Co-Chair in Program Committee within the CPP-track
Kenji MaillardMaillard, Kenji Inria Paris and ENS Paris Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Geoffrey MainlandMainland, Geoffrey Drexel University, USA Committee Member in Program Committee within the PADL-track
Claire MaizaMaiza, Claire Verimag, France Fast and exact analysis for LRU caches
Rupak MajumdarMajumdar, Rupak MPI-SWS, Germany Committee Member in Steering Committee for POPL 2019
Petar MaksimovićMaksimović, Petar Imperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, SerbiaUnited Kingdom JaVerT 2.0: Compositional Symbolic Execution for JavaScript
Konstantinos MamourasMamouras, Konstantinos University of Pennsylvania Modular Quantitative Monitoring
Stefan MangardMangard, Stefan Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs
Matteo ManighettiManighetti, Matteo Inria & École PolytechniqueFrance A Proof-Theoretic Approach to Certifying Skolemization
Carole MannMann, Carole R.S.L Registration in Organizing Committee for POPL 2019
Vikash K. MansinghkaMansinghka, Vikash K. MIT Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Susannah ManskyMansky, Susannah Dynamic Class Initialization Semantics: a Jinja Extension
William ManskyMansky, William University of Illinois at ChicagoUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Program Committee within the CoqPL-track
Xiaoguang MaoMao, Xiaoguang National University of Defense Technology Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Jean Everson MartinaMartina, Jean Everson UFSC - Universidade Federal de Santa CatarinaBrazil Committee Member in Program Committee within the CPP-track
Francisco MartinsMartins, Francisco LaSIGE, University of Lisbon Hardware Interactions as Behavioural Types
Ruben MartinsMartins, Ruben Carnegie Mellon UniversityPortugal Committee Member in Program Committee within the VMCAI-track
Christoph MathejaMatheja, Christoph RWTH Aachen UniversityGermany Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
Umang MathurMathur, Umang University of Illinois at Urbana-ChampaignUnited States Decidable Verification of Uninterpreted Programs
Kazutaka MatsudaMatsuda, Kazutaka Tohoku University, JapanJapan Committee Member in Program Committee within the PEPM-track
Damiano MazzaMazza, Damiano CNRSFrance Intersection Types and Runtime Errors in the Pi-Calculus
Jay McCarthyMcCarthy, Jay University of Massachusetts Lowell Demand Control-Flow Analysis
James McKinnaMcKinna, James Abstracting Extensible Data Types; Or, Rows By Any Other Name
Hernan MelgrattiMelgratti, Hernan University of Buenos Aires, Argentina Committee Member in Program Committee within the BEAT-track
Paul-André MelliesMellies, Paul-André CNRS and University Paris Diderot Categorical Combinatorics of Scheduling and Synchronization in Game Semantics
Kayvan MemarianMemarian, Kayvan University of CambridgeIran Exploring C Semantics and Pointer Provenance
Roland MeyerMeyer, Roland Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Aart MiddeldorpMiddeldorp, Aart A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Jan MidtgaardMidtgaard, Jan University of Southern DenmarkDenmark Committee Member in Program Committee within the PEPM-track
Matthew MightMight, Matthew University of Alabama at Birmingham \| Harvard Medical SchoolUnited States Relatively Complete Pushdown Analysis of Escape Continuations Demand Control-Flow Analysis
Christina Mika-MichalskiMika-Michalski, Christina University of Duisburg-Essen Fixpoint Games on Continuous Lattices
Dale MillerMiller, Dale INRIA Saclay and LIXFrance A Proof-Theoretic Approach to Certifying Skolemization
Heather MillerMiller, Heather Carnegie Mellon University Committee Member in Program Committee within the POPL Research Papers-track
Todd MillsteinMillstein, Todd University of California, Los Angeles Factorized Exact Inference for Discrete Probabilistic Programs
Victor Cacciari MiraldoMiraldo, Victor Cacciari Utrecht University, Netherlands Classes of Arbitrary Kind
Yusuke MiyazakiMiyazaki, Yusuke Kyoto UniversityJapan Dynamic Type Inference for Gradual Hindley–Milner Typing
Andrey MokhovMokhov, Andrey Newcastle University, UK Towards a Coq Formalisation of Build Systems
David MonniauxMonniaux, David CNRS, VERIMAGFrance Fast and exact analysis for LRU caches
Benoît MontaguMontagu, Benoît Prove & Run Inferring Frame Conditions with Static Correlation Analysis
Fabrizio MontesiMontesi, Fabrizio University of Southern DenmarkDenmark Better Late Than Never: A Fully Abstract Semantics for Classical Processes Committee Member in Program Committee within the BEAT-track
Andreia MordidoMordido, Andreia Lasige / Faculty of Sciences, Universidade de Lisboa Checking the Equivalence of Context-Free Session Types
J. Garrett MorrisMorris, J. Garrett University of Kansas, USAUnited States Abstracting Extensible Data Types; Or, Rows By Any Other Name Exceptional Asynchronous Session Types: Session Types without Tiers
Jean-Marc MotaMota, Jean-Marc Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking
Mohammad MousaviMousavi, Mohammad University of Leicester, UKUnited Kingdom Session Chair of Equational Characterisations, Transactions (part of OPCT) Committee Member in Organizing Committee within the OPCT-track
Prashanth MundkurMundkur, Prashanth SRI International ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Charlie MurphyMurphy, Charlie Princeton UniversityUnited States A Practical Algorithm for Structure Embedding
Toby MurrayMurray, Toby University of Melbourne, AustraliaAustralia Committee Member in Program Committee within the CPP-track
Andrew C. MyersMyers, Andrew C. Cornell UniversityUnited States Committee Member in Steering Committee for POPL 2019 Session Chair of Time (part of POPL Research Papers) Abstraction-Safe Effect Handlers via Tunneling
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology, SwedenSweden Session Chair of Keynote 1 and Research Paper (part of CPP) Business Meeting Program Co-Chair in Program Committee within the CPP-track
Carlos Mão de FerroMão de Ferro, Carlos LASIGE, Faculty of Sciences, University of LisbonPortugal Student Volunteer Co-Captain in Organizing Committee for POPL 2019 Hardware Interactions as Behavioural Types
Rasmus Ejlers MøgelbergMøgelberg, Rasmus Ejlers IT University of CopenhagenDenmark Bisimulation as Path Type for Guarded Recursive Types
N Santosh NagarakatteNagarakatte, Santosh Rutgers University, USAUnited States Committee Member in Program Committee within the PriSC-track
Mayur NaikNaik, Mayur University of Pennsylvania Committee Member in Program Committee within the POPL Research Papers-track
Keiko NakataNakata, Keiko SAP Innovation Center PotsdamGermany Committee Member in Program Committee within the PEPM-track
Kedar NamjoshiNamjoshi, Kedar Bell Labs, Nokia Session Chair of Decision Procedures (part of VMCAI) Security Witnesses for Compiler Transformations Designing Self-Certifying Software Systems Committee Member in Program Committee within the VMCAI-track Invited Speaker in Invited Speakers within the VMCAI-track
Daniele Nantes-SobrinhoNantes-Sobrinho, Daniele University of Brasília, Brazil Relating Process Languages for Security and Communication Correctness
Praveen NarayananNarayanan, Praveen Indiana University, USA Committee Member in Program Committee within the LAFI-track
David NaumannNaumann, David Stevens Institute of Technology Session Chair of Abstract Interpretation (part of POPL Research Papers) Session Chair of Session 4 (part of PriSC) Committee Member in Program Committee within the PriSC-track Committee Member in Program Committee within the POPL Research Papers-track
Hamed NematiNemati, Hamed CISPA Confidentiality-Preserving Refinement
Renato NevesNeves, Renato University of Minho & INESC TEC Hybrid System Iteration
Max NewNew, Max Northeastern University Panel: Grad School and Beyond Gradual Type Theory Panelist in Panelists within the PLMW-track
Ryan R. NewtonNewton, Ryan R. Indiana UniversityUnited States Committee Member in Program Committee within the POPL Research Papers-track
Rumyana NeykovaNeykova, Rumyana Brunel University LondonUnited Kingdom Invited Talk: A Session Type Provider: Compile-time Generation of Session Types with Interaction Refinements
Nicholas NgNg, Nicholas Imperial College LondonUnited Kingdom Distributed Programming using Role-Parametric Session Types in Go
Thanh-Toan NguyenNguyen, Thanh-Toan Automatic Program Repair using Formal Verification and Expression Templates
Van NguyenNguyen, Van Natural Language Generation From Ontologies
Dejan NickovicNickovic, Dejan Austrian Institute of Technology Committee Member in Program Committee within the VMCAI-track
Jens NicolayNicolay, Jens Vrije Universiteit Brussel, BelgiumBelgium Effect-driven Flow Analysis
Thomas NollNoll, Thomas RWTH Aachen University Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
Robert M. NortonNorton, Robert M. University of Cambridge ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
O Liam O'ConnorO'Connor, Liam UNSWAustralia A Data Layout Description Language for Cogent
Peter O'HearnO'Hearn, Peter Facebook Session Chair of Welcome & Keynote I (part of POPL Research Papers) Committee Member in Program Committee within the POPL Research Papers-track
Peter W. O'HearnO'Hearn, Peter W. Facebook and University College London A True Positives Theorem for a Static Race Detector
Emilia OikarinenOikarinen, Emilia University of HelsinkiFinland Committee Member in Program Committee within the PADL-track
Nastaran OkatiOkati, Nastaran Ferdowsi University of Mashhad Efficient Parameterized Algorithms for Data Packing
Cyrus OmarOmar, Cyrus University of ChicagoUnited States Live Functional Programming with Typed Holes
Dominic OrchardOrchard, Dominic University of Kent, UKUnited Kingdom Session Chair of Capabilities and Session Types I (part of POPL Research Papers) Session Chair of Session 2 (part of BEAT) Panel: Grad School and Beyond [T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning Panelist in Panelists within the PLMW-track Committee Member in Program Committee within the POPL Research Papers-track Committee Member in Program Committee within the BEAT-track
Joseph C. OsbornOsborn, Joseph C. Pomona College Teaching Discrete Mathematics to Early Undergraduates with Software Foundations
Hiroki OshikawaOshikawa, Hiroki University of Tokyo, Japan Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking
Scott OwensOwens, Scott University of Kent, UKUnited Kingdom Session Chair of Weak Memory (part of POPL Research Papers) Committee Member in Program Committee within the POPL Research Papers-track
P Munindar P. SinghP. Singh, Munindar North Carolina State University [T2] Engineering Distributed Systems via Protocols and Commitments
Tommaso PadoanPadoan, Tommaso University of Padova Fixpoint Games on Continuous Lattices
Luca PadovaniPadovani, Luca University of Turin, ItalyItaly Committee Member in Program Committee within the BEAT-track
Catuscia PalamidessiPalamidessi, Catuscia INRIA and LIX Research Skills: How to Choose Research Areas Speaker in Speakers within the PLMW-track
Viktor PalmkvistPalmkvist, Viktor KTH Royal Institute of TechnologySweden Composing Syntactical Constructs to Create Domain-Specific Languages
Karl PalmskogPalmskog, Karl University of Texas at AustinUnited States Verifying Finality for Blockchain Systems Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jens PalsbergPalsberg, Jens University of California, Los Angeles (UCLA) Session Chair of Quantum Programming (part of POPL Research Papers) What Is the Type of a Partial Evaluator? (Invited Talk) State of SIGPLAN Committee Member in Program Committee within the PEPM-track Committee Member in Program Committee within the VMCAI-track
Hugo PaquetPaquet, Hugo University of Cambridge Probabilistic Programming Inference via Intensional Semantics
Gyunghee ParkPark, Gyunghee KAIST, Oracle LabsSouth Korea Polymorphic Symmetric Multiple Dispatch with Variance
James ParkerParker, James University of Maryland LWeb: Information Flow Security for Multi-Tier Web Applications
Matthew ParkinsonParkinson, Matthew Microsoft Research, UKUnited Kingdom Committee Member in Program Committee within the POPL Research Papers-track
Bryan ParnoParno, Bryan A Verified, Efficient Embedding of a Verifiable Assembly Language
Marco PatrignaniPatrignani, Marco Saarland University & CISPAUnited States Committee Member in Organizing Committee within the PriSC-track Committee Member in Program Committee within the PriSC-track
Daniel PattersonPatterson, Daniel Northeastern UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Loïc PaulevéPaulevé, Loïc Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics
Lawrence PaulsonPaulson, Lawrence University of CambridgeUnited Kingdom Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem
Andreas PavlogiannisPavlogiannis, Andreas EPFL, Switzerland Efficient Parameterized Algorithms for Data Packing
Mathias PayerPayer, Mathias EPFLSwitzerland Committee Member in Program Committee within the PriSC-track
Jennifer PaykinPaykin, Jennifer Galois, Inc.United States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Barak A. PearlmutterPearlmutter, Barak A. Maynooth UniversityIreland A Nuts-and-Bolts Differential Geometric Perspective on Automatic Differentiation
Mathias Vorreiter PedersenPedersen, Mathias Vorreiter Aarhus University Modular Security Guarantees for Low-Level Languages with Stack Traversal
Dhruva PendharkarPendharkar, Dhruva An ASP-based Approach to Representing and Querying Textual Knowledge
Marco PeressottiPeressotti, Marco University of Southern DenmarkDenmark Better Late Than Never: A Fully Abstract Semantics for Classical Processes
Kirstin PetersPeters, Kirstin TU Berlin Invited Talk: Session Types for Fault-Tolerant Distributed Algorithms Taming Concurrency for Verification using Multiparty Session Types
Gustavo PetriPetri, Gustavo IRIF, Université Paris DiderotFrance Session Chair of Concurrent Programming, Memory Models (part of OPCT)
Tomas PetricekPetricek, Tomas University of KentUnited Kingdom Committee Member in Program Committee within the Off the Beaten Track-track
Ron PetrickPetrick, Ron Proof Carrying Plans
Tommaso PetruccianiPetrucciani, Tommaso DIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, FranceItaly Gradual Typing: A New Perspective
Alberto PettorossiPettorossi, Alberto University of Rome Tor Vergata, Italy Session Chair of Session 5 (part of PEPM) Committee Member in Program Committee within the PEPM-track
Lucas PeñaPeña, Lucas University of Illinois at Urbana-Champaign Verifying Finality for Blockchain Systems
Frank PfenningPfenning, Frank Carnegie Mellon University, USA Technical Talk: How to Think about Types Speaker in Speakers within the PLMW-track Committee Member in Program Committee within the PEPM-track
Anna PhilippouPhilippou, Anna University of Cyprus Behavioral Types as a Semantic Foundation for the GDPR Notion of Purpose Committee Member in Program Committee within the BEAT-track
Robin PiedeleuPiedeleu, Robin University of Oxford Diagrammatic Algebra: From Linear to Concurrent Systems
Brigitte PientkaPientka, Brigitte McGill University Committee Member in Steering Committee for POPL 2019 Mechanized Metatheory - The Next Chapter POPL 2020 Announcement
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server SIGPLAN Climate Committee Report SIGPLAN Awards [T1] QuickChick: Property-Based Testing in Coq
Frank PiessensPiessens, Frank KU Leuven Committee Member in Program Committee within the PriSC-track
Ruben P. PietersPieters, Ruben P. Faster Coroutine Pipelines: A Reconstruction
Anton PirogovPirogov, Anton Flat Model Checking for Counting LTL using Quantifier-free Presburger Arithmetic
Maciej PirógPiróg, Maciej University of WrocławPoland Abstracting Algebraic Effects
Ruzica PiskacPiskac, Ruzica Yale University, USA Session Chair of Invited Talk 3 (part of VMCAI) Co-chair in Organizing Committee within the VMCAI-track Program Co-Chair in Program Committee within the VMCAI-track
André PlatzerPlatzer, André Carnegie Mellon UniversityUnited States [T4] Programming Cyber-Physical Systems with Logic Committee Member in Program Committee within the CPP-track
Andreas PodelskiPodelski, Andreas University of Freiburg, GermanyGermany Committee Member in Program Committee within the POPL Research Papers-track
Anton PodkopaevPodkopaev, Anton Higher School of Economics, JetBrains ResearchRussia Bridging the Gap Between Programming Languages and Hardware Weak Memory Models
Piotr PolesiukPolesiuk, Piotr University of Wrocław Abstracting Algebraic Effects
Nadia PolikarpovaPolikarpova, Nadia University of California, San DiegoUnited States Structuring the Synthesis of Heap-Manipulating Programs
Axel PolleresPolleres, Axel Vienna University of Economincs and Business, Austria Committee Member in Program Committee within the PADL-track
Enrico PontelliPontelli, Enrico Natural Language Generation From Ontologies
Enrico PontelliPontelli, Enrico New Mexico State University Committee Member in Program Committee within the PADL-track
Andrei PopescuPopescu, Andrei Middlesex University, LondonUnited Kingdom Session Chair of Research Papers: Rewriting, Automated Reasoning (part of CPP) Bindings as Bounded Natural Functors Committee Member in Program Committee within the CPP-track
Natalie PopescuPopescu, Natalie University of California San Diego CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Turaga PrathameshPrathamesh, Turaga A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Viorel PreoteasaPreoteasa, Viorel Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
Maurizio ProiettiProietti, Maurizio Making Proofs Easy: Horn Clause Transformations to the Aid of Program Verification (Invited Talk)
Jonathan ProtzenkoProtzenko, Jonathan Microsoft Research, RedmondUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Christopher PultePulte, Christopher University of Cambridge ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Sylvie PutotPutot, Sylvie École Polytechnique Under and Over Approximated Reachability Analysis for the Verifcation of Control Systems Committee Member in Program Committee within the VMCAI-track Invited Speaker in Invited Speakers within the VMCAI-track
Pierre-Marie PédrotPédrot, Pierre-Marie Ltac2: Tactical Warfare
Jorge A. PérezPérez, Jorge A. University of Groningen, The NetherlandsNetherlands Session Chair of Session 4 (part of BEAT) Panel: Grad School and Beyond Relating Process Languages for Security and Communication Correctness Closing Opening Panelist in Panelists within the PLMW-track Co-chair in Program Committee within the BEAT-track Committee Member in Organizing Committee within the BEAT-track
Markus PüschelPüschel, Markus ETH ZürichSwitzerland An Abstract Domain for Certifying Neural Networks
Q Xuanrui QiQi, Xuanrui Tufts University From Tactics to Structure Editors for Proofs
Joe QianQian, Joe University of California, Los Angeles Factorized Exact Inference for Discrete Probabilistic Programs
Xiaokang QiuQiu, Xiaokang Purdue UniversityUnited States Session Chair of Model Checking (part of VMCAI) A Decidable Logic for Tree Data-Structures with Measurements
R Azalea RaadRaad, Azalea MPI-SWS, GermanyUnited Kingdom Panel: Grad School and Beyond On the Semantics of Snapshot Isolation On Library Correctness under Weak Memory Consistency Panelist in Panelists within the PLMW-track
Gabriel RadanneRadanne, Gabriel University of Freiburg, GermanyFrance Typed Parsing and Unparsing for Untyped Regular Expression Engines
Tom RainforthRainforth, Tom Department of Statistics, University of Oxford Committee Member in Program Committee within the LAFI-track
Vineet RajaniRajani, Vineet MPI-SWS From Fine- to Coarse-Grained Dynamic Information Flow Control and Back
Robert RandRand, Robert University of PennsylvaniaUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Francesco RanzatoRanzato, Francesco University of PadovaItaly A^2 I: Abstract^2 Interpretation
Franziska RappRapp, Franziska A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Aseem RastogiRastogi, Aseem Microsoft ResearchIndia A Verified, Efficient Embedding of a Verifiable Assembly Language
Antonio RavaraRavara, Antonio Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCSPortugal Session Chair of Session Types, Graph-Rewriting (part of OPCT) Closing Opening Getting Rid of Null-Dereferences – Behavioural Types to the Rescue Committee Member in Organizing Committee within the OPCT-track Co-chair in Program Committee within the BEAT-track Committee Member in Organizing Committee within the BEAT-track
Binoy RavindranRavindran, Binoy Virginia Tech Formally Verified Big Step Semantics out of x86-64 Binaries
Jakob RehofRehof, Jakob Technical University Dortmund Principality and Approximation under Dimensional Bound
Christoph ReichenbachReichenbach, Christoph Lund University Committee Member in Program Committee within the PEPM-track
Alastair ReidReid, Alastair Arm LtdUnited Kingdom ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Jan ReinekeReineke, Jan Saarland UniversityGermany Fast and exact analysis for LRU caches
Giselle ReisReis, Giselle Carnegie Mellon University Committee Member in Program Committee within the CPP-track
John RennerRenner, John University of California, San Diego CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Thomas RepsReps, Thomas University of Wisconsin - Madison and GrammaTech, Inc.United States Closed Forms for Numerical Loops Refinement of Path Expressions for Static Analysis
Tamara RezkRezk, Tamara InriaFrance Committee Member in Program Committee within the PriSC-track
Alexander RichardsonRichardson, Alexander University of Cambridge Protecting C++ Applications Using CHERI Secure Linking in the CheriBSD Operating System Exploring C Semantics and Pointer Provenance
Martin C. RinardRinard, Martin C. Massachusetts Institute of TechnologyUnited States Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling Committee Member in Program Committee within the PEPM-track
Talia RingerRinger, Talia University of WashingtonUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Program Committee within the CoqPL-track
Christine RizkallahRizkallah, Christine UNSWAustralia A Data Layout Description Language for Cogent Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ricardo RochaRocha, Ricardo University of Porto, PortugalPortugal Committee Member in Program Committee within the PADL-track
Ian RoessleRoessle, Ian Virginia Tech, USA Formally Verified Big Step Semantics out of x86-64 Binaries
Tiark RompfRompf, Tiark Purdue UniversityUnited States Steering Committee Member in Steering Committee within the PEPM-track
Simona Ronchi Della RoccaRonchi Della Rocca, Simona University of TorinoItaly Probabilistic Lambda Calculus: Beyond Deterministic Evaluation
Jurriaan RotRot, Jurriaan Radboud University Nijmegen Coalgebra Learning via Duality
Grigore RoşuRoşu, Grigore University of Illinois at Urbana-ChampaignUnited States Verifying Finality for Blockchain Systems
Lovro RožićRožić, Lovro MPI-SWS, Germany On Library Correctness under Weak Memory Consistency
Philipp RuemmerRuemmer, Philipp Uppsala UniversitySweden Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Jordy RuizRuiz, Jordy Static Analysis of Binary Code with Memory Indirections Using Polyhedra
Alejandro RussoRusso, Alejandro Chalmers University of Technology, SwedenArgentina From Fine- to Coarse-Grained Dynamic Information Flow Control and Back
Claudio RussoRusso, Claudio Microsoft Research Committee Member in Program Committee within the POPL Research Papers-track
Andrey RybalchenkoRybalchenko, Andrey Microsoft ResearchUnited Kingdom Fast BGP Simulation of Large Datacenters
Chris RyderRyder, Chris Application of Abstract Interpretation to the Automotive Electronic Control System
Sukyoung RyuRyu, Sukyoung KAIST, South KoreaKorea, South Polymorphic Symmetric Multiple Dispatch with Variance
S Feras A. SaadSaad, Feras A. Massachusetts Institute of TechnologyUnited States Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Konstantinos (Kostis) SagonasSagonas, Konstantinos (Kostis) Uppsala UniversitySweden Committee Member in Program Committee within the PEPM-track
Karem A. SakallahSakallah, Karem A. euforia: Complete Software Model Checking with Uninterpreted Functions
Gabriela SampaioSampaio, Gabriela Imperial College London, UK JaVerT 2.0: Compositional Symbolic Execution for JavaScript
Alex Sanchez-SternSanchez-Stern, Alex University of California, San DiegoUnited States Student Volunteer Co-Captain in Organizing Committee for POPL 2019
José Fragoso SantosSantos, José Fragoso Imperial College London JaVerT 2.0: Compositional Symbolic Execution for JavaScript
Isao SasanoSasano, Isao Shibaura Institute of TechnologyJapan Committee Member in Program Committee within the PEPM-track
Annabel SatinSatin, Annabel P.C.K. Conference Coordinator in Organizing Committee for POPL 2019 Treasurer in Organizing Committee for POPL 2019
Ryosuke SatoSato, Ryosuke Kyushu University, JapanJapan Combining Higher-Order Model Checking with Refinement Type Inference
Tetsuya SatoSato, Tetsuya University at Buffalo, SUNY, USAUnited States Formal Verification of Higher-Order Probabilistic Programs
Alceste ScalasScalas, Alceste Imperial College LondonUnited Kingdom Effpi: Concurrent Programming with Dependent Behavioural Types Less is More: Multiparty Session Types Revisited
Ulrich SchaechtleSchaechtle, Ulrich Massachusetts Institute of Technology, USA Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Konstantin SchekotihinSchekotihin, Konstantin Committee Member in Program Committee within the PADL-track
Gabriel SchererScherer, Gabriel INRIA SaclayFrance Committee Member in Program Committee within the PriSC-track Committee Member in Program Committee within the POPL Research Papers-track
Robert SchillingSchilling, Robert Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs
Tanja SchindlerSchindler, Tanja University of Freiburg Solving and Interpolating Constant Arrays Based on Weak Equivalences
Anders SchlichtkrullSchlichtkrull, Anders Technical University of Denmark A Verified Prover Based on Ordered Resolution
Alan SchmittSchmitt, Alan Inria Skeletal Semantics and their Interpretations
Tom SchrijversSchrijvers, Tom KU Leuven Faster Coroutine Pipelines: A Reconstruction
Ulrik Pagh SchultzSchultz, Ulrik Pagh University of Southern Denmark Steering Committee Member in Steering Committee within the PEPM-track
Christopher SchwaabSchwaab, Christopher University of St Andrews Proof Carrying Plans
Daniel Schwartz-NarbonneSchwartz-Narbonne, Daniel Amazon, n.n. Committee Member in Program Committee within the VMCAI-track
Steven SchäferSchäfer, Steven Saarland UniversityGermany Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Martina SeidlSeidl, Martina Committee Member in Program Committee within the VMCAI-track
Taro SekiyamaSekiyama, Taro National Institute of InformaticsJapan Dynamic Type Inference for Gradual Hindley–Milner Typing Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Peter SelingerSelinger, Peter Dalhaousie University Committee Member in Program Committee within the POPL Research Papers-track
Eli SenneshSennesh, Eli Northeastern University Model and Inference Combinators for Deep Probabilistic Programming
Ilya SergeySergey, Ilya Yale-NUS College and National University of SingaporeSingapore Session Chair of Separation Logic and Memory Semantics (part of POPL Research Papers) Session Chair of Keynote & Contributed Talks 1 (part of CoqPL) Research Skills: How to Bootstrap a Research Project Towards Mechanising Probabilistic Properties of a Blockchain Distributed Protocol Combinators Structuring the Synthesis of Heap-Manipulating Programs A True Positives Theorem for a Static Race Detector Speaker in Speakers within the PLMW-track Committee Member in Program Committee within the POPL Research Papers-track Committee Member in Program Committee within the PEPM-track Co-chair in Organizing Committee within the CoqPL-track
Alejandro SerranoSerrano, Alejandro Utrecht University, NetherlandsNetherlands Classes of Arbitrary Kind
Peter SewellSewell, Peter University of Cambridge Exploring C Semantics and Pointer Provenance ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Thomas SewellSewell, Thomas UNSW, Australia Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Chung-chieh ShanShan, Chung-chieh Indiana University, USA Research Skills: How to Give a Talk Verified Equational Reasoning on a Little Language of Measures Speaker in Speakers within the PLMW-track Committee Member in Steering Committee within the LAFI-track
Zhong ShaoShao, Zhong Yale UniversityUnited States Session Chair of Research Papers: Formalization of Mathematics and Computer Algebra (part of CPP) An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Kensen ShiShi, Kensen Stanford University FrAngel: Component-Based Synthesis with Control Structures
Sharon ShohamShoham, Sharon Tel Aviv universityIsrael Technical Talk: Verification of Distributed Protocols Using Decidable Logic Speaker in Speakers within the PLMW-track Committee Member in Program Committee within the VMCAI-track
Filip SieczkowskiSieczkowski, Filip University of WrocławPoland Abstracting Algebraic Effects
Jeremy G. SiekSiek, Jeremy G. Indiana University, USAUnited States Gradual Typing: A New Perspective
Mihaela SighireanuSighireanu, Mihaela IRIF, University Paris Diderot and CNRS, France Session Chair of Abstract Interpretation (2) (part of VMCAI) Exploiting Pointer Analysis in Memory Models for Deductive Verification
Alexandra SilvaSilva, Alexandra University College LondonUnited Kingdom Session Chair of Algebra, Coalgebra (part of OPCT) Committee Member in Organizing Committee within the OPCT-track
Gagandeep SinghSingh, Gagandeep United States An Abstract Domain for Certifying Neural Networks
Jeffrey Mark SiskindSiskind, Jeffrey Mark School of Electrical and Computer Engineering, Purdue University Co-chair in Program Committee within the LAFI-track
Lau SkorstengaardSkorstengaard, Lau Aarhus University StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
Anna SlobodovaSlobodova, Anna Committee Member in Program Committee within the CPP-track
Calvin SmithSmith, Calvin University of Wisconsin - MadisonUnited States Program Synthesis with Equivalence Reduction Trace Abstraction Modulo Probability
Gert SmolkaSmolka, Gert Saarland University On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Pawel SobocinskiSobocinski, Pawel University of Southampton Diagrammatic Algebra: From Linear to Concurrent Systems
Tran Cao SonSon, Tran Cao Natural Language Generation From Ontologies
Harald SondergaardSondergaard, Harald Committee Member in Program Committee within the PEPM-track
Romain SoulatSoulat, Romain Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking
Matthieu SozeauSozeau, Matthieu InriaFrance Session with the Coq Development Team Reification of Shallow-Embedded DSLs in Coq with Automated Verification Eliminating Reflection from Type Theory Definitional Proof-Irrelevance without K
Simon SpiesSpies, Simon Saarland UniversityGermany Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Bas SpittersSpitters, Bas Aarhus UniversityDenmark WIP: Formalizing the Concordium Consensus Protocol in Coq
Fausto SpotoSpoto, Fausto U. Verona Committee Member in Program Committee within the PEPM-track
Johannes SpäthSpäth, Johannes Fraunhofer IEMGermany Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems
Meera SridharSridhar, Meera University of North Carolina Charlotte, USA Committee Member in Program Committee within the PADL-track
Daniel StanStan, Daniel Syntactic Partial Order Compression for Probabilistic Reachability
Caleb StanfordStanford, Caleb University of PennsylvaniaUnited States Modular Quantitative Monitoring
Ian StarkStark, Ian The University of EdinburghUnited Kingdom ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Kathrin StarkStark, Kathrin Saarland University, GermanyGermany Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Sam StatonStaton, Sam University of Oxford A Domain Theory for Statistical Probabilistic Programming
Guy L. Steele Jr.Steele Jr., Guy L. Oracle LabsUnited States Polymorphic Symmetric Multiple Dispatch with Variance
Deian StefanStefan, Deian University of California San Diego Trestle: Bridging the Performance and Safety Divide in WebAssembly From Fine- to Coarse-Grained Dynamic Information Flow Control and Back Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem Committee Member in Program Committee within the PriSC-track
Jacob SteinhardtSteinhardt, Jacob Stanford University FrAngel: Component-Based Synthesis with Control Structures
Christian SternagelSternagel, Christian University of Innsbruck, AustriaAustria Certified ACKBO Committee Member in Program Committee within the CPP-track
Gordon StewartStewart, Gordon Ohio UniversityUnited States Committee Member in Program Committee within the CoqPL-track
Quentin StiévenartStiévenart, Quentin Vrije Universiteit Brussel, BelgiumBelgium Effect-driven Flow Analysis
Jan StolarekStolarek, Jan University of Edinburgh, UKUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Aaron StumpStump, Aaron The University of Iowa, USAUnited States Committee Member in Program Committee within the POPL Research Papers-track
Martin SulzmannSulzmann, Martin Karlsruhe University of Applied Sciences, Germany Futures and Promises in Haskell and Scala Advanced Futures and Promises in C++ (poster)
Partha SusarlaSusarla, Partha Data61, CSIRO A Data Layout Description Language for Cogent
Charles SuttonSutton, Charles University of EdinburghUnited Kingdom Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States Session Chair of Gradual Types (part of POPL Research Papers) A Verified, Efficient Embedding of a Verifiable Assembly Language Committee Member in Program Committee within the POPL Research Papers-track
David SwaseySwasey, David MPI-SWSGermany Committee Member in Program Committee within the PriSC-track Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
T Quang-Trung TaTa, Quang-Trung National University of Singapore Automatic Program Repair using Formal Verification and Expression Templates
Lucas M. TabajaraTabajara, Lucas M. Rice University Security Witnesses for Compiler Transformations
Nicolas TabareauTabareau, Nicolas InriaFrance Session Chair of Categories (part of POPL Research Papers)
Nicolas TabareauTabareau, Nicolas Inria Session Chair of Research Papers: Program Verification (part of CPP)
Nicolas TabareauTabareau, Nicolas InriaFrance Eliminating Reflection from Type Theory Definitional Proof-Irrelevance without K Committee Member in Program Committee within the POPL Research Papers-track
Éric TanterTanter, Éric University of Chile & Inria ParisChile Type-Driven Gradual Security with References Gradual Parametricity, Revisited
Paul TarauTarau, Paul University of North TexasUnited States A Combinatorial Testing Framework for Intuitionistic Propositional Theorem Provers Committee Member in Program Committee within the PADL-track
Joseph TassarottiTassarotti, Joseph Carnegie Mellon University A Separation Logic for Concurrent Randomized Programs
Enrico TassiTassi, Enrico INRIAFrance Session Chair of Contributed Talks 2 (part of CoqPL) Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the CoqPL-track
Christine TassonTasson, Christine University Paris Diderot Committee Member in Program Committee within the LAFI-track
Zachary TatlockTatlock, Zachary University of Washington, SeattleUnited States Committee Member in Program Committee within the CPP-track
Peter ThiemannThiemann, Peter University of Freiburg, Germany Committee Member in Steering Committee for POPL 2019 Invited Talk: Gradual Session Types — an Ongoing Journey
Michael ThomasThomas, Michael Independent Researcher Strongly Typed Tracing of Probabilistic Programs (cancelled, alas)
Amin TimanyTimany, Amin imec-Distrinet KU-LeuvenBelgium Committee Member in Program Committee within the PriSC-track Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Simone TiniTini, Simone University of Insubria Weak Bisimulation Metrics in Models with Nondeterminism and Continuous States Space: A Logical Characterization
Sam Tobin-HochstadtTobin-Hochstadt, Sam Indiana UniversityUnited States Committee Member in Program Committee within the POPL Research Papers-track
Andrew TolmachTolmach, Andrew Portland State University Committee Member in Program Committee within the POPL Research Papers-track
David TolpinTolpin, David PUB+Israel Server-side Probabilistic Programming
John TomanToman, John University of Washington, SeattleUnited States Concerto: A Framework for Combined Concrete and Abstract Interpretation
Bernardo ToninhoToninho, Bernardo Imperial College London Interconnectability of Session-Based Logical Processes Organizer in Organizing Committee within the PLMW-track
Matías ToroToro, Matías University of Chile Type-Driven Gradual Security with References Gradual Parametricity, Revisited
Paolo TorriniTorrini, Paolo Reifying and Translating a Monadic Fragment of Gallina
Valentin TouzeauTouzeau, Valentin Univ. Grenoble Alpes Fast and exact analysis for LRU caches
Jesse A. TovTov, Jesse A. Northwestern University, Department of Electrical Engineering and Computer Science A Calculus for Esterel: If can, can. If no can, no can.
Dmitriy TraytelTraytel, Dmitriy ETH ZurichSwitzerland A Verified Prover Based on Ordered Resolution Bindings as Bounded Natural Functors
Stavros TripakisTripakis, Stavros Aalto University and UC Berkeley Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
Ashutosh TrivediTrivedi, Ashutosh Type-directed Bounding of Collections in Reactive Programs
Anton TrunovTrunov, Anton IMDEA Software InstituteSpain Committee Member in Program Committee within the CoqPL-track
Daniel TschudiTschudi, Daniel Aarhus University WIP: Formalizing the Concordium Consensus Protocol in Coq
Takeshi TsukadaTsukada, Takeshi University of Tokyo, Japan Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking
U Irek UlidowskiUlidowski, Irek University of Leicester An Axiomatic Approach to Reversible Computation
Dominique UnruhUnruh, Dominique University of Tartu Quantum Relational Hoare Logic
Caterina UrbanUrban, Caterina INRIA & École Normale SupérieureFrance Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Program Committee within the VMCAI-track
V Viktor VafeiadisVafeiadis, Viktor MPI-SWS, GermanyGreece On the Semantics of Snapshot Isolation Grounding Thin-Air Reads with Event Structures Bridging the Gap Between Programming Languages and Hardware Weak Memory Models On Library Correctness under Weak Memory Consistency
Jan-Willem van de Meentvan de Meent, Jan-Willem Northeastern UniversityUnited States Model and Inference Combinators for Deep Probabilistic Programming
Guy Van den BroeckVan den Broeck, Guy University of California, Los Angeles Factorized Exact Inference for Discrete Probabilistic Programs
Bart van Merriënboervan Merriënboer, Bart Google Brain Committee Member in Program Committee within the LAFI-track
Evangelia VaneziVanezi, Evangelia University of Cyprus Behavioral Types as a Semantic Foundation for the GDPR Notion of Purpose
Vasco VasconcelosVasconcelos, Vasco LASIGE, Faculty of Sciences, University of LisbonPortugal Local Arrangements Chair in Organizing Committee for POPL 2019 Panel: How to Do Good PL Research Checking the Equivalence of Context-Free Session Types Panelist in Panelists within the PLMW-track
Marco VassenaVassena, Marco Chalmers University of TechnologySweden From Fine- to Coarse-Grained Dynamic Information Flow Control and Back
Niki VazouVazou, Niki IMDEA Software Institute Student Research Competition Chair in Organizing Committee for POPL 2019 Session Chair of Type Inference II (part of POPL Research Papers) LWeb: Information Flow Security for Multi-Tier Web Applications SRC Announcement Chair in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the POPL Research Papers-track
Martin VechevVechev, Martin ETH Zürich An Abstract Domain for Certifying Neural Networks
Niccolò VeltriVeltri, Niccolò IT University of Copenhagen Bisimulation as Path Type for Guarded Recursive Types
Freek VerbeekVerbeek, Freek Open University of the Netherlands, The Netherlands Formally Verified Big Step Semantics out of x86-64 Binaries
Jules VillardVillard, Jules Facebook LondonUnited Kingdom [T8] Building Your Own Modular Static Analyser with Infer
Mahesh ViswanathanViswanathan, Mahesh University of Illinois at Urbana-Champaign Decidable Verification of Uninterpreted Programs
Ian VoyseyVoysey, Ian Carnegie Mellon University Live Functional Programming with Typed Holes
Dimitrios VytiniotisVytiniotis, Dimitrios Microsoft Research, Cambridge Committee Member in Program Committee within the POPL Research Papers-track
Matthijs VákárVákár, Matthijs University of Oxford Invited talk: Connecting Probabilistic Programming Theory to Applications in Stan A Domain Theory for Statistical Probabilistic Programming
W Philip WadlerWadler, Philip University of Edinburgh, UKUnited Kingdom Session Chair of Session 1 (part of BEAT) Committee Member in Program Committee within the BEAT-track
David WalkerWalker, David Princeton UniversityUnited States Committee Member in Steering Committee for POPL 2019 Industrial Relations Chair in Organizing Committee for POPL 2019 Session Chair of Security and Information Flow (part of POPL Research Papers)
Bow-Yaw WangWang, Bow-Yaw Committee Member in Program Committee within the CPP-track
Di WangWang, Di Carnegie Mellon UniversityUnited States Type-Guided Worst-Case Input Generation Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Weijing WangWang, Weijing Nankai University, China Method Name Suggestion with Hierarchical Attention Networks
Yanjun WangWang, Yanjun Purdue UniversityUnited States A Decidable Logic for Tree Data-Structures with Measurements
Yuting WangWang, Yuting Yale University An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Mark WassellWassell, Mark University of Cambridge ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Keiichi WatanabeWatanabe, Keiichi University of Tokyo, Japan Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking
Robert N. M. WatsonWatson, Robert N. M. University of Cambridge Protecting C++ Applications Using CHERI Secure Linking in the CheriBSD Operating System Exploring C Semantics and Pointer Provenance
Conrad WattWatt, Conrad University of Cambridge Trestle: Bridging the Performance and Safety Divide in WebAssembly CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Tjark WeberWeber, Tjark Uppsala UniversitySweden Committee Member in Program Committee within the CPP-track
Stephanie WeirichWeirich, Stephanie University of Pennsylvania, USAUnited States Committee Member in Steering Committee for POPL 2019 Program Chair in Organizing Committee for POPL 2019 Session Chair of SRC Announcement & Keynote II (part of POPL Research Papers) PC Chair Report Welcome PC Chair in Program Committee within the POPL Research Papers-track
Joe WellsWells, Joe Proof Carrying Plans
Edwin WestbrookWestbrook, Edwin Galois, Inc.United States Committee Member in Program Committee within the CoqPL-track
Pierre WilkeWilke, Pierre Yale University An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Glynn WinskelWinskel, Glynn Game Semantics for Quantum Programming
Kirsten WinterWinter, Kirsten The University of Queensland Linearizability in the Context of Weak Memory Models
Theo WinterhalterWinterhalter, Theo Gallinette / Inria / LS2NFrance Eliminating Reflection from Type Theory
Sebastian WolffWolff, Sebastian TU BraunschweigGermany Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Hao WuWu, Hao Northeastern University Model and Inference Combinators for Deep Probabilistic Programming
Xiaodi WuWu, Xiaodi University of Oregon, USAUnited States Quantitative Robustness Analysis of Quantum Programs
Zhilin WuWu, Zhilin State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
X Li-yao XiaXia, Li-yao University of Pennsylvania From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Jing XuXu, Jing Nankai University, China Method Name Suggestion with Hierarchical Attention Networks
Sihan XuXu, Sihan Nankai University, China Method Name Suggestion with Hierarchical Attention Networks
Y Eran YahavYahav, Eran TechnionIsrael code2vec: Learning Distributed Representations of Code
Boris YakobowskiYakobowski, Boris CEA - LISTFrance Exploiting Pointer Analysis in Memory Models for Deductive Verification
Jeremy YallopYallop, Jeremy University of Cambridge, UK Generating Mutually Recursive Definitions Steering Committee Chair in Steering Committee within the PEPM-track
Tomoya YamaguchiYamaguchi, Tomoya Application of Abstract Interpretation to the Automotive Electronic Control System
Qianchuan YeYe, Qianchuan Purdue University A Verified Protocol Buffer Compiler
Xin YiYi, Xin National University of Defense TechnologyChina Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Mingsheng YingYing, Mingsheng University of Technology SydneyAustralia Quantitative Robustness Analysis of Quantum Programs
Nobuko YoshidaYoshida, Nobuko Imperial College London Effpi: Concurrent Programming with Dependent Behavioural Types Interconnectability of Session-Based Logical Processes Two sides of the same coin: Session Types and Game Semantics Distributed Programming using Role-Parametric Session Types in Go Less is More: Multiparty Session Types Revisited Organizer in Organizing Committee within the PLMW-track
Akira YoshimizuYoshimizu, Akira INRIA Intersection Types and Runtime Errors in the Pi-Calculus
Shu-Hung YouYou, Shu-Hung Northwestern University, USATaiwan A Calculus for Esterel: If can, can. If no can, no can.
Z Jakub ZalewskiZalewski, Jakub Video Chair in Organizing Committee for POPL 2019
Vadim ZalivaZaliva, Vadim Carnegie Mellon University, USAUnited States Reification of Shallow-Embedded DSLs in Coq with Automated Verification
Fabio ZanasiZanasi, Fabio University College London Diagrammatic Algebra: From Linear to Concurrent Systems
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server Organizer in Organizing Committee within the PLMW-track Committee Member in Program Committee within the CoqPL-track
Noam ZeilbergerZeilberger, Noam University of Birmingham, UK Session Chair of Semantics (part of POPL Research Papers) Committee Member in Program Committee within the POPL Research Papers-track
Bohua ZhanZhan, Bohua Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
Sen ZhangZhang, Sen Nankai University, China Method Name Suggestion with Hierarchical Attention Networks
Yizhou ZhangZhang, Yizhou Cornell University Abstraction-Safe Effect Handlers via Tunneling
He ZhuZhu, He Rutgers University, USA Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Shaopeng ZhuZhu, Shaopeng University of Maryland Quantitative Robustness Analysis of Quantum Programs
Lukasz ZiarekZiarek, Lukasz SUNY Buffalo, USAUnited States Committee Member in Program Committee within the PADL-track
Meital ZilbersteinZilberstein, Meital TechnionIsrael code2vec: Learning Distributed Representations of Code
Elena ZuccaZucca, Elena University of Genova Committee Member in Program Committee within the PEPM-track
Lenore ZuckZuck, Lenore Session Chair of Invited Talk 2 (part of VMCAI) Committee Member in Program Committee within the VMCAI-track
Damien ZuffereyZufferey, Damien MPI-SWS Committee Member in Program Committee within the VMCAI-track
Ç Ezgi ÇiçekÇiçek, Ezgi Facebook London [T8] Building Your Own Modular Static Analyser with Infer
Ś Adam ŚcibiorŚcibior, Adam University of Cambridge and MPI Tuebingen Strongly Typed Tracing of Probabilistic Programs (cancelled, alas) Model and Inference Combinators for Deep Probabilistic Programming