POPL 2020 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (848)

A Rodin AarssenAarssen, Rodin CWI, NetherlandsNetherlands High-Fidelity Metaprogramming with Separator Syntax Trees
Martín AbadiAbadi, Martín Google A Simple Differentiable Programming Language
Carmine AbateAbate, Carmine Inria Paris Trace-Relating Compiler Correctness and Secure Compilation
Parosh Aziz AbdullaAbdulla, Parosh Aziz Uppsala University, SwedenSweden Parameterized Verification under TSO is PSPACE-Complete
Andreas AbelAbel, Andreas Gothenburg UniversitySweden Committee Member in Program Committee within the PEPM-track
Umut A. AcarAcar, Umut A. Carnegie Mellon University Disentanglement in Nested-Parallel Programs
Amal AhmedAhmed, Amal Northeastern University, USAUnited States Session Chair of Gradual Criteria (part of WGT) Foreign Function Typing: Semantic Type Soundness for FFIs Graduality and Parametricity: Together Again for the First Time Committee Member in Organizers within the POPL W@POPL Dinner-track Committee Member in Program Committee within the WGT-track
Benedikt AhrensAhrens, Benedikt University of Birmingham, United Kingdom Reduction Monads and Their Signatures
Murad AkhundovAkhundov, Murad University of Toronto Expediting Verification of Assertions in Loops by Isolation
Jonathan AldrichAldrich, Jonathan Carnegie Mellon UniversityUnited States Gradual Program Analysis Gradual Verification of Recursive Heap Data Structures Decidable Subtyping for Path Dependent Types
Thomas AlexanderAlexander, Thomas IBM T.J. Watson Research Center, New York, USA Tuning up entanglement through the cloud using Qiskit-OpenPulse
Guillaume AllaisAllais, Guillaume University of StrathclydeUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Program Committee within the PEPM-track
Deyaaeldeen AlmahallawiAlmahallawi, Deyaaeldeen Indiana UniversityUnited States Space-Efficient Monotonic References
Uri AlonAlon, Uri TechnionIsrael Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Johannes AltmanningerAltmanninger, Johannes TU Wien Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs
Rajeev AlurAlur, Rajeev University of PennsylvaniaUnited States Model Checking for Safe Autonomy Invited Speaker in Invited Speakers within the VMCAI-track
Peter AmidonAmidon, Peter University of California, San Diego A Spectrum of Safety for Foreign Function Interfaces
Nada AminAmin, Nada Harvard UniversityUnited States Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the PEPM-track
Matthew AmyAmy, Matthew Committee Member in Program Committee within the PLanQC-track
Shengwei AnAn, Shengwei Purdue University Augmented Example-based Synthesis using Relational Perturbation Properties
Leif AndersenAndersen, Leif Northeastern University, USA Video Chair in Organizing Committee for POPL 2020
Sean AndersonAnderson, Sean Portland State University Flexible Tag-based Policies for Compartmentalized C
Pablo Andres-MartinezAndres-Martinez, Pablo University of EdinburghUnited Kingdom Automated distribution of quantum circuits via hypergraph partitioning
Danil AnnenkovAnnenkov, Danil Concordium Blockchain Research Center, Aarhus UniversityDenmark ConCert: A Smart Contract Certification Framework in Coq
Timos AntonopoulosAntonopoulos, Timos Yale UniversityUnited States PC Member in Program Committee within the VMCAI-track
Andrew W. AppelAppel, Andrew W. Princeton Session Chair of Verified & Secure Compilation (part of POPL Research Papers) Committee Member in Program Committee within the POPL Research Papers-track
Jesús AransayAransay, Jesús Universidad de la Rioja, Spain Committee Member in Program Committee within the CPP-track
Molham ArefAref, Molham Relational.ai Invited Talk: Relational Artificial Intelligence Panel: Experience and Direction
Michael ArntzeniusArntzenius, Michael University of Birmingham, UK Seminaïve Evaluation for a Higher-Order Functional Language
Federico AschieriAschieri, Federico TU Wien Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
Aslan AskarovAskarov, Aslan Aarhus University Reconciling progress-insensitive noninterference and declassification Committee Member in Program Committee within the PriSC-track
David AspinallAspinall, David University of Edinburgh Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL
Mohamed Faouzi AtigAtig, Mohamed Faouzi Uppsala University, SwedenSweden Parameterized Verification under TSO is PSPACE-Complete
Mauricio Ayala-RinconAyala-Rincon, Mauricio University of BrasíliaBrazil Committee Member in Program Committee within the CPP-track
Sharon AyaldeAyalde, Sharon Facebook Committee Member in Organizers within the POPL W@POPL Dinner-track
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Carnegie Mellon University, USAUnited States Session Chair of Semantics & Type Theory (part of POPL Research Papers) Session Chair of Probabilistic Reasoning and Verification (part of POPL Research Papers) Deriving Instances with Dependent Types Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the POPL Research Papers-track
B Casper Bach PoulsenBach Poulsen, Casper Delft University of Technology Session Chair of Keynote Talk 2 (part of PEPM) Session Chair of Opening & Keynote Talk 1 (part of PEPM) Opening Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages Co-chair in PC Chairs within the PEPM-track Co-chair in Program Committee within the PEPM-track
Johannes BaderBader, Johannes FacebookUnited States Gradual Program Analysis Gradual Verification of Recursive Heap Data Structures
Alexander BagnallBagnall, Alexander Ohio University Coinductive Trees for Exact Inference of Probabilistic Programs
Patrick BahrBahr, Patrick IT University of CopenhagenDenmark Committee Member in Program Committee within the PEPM-track
Alexander BakstBakst, Alexander Galois, Inc Exploits as Insecure Compilation
Michael BallantyneBallantyne, Michael PLT @ Northeastern UniversityUnited States Dependent Type Systems as Macros
Stephanie BalzerBalzer, Stephanie Carnegie Mellon University, USAUnited States Session Chair of Morning 1 (part of PLMW) Committee Member in Organizers within the POPL W@POPL Dinner-track Committee Member in Organizing Committee within the POPL Mentoring Breakfasts-track Organizer in Organizing Committee within the PLMW-track
Anindya BanerjeeBanerjee, Anindya IMDEA Software Institute Coinductive Trees for Exact Inference of Probabilistic Programs
Subarno BanerjeeBanerjee, Subarno University of MichiganUnited States Safe Provenance Based Garbage Collection for C
Suguman BansalBansal, Suguman Rice University, USAUnited States Synthesis of Coordination Programs from Linear Temporal Specifications
Jialu BaoBao, Jialu University of Wisconsin - Madison A logic for verifying conditional independence
Davide BarbarossaBarbarossa, Davide Université Paris 13 Taylor Subsumes Scott, Berry, Kahn and Plotkin
Sébastien BardinBardin, Sébastien CEA LISTFrance Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control Qbricks: formal verification in quantum computing
Aurèle BarrièreBarrière, Aurèle Univ Rennes, IRISA Towards Formally Verified Just-in-Time compilation
Gilles BartheBarthe, Gilles MPI for Security and Privacy (MPI-SP) and IMDEA Software InstituteGermany Formal Verification of a Constant-Time Preserving C Compiler A Probabilistic Separation Logic Relational Proofs for Quantum Programs
Osbert BastaniBastani, Osbert University of PennsylvaniaUnited States Committee Member in Program Committee within the POPL Research Papers-track
Kinjal BasuBasu, Kinjal AQuA: ASP-based Visual Question Answering Panel: Programming with logic for the masses
Andrej BauerBauer, Andrej University of LjubljanaSlovenia Committee Member in Program Committee within the POPL Research Papers-track
Johan BayBay, Johan Aarhus University Reconciling progress-insensitive noninterference and declassification
Ryan BeckettBeckett, Ryan Microsoft Research Abstract Interpretation of Distributed Network Control Planes
Jesper BengtsonBengtson, Jesper IT University of Copenhagen Actris: Session-Type Based Reasoning in Separation Logic
Nick BentonBenton, Nick Facebook LondonUnited Kingdom Committee Member in Program Committee within the WGT-track
Josh BerdineBerdine, Josh Facebook SLEdge: Bounded Model Checking in Separation Logic Committee Member in Program Committee within the ADSL-track
Yves BertotBertot, Yves INRIAFrance Session Chair of Invited Talk (part of CoqPL) Session Chair of Proof engineering and user interaction (part of CPP) The use of Coq for Common Criteria Evaluations
Frédéric BessonBesson, Frédéric Committee Member in Program Committee within the PriSC-track
Dirk BeyerBeyer, Dirk LMU MunichGermany Session Chair of Papers 3 (part of VMCAI) Session Chair of Invited 1 (part of VMCAI) Session Chair of Panel Session (part of VMCAI) Panel "The Future of Software Verification" at VMCAI PC Chair in Program Committee within the VMCAI-track PC Chair in Organizing Committee within the VMCAI-track
Karthikeyan BhargavanBhargavan, Karthikeyan Inria, France Committee Member in Organizing Committee within the HASE-track
Aggelos BiboudisBiboudis, Aggelos EPFL, SwitzerlandSwitzerland Committee Member in Program Committee within the PEPM-track
Dariusz BiernackiBiernacki, Dariusz University of Wrocław Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers
David BinderBinder, David University of Tübingen Decomposition Diversity with Symmetric Data and Codata
Lars BirkedalBirkedal, Lars Aarhus University Program Chair in Organizing Committee for POPL 2020 Session Chair of Automatic Differentiation / Kleene Algebra (part of POPL Research Papers) Session Chair of Welcome + SIGPLAN Award Ceremony (part of POPL Research Papers) Session Chair of Invited Talk (part of POPL Research Papers) Mechanized Reasoning about a Capability Machine PC Chair in Program Committee within the POPL Research Papers-track
Aleš BizjakBizjak, Aleš Aarhus UniversityDenmark Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Nikolaj BjørnerBjørner, Nikolaj Microsoft ResearchUnited States Session Chair of Papers 5 (part of VMCAI) Solving LIA* Using Approximations Invited Talk: Logical Engines for Cloud Configurations Panel: Programming with logic for the masses PC Member in Program Committee within the VMCAI-track
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands Session Chair of Invited talk (part of CPP) PC Chairs' report Program Co-Chair in Program Committee within the CPP-track
Eduardo BlancoBlanco, Eduardo Interactive Text Graph Mining with a Prolog-based Dialog Engine Panel: Programming with logic for the masses
Roberto BlancoBlanco, Roberto Inria Trace-Relating Compiler Correctness and Secure Compilation
Austin J. BlattBlatt, Austin J. Puppet Labs Executable Formal Semantics for the POSIX Shell
Clément BlaudeauBlaudeau, Clément Ecole PolytechniqueFrance A Verified Packrat Parser Interpreter for Parsing Expression Grammars
Sandrine BlazyBlazy, Sandrine Univ Rennes- IRISAFrance Session Chair of Verification in Proof Assistants (part of POPL Research Papers) Towards Formally Verified Just-in-Time compilation A CompCert Compiler that Preserves Cryptographic Constant-time Formal Verification of a Constant-Time Preserving C Compiler Committee Member in Program Committee within the POPL Research Papers-track Committee Member in Program Committee within the PriSC-track
Martin BlichaBlicha, Martin Università della Svizzera italianaSwitzerland A Cooperative Parallelization Approach for Property-Directed k-Induction
François BobotBobot, François CEA Qbricks: formal verification in quantum computing
Rastislav BodíkBodík, Rastislav University of WashingtonUnited States Visualization by Example Committee Member in Program Committee within the POPL Research Papers-track
Filippo BonchiBonchi, Filippo University of Pisa Committee Member in Program Committee within the POPL Research Papers-track
James BornholtBornholt, James University of Texas at AustinUnited States Fixing Code That Explodes Under Symbolic Evaluation
Jay BosamiyaBosamiya, Jay Carnegie Mellon University WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
Ahmed BouajjaniBouajjani, Ahmed IRIF, Université Paris DiderotFrance Formalizing and Checking Multilevel Consistency
Simon BoulierBoulier, Simon Inria Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
Timothy BourkeBourke, Timothy Inria / École normale supérieure Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
William J. BowmanBowman, William J. University of British ColumbiaCanada Panel Dependent Type Systems as Macros Panelist in Panelists within the PLMW-track
Alex BrikBrik, Alex Session Chair of Answer Set Programming Applications and Competitive programming experience (part of PADL) Diagnosing Data Pipeline Failures Using Action Languages: A Progress Report Panel: Programming with logic for the masses
Martin BrombergerBromberger, Martin MPI-INFGermany Committee Member in Artifact-Evaluation Committee within the VMCAI-track
James BrotherstonBrotherston, James Committee Member in Program Committee within the ADSL-track
Chad BrownBrown, Chad Czech Technical University in Prague Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Christopher BrownBrown, Christopher University of St. Andrews, UKUnited Kingdom Committee Member in Program Committee within the PADL-track
Lelio BrunBrun, Lelio ENS/InriaFrance Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
Aloïs BrunelBrunel, Aloïs DeepomaticFrance Backpropagation in the Simply Typed Lambda-calculus with Linear Negation Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Roberto BruniBruni, Roberto University of PisaItaly Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Maurice BruynoogheBruynooghe, Maurice Katholieke Universiteit LeuvenBelgium Improving Parity Game Solvers with Justifications
Ahto BuldasBuldas, Ahto Tallinn University of Technology Verified Security of BLT Signature Scheme
Matteo BusiBusi, Matteo Università di Pisa - Dipartimento di Informatica Securing Interruptible Enclaves
David ButlerButler, David Alan Turing Institute Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL
Kevin BuzzardBuzzard, Kevin Imperial College London Formalising perfectoid spaces
William E. ByrdByrd, William E. University of Alabama at Birmingham, USAUnited States Committee Member in Program Committee within the PADL-track
C Anthony CaninoCanino, Anthony [T1] Building Program Reasoning Tools using LLVM and Z3
Michael CarbinCarbin, Michael Massachusetts Institute of TechnologyUnited States MetaPPL: Inference Algorithms as First-Class Generative Models Gen and MetaGen Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages
Jacques CaretteCarette, Jacques McMaster UniversityCanada GOOL: A Generic Object-Oriented Language
Luís CarvalhoCarvalho, Luís Fac. Ciências e Tecnologias, Universidade Nova de Lisboa Software Evolution with a Typeful Version Control System
Giuseppe CastagnaCastagna, Giuseppe CNRS - Université de Paris, FranceFrance Session Chair of Programming features (part of WGT) Organizer in Organizing Committee within the WGT-track Co-chair in Program Committee within the WGT-track
Pavol CernyCerny, Pavol University of Colorado BoulderSlovakia PC Member in Program Committee within the VMCAI-track
Tej ChajedChajed, Tej Massachusetts Institute of Technology, USAUnited States Verifying concurrent Go code in Coq with Goose Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Sheung Chi ChanChan, Sheung Chi Flexible Graph Matching and Graph Edit Distance Using Answer Set Programming
Bor-Yuh Evan ChangChang, Bor-Yuh Evan University of Colorado Boulder \| Amazon Committee Member in Program Committee within the POPL Research Papers-track
Stephen ChangChang, Stephen Northeastern University Dependent Type Systems as Macros
James ChapmanChapman, James IOHK Committee Member in Program Committee within the PADL-track
Christopĥe CharetonChareton, Christopĥe CEA, LIST, France Qbricks: formal verification in quantum computing
Arthur CharguéraudCharguéraud, Arthur InriaFrance Committee Member in Program Committee within the POPL Research Papers-track
Krishnendu ChatterjeeChatterjee, Krishnendu IST Austria Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
Sudipta ChattopadhyayChattopadhyay, Sudipta Singapore University of Technology and DesignSingapore Systematic Classification of Attackers via Bounded Model Checking
Marsha ChechikChechik, Marsha University of TorontoCanada Panel: Reasoning for machine learning at large Variability-aware Datalog
Dong ChenChen, Dong Department of Computing Science, College of Computer, National University of Defense Technology, Changsha, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Xiaohong ChenChen, Xiaohong University of Illinois at Urbana-ChampaignUnited States Invited talk: Matching Logic: The Foundation of the K Framework
James CheneyCheney, James University of Edinburgh, UKUnited States Session Chair of Small Languages and Implementation (part of PADL) Flexible Graph Matching and Graph Edit Distance Using Answer Set Programming
Fucheng ChengCheng, Fucheng Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Alvin CheungCheung, Alvin University of California, Berkeley Visualization by Example
Marc ChevalierChevalier, Marc ENS, CNRS, PSL University, INRIAFrance Sharing Ghost Variables in a Collection of Abstract Domains
CHR ChhakChhak, CHR Portland State University Flexible Tag-based Policies for Compartmentalized C
David ChisnallChisnall, David University of Cambridge Committee Member in Program Committee within the PriSC-track
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Session Chair of Verified cryptography (part of CPP) Invited talk: Proof Assistants at the Hardware-Software Interface
Minki ChoCho, Minki Seoul National University CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
Frederic T. ChongChong, Frederic T. University of ChicagoUnited States Invited Talk: Resource-Efficient Quantum Computing by Breaking Abstractions
Stephen ChongChong, Stephen Harvard UniversityUnited States Committee Member in Program Committee within the PriSC-track
Benjamin ChungChung, Benjamin Northeastern University Video Chair in Organizing Committee for POPL 2020
Cristina CifuentesCifuentes, Cristina Oracle LabsAustralia Session Chair of New outlooks on secure compilation (part of PriSC) What is a Secure Programming Language? Committee Member in Program Committee within the PriSC-track
Matteo CiminiCimini, Matteo University of Massachusetts LowellUnited States Committee Member in Program Committee within the POPL Research Papers-track
Stefan CiobacaCiobaca, Stefan Alexandru Ioan Cuza University of Iasi Trace-Relating Compiler Correctness and Secure Compilation
Pierre ClairambaultClairambault, Pierre CNRS & ENS LyonFrance Full Abstraction for the Quantum Lambda-Calculus
Martin ClochardClochard, Martin ETH Zürich Deductive Verification with Ghost Monitors
Jesper CockxCockx, Jesper TU DelftNetherlands Committee Member in Program Committee within the POPL Research Papers-track
Liron CohenCohen, Liron Ben-Gurion University of the NegevIsrael Committee Member in Program Committee within the CPP-track
Johan CommelinCommelin, Johan Universität Freiburg Formalising perfectoid spaces
Tino CortesiCortesi, Tino Steering Committee Member in Steering Committee within the VMCAI-track
David CostanzoCostanzo, David Yale University Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Nathanaël CourantCourant, Nathanaël INRIAFrance The Correctness of a Code Generator for a Functional Language
Patrick CousotCousot, Patrick Steering Committee Member in Steering Committee within the VMCAI-track
Andrew CrossCross, Andrew IBM Research Committee Member in Program Committee within the PLanQC-track
Marco Cusumano-TownerCusumano-Towner, Marco MIT-CSAIL MetaPPL: Inference Algorithms as First-Class Generative Models Gen and MetaGen Monte Carlo Semantic Differencing of Probabilistic Programs Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages
D Pedro da Costa Abreu Juniorda Costa Abreu Junior, Pedro Purdue University Shrinking Coq's Trusted Code Base by Transpiling to a Minimal Type Theory
Maryam DabaghchianDabaghchian, Maryam University of Utah Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Fredrik DahlqvistDahlqvist, Fredrik University College London Semantics of Higher-Order Probabilistic Programs with Conditioning
Ugo Dal LagoDal Lago, Ugo University of Bologna, Italy / Inria, FranceItaly Committee Member in Program Committee within the POPL Research Papers-track
Hoang-Hai DangDang, Hoang-Hai MPI-SWS RustBelt Meets Relaxed Memory Stacked Borrows: An Aliasing Model for Rust
Tommy DangDang, Tommy Texas Tech University VRASP: A Virtual Reality Environment for Learning Answer Set Programming Panel: Programming with logic for the masses
Norman DannerDanner, Norman Wesleyan University Recurrence Extraction for Functional Programs through Call-by-Push-Value
Olivier DanvyDanvy, Olivier Yale-NUS College, SingaporeSingapore Committee Member in Program Committee within the PEPM-track
David DaraisDarais, David University of VermontUnited States A Language for Probabilistically Oblivious Computation
Adnan DarwicheDarwiche, Adnan UCLA Invited Talk: Symbolic Reasoning About Machine Learning Systems Panel: Reasoning for machine learning at large
Swaraj DashDash, Swaraj University of Oxford A Monad for Point Processes
Sarah de Haasde Haas, Sarah Google Research Peer Skillshare Organizer in Organizing Committee within the HASE-track
Paulo Emílio de Vilhenade Vilhena, Paulo Emílio InriaFrance Spy Game: Verifying a Local Generic Solver in Iris
Marc De VismeDe Visme, Marc ENS Lyon Full Abstraction for the Quantum Lambda-Calculus
Pierpaolo DeganoDegano, Pierpaolo Università di Pisa - Dipartimento di Informatica Securing Interruptible Enclaves
Benjamin DelawareDelaware, Benjamin Purdue University Artifact Evaluation Co-Chair in Organizing Committee for POPL 2020 Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Delphine DemangeDemange, Delphine Univ Rennes, Inria, CNRS, IRISA Committee Member in Program Committee within the CoqPL-track
Stephane DemriDemri, Stephane CNRS, LSV, ENS Paris-Saclay Committee Member in Program Committee within the ADSL-track
Marc DeneckerDenecker, Marc Katholieke Universiteit LeuvenBelgium Improving Parity Game Solvers with Justifications
Haowei DengDeng, Haowei University of Science and Technology of China Context-Sensitive and Duration-Aware Qubit Mapping for Various NISQ Devices
Mingtang DengDeng, Mingtang Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Xi DengDeng, Xi Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Yuxin DengDeng, Yuxin East China Normal University Quingo: A Domain Specific Language for Quantum Computing with NISQ Features Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
Dominique DevrieseDevriese, Dominique Vrije Universiteit BrusselBelgium Session Chair of Type Systems (part of POPL Research Papers) Session Chair of Types and Effects (part of POPL Research Papers) Fully Abstract from Static to Gradual PriSC Introduction Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the POPL Research Papers-track Program Co-Chair in Program Committee within the PriSC-track Committee Member in Steering Committee within the PriSC-track
Iavor DiatchkiDiatchki, Iavor Galois, Inc. Committee Member in Program Committee within the PADL-track
Simon DierlDierl, Simon Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Daniel DietschDietsch, Daniel University of FreiburgGermany Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Artifact Evaluation Chair in Artifact-Evaluation Committee within the VMCAI-track Artifact Evaluation Chair in Organizing Committee within the VMCAI-track
Işil DilligDillig, Işil University of Texas AustinUnited States Automated Program Verification using Abductive Reasoning Visualization by Example Invited Speaker in Invited speakers within the PLMW-track
Rayna DimitrovaDimitrova, Rayna University of Leicester, UK Committee Member in Artifact-Evaluation Committee within the VMCAI-track PC Member in Program Committee within the VMCAI-track
Christos DimoulasDimoulas, Christos PLT @ Northwestern UniversityUnited States Does Blame Shifting Work?
Elizabeth DinellaDinella, Elizabeth University of Pennsylvania [T1] Building Program Reasoning Tools using LLVM and Z3
Christian DoczkalDoczkal, Christian Université Côte d'Azur Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
Alastair F. DonaldsonDonaldson, Alastair F. Imperial College LondonUnited Kingdom Committee Member in Program Committee within the POPL Research Papers-track
Derek DreyerDreyer, Derek MPI-SWSGermany How to Write Papers So People Can Read Them RustBelt Meets Relaxed Memory The High-Level Benefits of Low-Level Sandboxing Stacked Borrows: An Aliasing Model for Rust The Future is Ours: Prophecy Variables in Separation Logic [T4] Proving Semantic Type Soundness in Iris Invited Speaker in Invited speakers within the PLMW-track
Cezara DrăgoiDrăgoi, Cezara INRIA, ENS, CNRSFrance Committee Member in Program Committee within the POPL Research Papers-track
Andrej DudenhefnerDudenhefner, Andrej Saarland University A Coq Library of Undecidable Problems
Stefania DumbravaDumbrava, Stefania ENSIIE Paris-ÉvryFrance Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Eugene DumitrescuDumitrescu, Eugene Oak Ridge National Laboratory Extending Modern C++ for Heterogeneous Quantum-Classical Computing
Ross DuncanDuncan, Ross Cambridge Quantum Computing Committee Member in Program Committee within the PLanQC-track
Sandra DylusDylus, Sandra University of Kiel, GermanyGermany Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Maxime DénèsDénès, Maxime Inria The use of Coq for Common Criteria Evaluations Session with the Coq Development Team
Tomás DíazDíaz, Tomás IMFD Chile A Mechanized Formalization of GraphQL
Alejandro Díaz-CaroDíaz-Caro, Alejandro ICC (UBA-CONICET) & UNQArgentina Runtime Analysis of Quantum Programs: A Formal Approach
E Gabriel EbnerEbner, Gabriel Vrije Universiteit AmsterdamNetherlands Committee Member in Program Committee within the PADL-track
Mnacho EchenimEchenim, Mnacho The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions
Daniel EggerEgger, Daniel IBM Research, Zurich, Switzerland Tuning up entanglement through the cloud using Qiskit-OpenPulse
Gabriel EisemanEiseman, Gabriel Georgia Institute of Technology Rewriting Pure Multiply-Recursive Functions
Richard A. EisenbergEisenberg, Richard A. Bryn Mawr College, USAUnited States Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc Kind Inference for Datatypes
Martin ElsmanElsman, Martin University of Copenhagen, DenmarkDenmark On the Effects of Integrating Region-based Memory Managemen and Generational Garbage Collection in ML Panel: Memory and real-time programming in practice
Constantin EneaEnea, Constantin IRIF, University Paris Diderot & CNRSFrance Formalizing and Checking Multilevel Consistency PC Member in Program Committee within the VMCAI-track
Esra ErdemErdem, Esra Sabanci University, Turkey Committee Member in Program Committee within the PADL-track
Sebastian ErdwegErdweg, Sebastian JGU MainzGermany A Systematic Approach to Abstract Interpretation of Program Transformations
Johannes ErikssonEriksson, Johannes A DSL for Integer Range Reasoning: Partition, Interval and Mapping Diagrams Panel: Reasoning for machine learning at large
Erik ErnstErnst, Erik Google Inc.Denmark Committee Member in Program Committee within the WGT-track
Martin ErwigErwig, Martin Oregon State UniversityUnited States Explanations for Dynamic Programming Panel: Reasoning for machine learning at large
Samuel EstepEstep, Samuel Liberty University Gradual Program Analysis
F Azadeh FarzanFarzan, Azadeh University of TorontoCanada Reductions for Safety Proofs
Grigory FedyukovichFedyukovich, Grigory Florida State UniversityUnited States Synthesizing Environment Invariants for Modular Hardware Verification
Yotam M. Y. FeldmanFeldman, Yotam M. Y. Tel Aviv UniversityIsrael Complexity and Information in Invariant Inference
Andreas FellnerFellner, Andreas AIT - Austrian Institute of TechnologyAustria Language Inclusion for Finite Prime Event Structures
Xinyu FengFeng, Xinyu Nanjing UniversityChina Reasoning about Progress of Concurrent Objects
Yu FengFeng, Yu University of California, Santa BarbaraChina Visualization by Example
Yuan FengFeng, Yuan Centre for Quantum Software and Information, University of Technology Sydney, Australia Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Jerome FeretFeret, Jerome INRIA ParisFrance Sharing Ghost Variables in a Collection of Abstract Domains
Alan FernFern, Alan Explanations for Dynamic Programming Panel: Reasoning for machine learning at large
Pietro FerraraFerrara, Pietro Università Ca' Foscari, Venezia, ItalyItaly BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results
Johannes K. FichteFichte, Johannes K. TU DresdenGermany Exploiting Database Systems and Treewidth for Counting Panel: Reasoning for machine learning at large
Jean-Christophe FilliatreFilliatre, Jean-Christophe CNRS, ParisFrance Committee Member in Program Committee within the CPP-track
Robby FindlerFindler, Robby Northwestern University, USAUnited States Does Blame Shifting Work? Panelist in Panel within the POPL mark 15 Year Retrospective Panel-track
Bernd FinkbeinerFinkbeiner, Bernd Saarland UniversityGermany How to Win First-Order Safety Games
Denis FirsovFirsov, Denis Guardtime ASEstonia Verified Security of BLT Signature Scheme
Mathias FleuryFleury, Mathias MPI-INFGermany Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Spencer P. FlorenceFlorence, Spencer P. Northwestern University, USA Towards Fully Abstract Compilation for Esterel
Matthew FluetFluet, Matthew Rochester Institute of TechnologyUnited States Disentanglement in Nested-Parallel Programs
Kenny FonerFoner, Kenny Galois How Can I Academia When My Brain Can't Even? Mental Health in Grad School and Beyond Panel Panelist in Panelists within the PLMW-track Invited Speaker in Invited speakers within the PLMW-track
Arnaud FontaineFontaine, Arnaud ANSSI The use of Coq for Common Criteria Evaluations
Yannick ForsterForster, Yannick Saarland UniversityGermany A Coq Library of Undecidable Problems Verified Programming of Turing Machines in Coq Undecidability of Higher-Order Unification Formalised in Coq Coq à la Carte - A Practical Approach to Modular Syntax with Binders The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
Jeffrey S. FosterFoster, Jeffrey S. Tufts UniversityUnited States Committee Member in Program Committee within the POPL Research Papers-track
Nate FosterFoster, Nate Cornell UniversityUnited States Industrial Relations Co-Chair in Organizing Committee for POPL 2020 Network Verification: Past, Present, and Future [T7] Programming and Reasoning with Kleene Algebra with Tests Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time Organizer in Organizers within the POPL Ally Skills Session-track
Cédric FournetFournet, Cédric Microsoft Research Committee Member in Program Committee within the POPL Research Papers-track
Juliana FrancoFranco, Juliana Microsoft Research, CambridgeUnited Kingdom Panel Panelist in Panelists within the PLMW-track
Cameron FreerFreer, Cameron Massachusetts Institute of TechnologyUnited States Optimal Approximate Sampling From Discrete Probability Distributions Committee Member in Steering Committee within the LAFI-track
Aymeric FromherzFromherz, Aymeric Carnegie Mellon University Steel: scaling up memory reasoning for F*
Frank FuFu, Frank Session Chair of Invited Talks, Pulses, Errors and Categories (part of PLanQC)
Hongfei FuFu, Hongfei Shanghai Jiao Tong University Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
Xiang FuFu, Xiang Institute for Quantum Information & State Key Laboratory of High Performance Computing, College of Computer, National University of Defense Technology, Changsha, ChinaChina Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Zhoulai FuFu, Zhoulai IT University of Copenhagen, Denmark Detecting Floating-Point Errors via Atomic Conditions
G Marco GaboardiGaboardi, Marco Boston UniversityUnited States Research as a collaborative effort Invited Speaker in Invited speakers within the PLMW-track
Letterio GallettaGalletta, Letterio IMT School for Advanced Studies Securing Interruptible Enclaves
Vijay GaneshGanesh, Vijay University of WaterlooCanada Committee Member in Program Committee within the POPL Research Papers-track
Pierre GantyGanty, Pierre IMDEA Software InstituteSpain PC Member in Program Committee within the VMCAI-track
Ronald GarciaGarcia, Ronald University of British Columbia Gradual Typing as if Types Mattered Committee Member in Program Committee within the WGT-track
Isabel Garcia-ContrerasGarcia-Contreras, Isabel IMDEA Software InstituteSpain Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Philippa GardnerGardner, Philippa Imperial College LondonUnited Kingdom Interactive Knowledge Shares
Tal GarfinkelGarfinkel, Tal Stanford University Committee Member in Program Committee within the PriSC-track
Deepak GargGarg, Deepak Max Planck Institute for Software SystemsGermany Trace-Relating Compiler Correctness and Secure Compilation The High-Level Benefits of Low-Level Sandboxing Committee Member in Steering Committee within the PriSC-track
Austin GarrettGarrett, Austin MIT MetaPPL: Inference Algorithms as First-Class Generative Models Gen and MetaGen
Jack GarzellaGarzella, Jack University of UtahUnited States Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Adria GasconGascon, Adria Alan Turing Institute Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL
Martin GebserGebser, Martin University of Klagenfurt, AustriaAustria Committee Member in Program Committee within the PADL-track
Francesco A. GencoGenco, Francesco A. IHPST, Université Paris 1 Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
Aina Linn GeorgesGeorges, Aina Linn Aarhus University Mechanized Reasoning about a Capability Machine
Alex GerdesGerdes, Alex University of Gothenburg, SwedenSweden Committee Member in Program Committee within the PADL-track
Neil GhaniGhani, Neil University of Strathclyde Three equivalent ordinal notation systems in Cubical Agda
Roberto GiacobazziGiacobazzi, Roberto University of Verona and IMDEA Software InstituteItaly Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Jeremy GibbonsGibbons, Jeremy Department of Computer Science, University of OxfordUnited Kingdom Committee Member in Program Committee within the PEPM-track
Jürgen GieslGiesl, Jürgen RWTH Aachen UniversityGermany Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification
Andrew N. GlaudellGlaudell, Andrew N. University of Maryland Optimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation
Klaus GleissenthallGleissenthall, Klaus University of California, San Diego Committee Member in Program Committee within the PriSC-track
Klaus v. GleissenthallGleissenthall, Klaus v. University of California at San Diego, USA Short Talk: Automatically Eliminating Speculative Leaks With Blade
Robert GlückGlück, Robert University of CopenhagenDenmark Committee Member in Program Committee within the PEPM-track
Shilpi GoelGoel, Shilpi Centaur Technology, Inc. Verifying x86 Instruction Implementations
Harrison GoldsteinGoldstein, Harrison University of Pennsylvania Combinatorial Testing for Algebraic Data Types
Anitha GollamudiGollamudi, Anitha Harvard University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Hannah GommerstadtGommerstadt, Hannah Vassar College Panel Panelist in Panelists within the PLMW-track
Andrew D. GordonGordon, Andrew D. Microsoft Research and University of EdinburghUnited Kingdom Committee Member in Steering Committee within the LAFI-track
Colin GordonGordon, Colin Drexel UniversityUnited States Committee Member in Program Committee within the POPL Research Papers-track
Roberta GoriGori, Roberta University of PisaItaly Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Nikos GorogiannisGorogiannis, Nikos Facebook and Middlesex University LondonUnited Kingdom Committee Member in Program Committee within the ADSL-track Co-chair in Organizing Committee within the ADSL-track
Alexey GotsmanGotsman, Alexey IMDEA Software InstituteSpain Committee Member in Program Committee within the POPL Research Papers-track
Adam GrabowskiGrabowski, Adam University of BialystokPoland Committee Member in Program Committee within the CPP-track
Chris GranadeGranade, Chris Microsoft Committee Member in Program Committee within the PLanQC-track
Michael GreenbergGreenberg, Michael Pomona College Publicity Chair in Organizing Committee for POPL 2020 Gradual Algebraic Data Types Executable Formal Semantics for the POSIX Shell
Benjamin GregoireGregoire, Benjamin INRIA Formal Verification of a Constant-Time Preserving C Compiler Committee Member in Program Committee within the PriSC-track
Alberto GriggioGriggio, Alberto Fondazione Bruno KesslerItaly PC Member in Program Committee within the VMCAI-track
Dan GrossmanGrossman, Dan University of WashingtonUnited States REPLICA: REPL Instrumentation for Coq Analysis Organizing Committee in Organizing Committee within the POPL mark 15 Year Retrospective Panel-track
Lindsay GrovesGroves, Lindsay Victoria University of Wellington Decidable Subtyping for Path Dependent Types
Torsten GrustGrust, Torsten University of TübingenGermany Committee Member in Program Committee within the PEPM-track
Ronghui GuGu, Ronghui Columbia University Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Marco GuarnieriGuarnieri, Marco IMDEA Software InstituteSpain Exorcising Spectres with Secure Compilers
Arjun GuhaGuha, Arjun University of Massachusetts Amherst Committee Member in Program Committee within the POPL Research Papers-track
Zheng GuoGuo, Zheng University of California, San DiegoUnited States Program Synthesis by Type-Guided Abstraction Refinement
Aarti GuptaGupta, Aarti Princeton UniversityUnited States Synthesizing Environment Invariants for Modular Hardware Verification Abstract Interpretation of Distributed Network Control Planes
Ashutosh GuptaGupta, Ashutosh TIFR, India PC Member in Program Committee within the VMCAI-track
Gopal GuptaGupta, Gopal Opening Whitebox Induction of Default Rules Using High-Utility Itemset Mining AQuA: ASP-based Visual Question Answering Panel: Programming with logic for the masses Panel: Reasoning for machine learning at large
Sankha Narayan GuriaGuria, Sankha Narayan University of Maryland, College ParkUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Dilian GurovGurov, Dilian KTH Royal Institute of TechnologySweden Practical Abstractions for Automated Verification of Shared-Memory Concurrency
H Jennifer HackettHackett, Jennifer University of Nottingham, UKUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Thanh Hai NguyenHai Nguyen, Thanh On Repairing Web Services Workflows
Ákos HajduHajdu, Ákos Budapest University of Technology and EconomicsHungary Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Niels HallenbergHallenberg, Niels On the Effects of Integrating Region-based Memory Managemen and Generational Garbage Collection in ML Panel: Memory and real-time programming in practice
Jesse Michael HanHan, Jesse Michael University of Pittsburgh A Formal Proof of the Independence of the Continuum Hypothesis
Martin Adam Thomas HandleyHandley, Martin Adam Thomas University of Nottingham Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell
Marcel HarkHark, Marcel RWTH Aachen University, Germany Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Daniel HausmannHausmann, Daniel Friedrich-Alexander-Universität Erlangen-NürnbergGermany Cheap CTL Compassion in NuSMV
Paul HeHe, Paul University of PennsylvaniaUnited States An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction Interaction Trees: Representing Recursive and Impure Programs in Coq
Shaobo HeHe, Shaobo University of UtahUnited States Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Markus HecherHecher, Markus Exploiting Database Systems and Treewidth for Counting Panel: Reasoning for machine learning at large
Bettina HeimHeim, Bettina Microsoft Invited Talk: Q# - Going Beyond Quantum Circuits Committee Member in Program Committee within the PLanQC-track
Edith HeiterHeiter, Edith Saarland University A Coq Library of Undecidable Problems
Ben HermannHermann, Ben Paderborn UniversityGermany Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Manuel HermenegildoHermenegildo, Manuel IMDEA Software Institute and T.U. of Madrid (UPM)Spain Committee Member in Program Committee within the PADL-track
Christian HerreraHerrera, Christian fortiss GmbHGermany Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Chris HeunenHeunen, Chris University of EdinburghUnited Kingdom Automated distribution of quantum circuits via hypergraph partitioning
Michael HicksHicks, Michael University of MarylandUnited States Session Chair of Quantum-Classical Communication (part of PLanQC) Tracking Errors through Types in Quantum Programs A Verified Optimizer for Quantum Circuits Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages Verified translation between low-level quantum languages A Language for Probabilistically Oblivious Computation Organizer in Organizing Committee within the PLanQC-track Moderator in Panel within the POPL mark 15 Year Retrospective Panel-track Committee Member in Steering Committee within the PriSC-track
Kesha HietalaHietala, Kesha University of Maryland Tracking Errors through Types in Quantum Programs A Verified Optimizer for Quantum Circuits Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages
Jonas Kastberg HinrichsenHinrichsen, Jonas Kastberg IT University of CopenhagenDenmark Actris: Session-Type Based Reasoning in Separation Logic
Andrew K. HirschHirsch, Andrew K. Max Planck Institute for Software SystemsGermany Panel Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Panelist in Panelists within the PLMW-track
André HirschowitzHirschowitz, André Université Côte d'Azur Reduction Monads and Their Signatures
Aquinas HoborHobor, Aquinas National University of Singapore A Functional Proof Pearl: Inverting the Ackermann Hierarchy
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Workshops Co-Chair in Organizing Committee for POPL 2020 Committee Member in Tutorials Evaluation Committee within the POPL TutorialFest-track
Lukáš HolíkHolík, Lukáš Brno University of Technology Committee Member in Program Committee within the ADSL-track
Zechen HouHou, Zechen East China Normal University Symbolic Bisimulation for Open and Parameterized System
Cătălin HriţcuHriţcu, Cătălin Inria ParisFrance Session Chair of Invited talk (part of CPP) Trace-Relating Compiler Correctness and Secure Compilation PC Chairs' report The Next 700 Relational Program Logics Program Co-Chair in Program Committee within the CPP-track Chair in Steering Committee within the PriSC-track
Justin HsuHsu, Justin University of Wisconsin-Madison, USAUnited States Session Chair of Afternoon 1 (part of PLMW) [T6] Verifying Probabilistic Properties with Couplings A Probabilistic Separation Logic Relational Proofs for Quantum Programs Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time Committee Member in Organizing Committee within the POPL Mentoring Breakfasts-track Organizer in Organizing Committee within the PLMW-track Committee Member in Program Committee within the LAFI-track
Chunchao HuHu, Chunchao School of Information Engineering, Zhengzhou University, Zhengzhou, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Jason Z.S. HuHu, Jason Z.S. McGill University Undecidability of D<: and Its Decidable Fragments
Zhenjiang HuHu, Zhenjiang Peking UniversityChina Session Chair of Opening & Keynote Talk 1 (part of PEPM) Opening Co-chair in PC Chairs within the PEPM-track Co-chair in Program Committee within the PEPM-track
Anqi HuangHuang, Anqi Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Guangyao HuangHuang, Guangyao Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Yipeng HuangHuang, Yipeng Princeton UniversityUnited States Committee Member in Program Committee within the PLanQC-track
John HughesHughes, John Chalmers University of Technology, SwedenSweden Session Chair of Memory and Real-Time in Functional Programming (part of PADL) Committee Member in Program Committee within the PADL-track
Marieke HuismanHuisman, Marieke University of TwenteNetherlands Practical Abstractions for Automated Verification of Shared-Memory Concurrency
Shih-Han HungHung, Shih-Han University of Maryland A Verified Optimizer for Quantum Circuits Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages
Warren HuntHunt, Warren University of Texas Committee Member in Program Committee within the CPP-track
Chung-Kil HurHur, Chung-Kil Seoul National UniversityKorea, South Session Chair of Program Logics (part of POPL Research Papers) An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification Interaction Trees: Representing Recursive and Impure Programs in Coq Committee Member in Program Committee within the POPL Research Papers-track
Rémi HutinHutin, Rémi IRISA / ENS RennesFrance A CompCert Compiler that Preserves Cryptographic Constant-time Formal Verification of a Constant-Time Preserving C Compiler
Graham HuttonHutton, Graham University of Nottingham, UKUnited Kingdom Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell
Antti HyvärinenHyvärinen, Antti Università della Svizzera ItalianaSwitzerland A Cooperative Parallelization Approach for Property-Directed k-Induction
I Atsushi IgarashiIgarashi, Atsushi Kyoto University, JapanJapan Session Chair of Sessions 3 & 4 (part of PEPM) Dependently-Typed Multi-Stage Programming Revisited (invited talk) Space-Efficient Gradual Typing in Coercion-Passing Style Gradual Typing for Extensibility by Rows Committee Member in Program Committee within the WGT-track
Neil ImmermanImmerman, Neil University of Massachusetts, Amherst Complexity and Information in Invariant Inference
Fabian ImmlerImmler, Fabian Carnegie Mellon University The Poincaré-Bendixson Theorem in Isabelle/HOL
Radu IosifIosif, Radu VERIMAG, CNRS, Université Grenoble-Alpes The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions Committee Member in Program Committee within the ADSL-track Co-chair in Organizing Committee within the ADSL-track
Oren Ish-ShalomIsh-Shalom, Oren Tel Aviv University, IsraelIsrael Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
Takuya IshizawaIshizawa, Takuya Kyoto UniversityJapan Generalized Property-Directed Reachability for Hybrid Systems
Shachar ItzhakyItzhaky, Shachar Technion, IsraelIsrael Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
Hideya IwasakiIwasaki, Hideya University of Electro-Communications, Japan Committee Member in Program Committee within the PEPM-track
J Guilhem JaberJaber, Guilhem LS2N, Université de NantesFrance SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References Committee Member in Selection Committee within the POPL Student Research Competition-track
Julian JabsJabs, Julian University of Tübingen Decomposition Diversity with Symmetric Data and Codata
Bart JacobsJacobs, Bart imec-DistriNet, Dept. CS, KU LeuvenBelgium The Future is Ours: Prophecy Variables in Separation Logic
Koen JacobsJacobs, Koen KU Leuven Fully Abstract from Static to Gradual
Swen JacobsJacobs, Swen CISPA Helmholtz Center for Information SecurityGermany Promptness and Bounded Fairness in Concurrent and Parameterized Systems
Radha JagadeesanJagadeesan, Radha DePaul University Committee Member in Program Committee within the POPL Research Papers-track
Marie-Christine JakobsJakobs, Marie-Christine TU Darmstadt, Germany Artifact Evaluation Chair in Artifact-Evaluation Committee within the VMCAI-track PC Member in Program Committee within the VMCAI-track Artifact Evaluation Chair in Organizing Committee within the VMCAI-track
Michael B. JamesJames, Michael B. University of California, San DiegoUnited States Synthesis from Partial Refinement Types Program Synthesis by Type-Guided Abstraction Refinement
Dustin JamnerJamner, Dustin Northeastern University, USA Graduality and Parametricity: Together Again for the First Time
David JaninJanin, David Bordeaux INP / CNRS LaBRI / Bordeaux UniversityFrance A Timed IO Monad Panel: Memory and real-time programming in practice
Ali Javadi-AbhariJavadi-Abhari, Ali IBM T.J. Watson Research Center, New York, USA Tuning up entanglement through the cloud using Qiskit-OpenPulse
Ranjit JhalaJhala, Ranjit University of California, San DiegoUnited States Program Synthesis by Type-Guided Abstraction Refinement
Limin JiaJia, Limin Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the POPL Research Papers-track Committee Member in Program Committee within the PriSC-track
Hanru JiangJiang, Hanru Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, ChinaChina Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Lei JinJin, Lei School of Information Engineering, Zhengzhou University, Zhengzhou, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Mark JonesJones, Mark Portland State University Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc
Martin JonášJonáš, Martin Fondazione Bruno KesslerItaly Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Jacques-Henri JourdanJourdan, Jacques-Henri CNRS, LRI, Université Paris-SudFrance Spy Game: Verifying a Local Generic Solver in Iris RustBelt Meets Relaxed Memory
Kwanghee JungJung, Kwanghee VRASP: A Virtual Reality Environment for Learning Answer Set Programming Panel: Programming with logic for the masses
Ralf JungJung, Ralf MPI-SWSGermany Stacked Borrows: An Aliasing Model for Rust The Future is Ours: Prophecy Variables in Separation Logic
Kristoffer Just Arndal AndersenJust Arndal Andersen, Kristoffer Aarhus UniversityDenmark Technical Support in Organizing Committee for POPL 2020
David JustoJusto, David University of California, San DiegoUnited States Program Synthesis by Type-Guided Abstraction Refinement
K M. Frans KaashoekKaashoek, M. Frans Massachusetts Institute of Technology, USA Verifying concurrent Go code in Coq with Goose
Bishoksan KafleKafle, Bishoksan The university of MelbourneAustralia Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Jan-Oliver KaiserKaiser, Jan-Oliver MPI-SWS RustBelt Meets Relaxed Memory
Cezary KaliszykKaliszyk, Cezary University of Innsbruck Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Yukiyoshi KameyamaKameyama, Yukiyoshi University of Tsukuba, JapanJapan Module Generation without Regret
Benjamin Lucien KaminskiKaminski, Benjamin Lucien RWTH Aachen University, GermanyGermany Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom Session Chair of Probabilistic Programming (part of POPL Research Papers) Session Chair of Sessions 1 & 2 (part of PEPM) Frex: Free extensions for normalisation by evaluation (invited talk) Co-chair in Program Committee within the LAFI-track Committee Member in Program Committee within the POPL Research Papers-track
Hrutvik KanabarKanabar, Hrutvik University of Kent Verified efficient libraries for CakeML
Naoki KanazawaKanazawa, Naoki IBM Research, Tokyo, Japan Tuning up entanglement through the cloud using Qiskit-OpenPulse
Jeehoon KangKang, Jeehoon KAISTSouth Korea Artifact Evaluation Co-Chair in Organizing Committee for POPL 2020 Stacked Borrows: An Aliasing Model for Rust CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tobias KappéKappé, Tobias University College London Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time
Jerzy KarczmarczukKarczmarczuk, Jerzy France Committee Member in Program Committee within the LAFI-track
Jens KatelaanKatelaan, Jens Strong-Separation Logic Extending the Profile Abstraction for Complete Entailment Checking of Symbolic Heaps of Bounded Treewidth
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification
Alex KavvosKavvos, Alex Aarhus UniversityDenmark Recurrence Extraction for Functional Programs through Call-by-Push-Value
Ilya KaysinKaysin, Ilya National Research University Higher School of Economics, JetBrains ResearchRussia Mechanization of Data Race Freedom guarantee proofs for Weakestmo memory model
Sven KeidelKeidel, Sven JGU MainzGermany A Systematic Approach to Abstract Interpretation of Program Transformations
Chantal KellerKeller, Chantal LRI, Université Paris-SudFrance SMTCoq: Safe and efficient automation in Coq (Keynote) Invited Speaker in Invited speakers within the CoqPL-track
Martin KelloggKellogg, Martin University of Washington, SeattleUnited States Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Marie KerjeanKerjean, Marie Committee Member in Program Committee within the LAFI-track
Kristian KerstingKersting, Kristian TU DarmstadtGermany Committee Member in Program Committee within the PADL-track
Rami Gökhan KıcıKıcı, Rami Gökhan University of California at San Diego, USA Short Talk: Automatically Eliminating Speculative Leaks With Blade
Deokhwan KimKim, Deokhwan CSAIL, MIT Synthesizing Replacement Classes
Dongjoo KimKim, Dongjoo Seoul National University CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
Hong-Seok KimKim, Hong-Seok Working Sessions I Committee Member in Organizing Committee within the HASE-track
Jinwoo KimKim, Jinwoo University of Wisconsin-Madison Proving Unrealizability for Imperative Syntax-Guided Synthesis Problems
Jung-Eun KimKim, Jung-Eun Yale University Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Yonghyun KimKim, Yonghyun Seoul National University, South Korea CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
Yoonseung KimKim, Yoonseung Seoul National University (South Korea) Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Zachary KincaidKincaid, Zachary Princeton UniversityUnited States Workshops Co-Chair in Organizing Committee for POPL 2020 Committee Member in Tutorials Evaluation Committee within the POPL TutorialFest-track
Alexis KingKing, Alexis Northwestern University Does Blame Shifting Work?
Dominik KirstKirst, Dominik Saarland UniversityGermany A Coq Library of Undecidable Problems
Oleg KiselyovKiselyov, Oleg Committee Member in Program Committee within the PEPM-track
Aleks KissingerKissinger, Aleks Radboud University Committee Member in Program Committee within the PLanQC-track
Hsiang-Shang ‘Josh’ KoKo, Hsiang-Shang ‘Josh’ Institute of Information Science, Academia Sinica, Taiwan Web Chair in Organizing Committee for POPL 2020 Committee Member in Program Committee within the PADL-track
Wen KokkeKokke, Wen University of EdinburghUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Michalis KokologiannakisKokologiannakis, Michalis MPI-SWS, GermanyGreece Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University, UK Session Chair of Logical Engines and Applications (part of PADL) Closing Chair in Program Chairs within the PADL-track
Sung Kook KimKook Kim, Sung University of California, Davis Deterministic Parallel Fixpoint Computation
Andre KornellKornell, Andre Tulane University Quantum CPOs
Eric KoskinenKoskinen, Eric Stevens Institute of Technology Committee Member in Program Committee within the POPL Research Papers-track
Laura KovacsKovacs, Laura Vienna University of Technology (TU Wien)Austria PC Member in Program Committee within the VMCAI-track
Dexter KozenKozen, Dexter Cornell UniversityUnited States Semantics of Higher-Order Probabilistic Programs with Conditioning [T7] Programming and Reasoning with Kleene Algebra with Tests Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time
Robbert KrebbersKrebbers, Robbert Delft University of TechnologyNetherlands Session Chair of Contributed Talks & Coq Developers (part of CoqPL) Session Chair of Invited Talk (part of CoqPL) Session Chair of Morning 2 (part of PLMW) Relational reasoning using concurrent separation logic Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages [T4] Proving Semantic Type Soundness in Iris Actris: Session-Type Based Reasoning in Separation Logic Committee Member in Organizing Committee within the POPL Mentoring Breakfasts-track Organizer in Organizing Committee within the PLMW-track Co-chair in Organizing Committee within the CoqPL-track
Jan KretinskyKretinsky, Jan TU Munich, Germany PC Member in Program Committee within the VMCAI-track
Neel KrishnaswamiKrishnaswami, Neel Computer Laboratory, University of Cambridge Seminaïve Evaluation for a Higher-Order Functional Language
Paul KrogmeierKrogmeier, Paul University of Illinois at Urbana-Champaign Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
Andre KuhlenschmidtKuhlenschmidt, Andre Indiana UniversityUnited States Hypercoercions and a Framework for Equivalence of Cast Calculi
Prashant KumarKumar, Prashant Explanations for Dynamic Programming Panel: Reasoning for machine learning at large
Ramana KumarKumar, Ramana DeepMindUnited Kingdom Committee Member in Program Committee within the PADL-track
Fabian KunzeKunze, Fabian Saarland University A Coq Library of Undecidable Problems Verified Programming of Turing Machines in Coq The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
Lindsey KuperKuper, Lindsey University of California, Santa Cruz Making Progress Under Uncertainty in SMT Solving, Research, and Life Invited Speaker in Invited speakers within the PLMW-track
Ismail KuruKuru, Ismail Drexel UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Markus KusanoKusano, Markus Virginia TechUnited States PC Member in Program Committee within the VMCAI-track
Marta KwiatkowskaKwiatkowska, Marta University of Oxford Safety and Robustness for Deep Learning with Provable Guarantees Invited Speaker in Invited Speakers within the VMCAI-track
Robert KünnemannKünnemann, Robert CISPA, Saarland University Universal Composability is Secure Compilation
L Risto LaanojaLaanoja, Risto Guardtime AS Verified Security of BLT Signature Scheme
Brian LaChanceLaChance, Brian Tufts University Towards efficient, executable abstract machines
Ambroise LafontLafont, Ambroise Inria, France Reduction Monads and Their Signatures
Ori LahavLahav, Ori Tel Aviv University Student Research Competition Co-Chair in Organizing Committee for POPL 2020 Session Chair of Papers 8 (part of VMCAI) Session Chair of Automated verification and SAT solving (part of CPP) Co-chair in Selection Committee within the POPL Student Research Competition-track PC Member in Program Committee within the VMCAI-track Committee Member in Program Committee within the CPP-track
Shuvendu K. LahiriLahiri, Shuvendu K. Microsoft Research Committee Member in Program Committee within the POPL Research Papers-track
Peter LammichLammich, Peter The University of Manchester Committee Member in Program Committee within the CPP-track
Ruben LapauwLapauw, Ruben Katholieke Universiteit LeuvenBelgium Improving Parity Game Solvers with Justifications
Vincent LaporteLaporte, Vincent Inria The use of Coq for Common Criteria Evaluations Formal Verification of a Constant-Time Preserving C Compiler
Dominique Larchey-WendlingLarchey-Wendling, Dominique CNRS, LORIAFrance A Coq Library of Undecidable Problems Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the ADSL-track
Ken Friis LarsenLarsen, Ken Friis DIKU, University of CopenhagenDenmark Hermes: Implementing Cryptography without Side-channels
Ben LaurieLaurie, Ben Google Research Working Sessions I Working Sessions II Committee Member in Organizing Committee within the HASE-track
Lukas LazarekLazarek, Lukas Northwestern University Does Blame Shifting Work?
Quang Loc LeLe, Quang Loc Teesside UniversityUnited Kingdom Committee Member in Program Committee within the ADSL-track
Dongho LEELEE, Dongho LRI / CEA LIST, Univ Paris Saclay Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
Wonyeol LeeLee, Wonyeol KAISTSouth Korea Towards Verified Stochastic Variational Inference for Probabilistic Programs Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Rodolphe LepigreLepigre, Rodolphe MPI-SWSGermany The Future is Ours: Prophecy Variables in Separation Logic
Sorin LernerLerner, Sorin University of California, San Diego REPLICA: REPL Instrumentation for Coq Analysis
Xavier LeroyLeroy, Xavier Collège de FranceFrance Theorem provers are a P.L. researcher's best friend Invited Speaker in Invited speakers within the PLMW-track Panelist in Panel within the POPL mark 15 Year Retrospective Panel-track
Mohsen LesaniLesani, Mohsen University of California, Riverside Session Chair of Synthesis (part of POPL Research Papers) Session Chair of Synthesis (part of POPL Research Papers) Committee Member in Program Committee within the POPL Research Papers-track
Thomas LetanLetan, Thomas ANSSI The use of Coq for Common Criteria Evaluations FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
Michael LeuschelLeuschel, Michael University of Düsseldorf Committee Member in Program Committee within the PADL-track
Maxwell LevatichLevatich, Maxwell YaleUnited States Solving LIA* Using Approximations
Alexander K. LewLew, Alexander K. Massachusetts Institute of Technology, USAUnited States MetaPPL: Inference Algorithms as First-Class Generative Models Gen and MetaGen Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages Chair in Organizer within the POPL LGBTQ Lunch-track
Robert Y. LewisLewis, Robert Y. Vrije Universiteit AmsterdamNetherlands Session Chair of Formalized mathematics 1 (part of CPP)
Ondřej LhotákLhoták, Ondřej University of WaterlooCanada Undecidability of D<: and Its Decidable Fragments
Quanxi LiLi, Quanxi University of Science and Technology of ChinaChina Context-Sensitive and Duration-Aware Qubit Mapping for Various NISQ Devices
Hongjin LiangLiang, Hongjin Nanjing University, ChinaChina Committee Member in Program Committee within the CPP-track
Kevin LiaoLiao, Kevin Max Planck Institute for Security and Privacy A Probabilistic Separation Logic
Dan LicataLicata, Dan Wesleyan UniversityUnited States Recurrence Extraction for Functional Programs through Call-by-Push-Value
Benjamin LimLim, Benjamin Carnegie Mellon University WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
Bert LindenhoviusLindenhovius, Bert Tulane University Quantum CPOs
Sam LindleyLindley, Sam The University of Edinburgh and Imperial College LondonUnited Kingdom Committee Member in Program Committee within the POPL Research Papers-track
Sven LinkerLinker, Sven Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Francesca Alessandra LisiLisi, Francesca Alessandra University of BariItaly Committee Member in Program Committee within the PADL-track
Tadeusz LitakLitak, Tadeusz FAU Erlangen-Nuremberg, INF 8Germany Cheap CTL Compassion in NuSMV The High-Level Benefits of Low-Level Sandboxing
Chang LiuLiu, Chang Citadel Securities A Language for Probabilistically Oblivious Computation
Mengqi LiuLiu, Mengqi Yale University Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Wanwei LiuLiu, Wanwei National University of Defense Technology Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Y. Annie LiuLiu, Y. Annie Stony Brook UniversityUnited States Session Chair of Reasoning and Efficient Implementation (part of PADL) Session Chair of Invited Experience and Direction Session (Continued) (part of PADL) Closing Chair in Program Chairs within the PADL-track
Pavel LougovskiLougovski, Pavel Oak Ridge National Laboratory Extending Modern C++ for Heterogeneous Quantum-Classical Computing
Kuang-Chen LuLu, Kuang-Chen Indiana University BloomingtonUnited States Hypercoercions and a Framework for Equivalence of Cast Calculi
M Julian MackayMackay, Julian Victoria University of Wellington Decidable Subtyping for Path Dependent Types
Brooks MacLachlanMacLachlan, Brooks McMaster University GOOL: A Generic Object-Oriented Language
Dougal MaclaurinMaclaurin, Dougal Co-chair in Program Committee within the LAFI-track
Eric MadelaineMadelaine, Eric INRIA Symbolic Bisimulation for Open and Parameterized System
P. MadhusudanMadhusudan, P. University of Illinois at Urbana-ChampaignUnited States Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
Marco MaggesiMaggesi, Marco Università di Firenze Reduction Monads and Their Signatures
Ratul MahajanMahajan, Ratul University of Washington, Intentionet Abstract Interpretation of Distributed Network Control Planes
Assia MahboubiMahboubi, Assia INRIAFrance Committee Member in Program Committee within the CPP-track Co-chair in Organizing Committee within the CoqPL-track
Kenji MaillardMaillard, Kenji Inria Nantes & University of Chile The Next 700 Relational Program Logics
Carol MakMak, Carol University of Oxford A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation
Gregory MalechaMalecha, Gregory BedRock SystemsUnited States Interaction Trees: Representing Recursive and Impure Programs in Coq
Stefan MalewskiMalewski, Stefan University of Santiago de Chile Gradual Algebraic Data Types
Sharad MalikMalik, Sharad Princeton UniversityUnited States Synthesizing Environment Invariants for Modular Hardware Verification
Roman ManevichManevich, Roman Mellanox TechnologiesIsrael Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
Ravi MangalMangal, Ravi Georgia Institute of TechnologyUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Carole MannMann, Carole R.S.L Registration in Organizing Committee for POPL 2020
Vikash MansinghkaMansinghka, Vikash MIT Gen and MetaGen
Vikash K. MansinghkaMansinghka, Vikash K. MIT MetaPPL: Inference Algorithms as First-Class Generative Models Monte Carlo Semantic Differencing of Probabilistic Programs Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages Optimal Approximate Sampling From Discrete Probability Distributions
Alessio MansuttiMansutti, Alessio CNRS, LSV, ENS Paris-Saclay Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Giulio ManzonettoManzonetto, Giulio Université Paris 13France Taylor Subsumes Scott, Berry, Kahn and Plotkin
Claude MarchéMarché, Claude Inria Saclay & Université Paris-Saclay Deductive Verification with Ghost Monitors
Matteo MarescottiMarescotti, Matteo Università della Svizzera ItalianaSwitzerland A Cooperative Parallelization Approach for Property-Directed k-Induction
Patrick MassotMassot, Patrick Université Paris Sud Formalising perfectoid spaces
Hidehiko MasuharaMasuhara, Hidehiko Tokyo Institute of TechnologyJapan Committee Member in Program Committee within the PEPM-track
Umang MathurMathur, Umang University of Illinois at Urbana-ChampaignUnited States Deciding Memory Safety for Single-Pass Heap-Manipulating Programs Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tom MattinsonMattinson, Tom University of Oxford Density Functions of Statistical Probabilistic Programs
Luke MaurerMaurer, Luke Galois, Inc Exploits as Insecure Compilation
Damiano MazzaMazza, Damiano CNRSFrance Backpropagation in the Simply Typed Lambda-calculus with Linear Negation Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Alexander McCaskeyMcCaskey, Alexander Oak Ridge National Laboratory Extending Modern C++ for Heterogeneous Quantum-Classical Computing
David C. McKayMcKay, David C. IBM T.J. Watson Research Center, New York, USA Tuning up entanglement through the cloud using Qiskit-OpenPulse
James McKinnaMcKinna, James University of Edinburgh Blame tracking at higher fidelity
Tyler McMullenMcMullen, Tyler FastlyUnited States Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing
Jonathan MendelsonMendelson, Jonathan University of Pennsylvania Provenance-Guided Synthesis of Datalog Programs
Denis MerigouxMerigoux, Denis INRIAFrance Steel: scaling up memory reasoning for F*
Eric MertensMertens, Eric Galois, Inc. Exploits as Insecure Compilation
Roland MeyerMeyer, Roland TU Braunschweig Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Zeina MigeedMigeed, Zeina University of California, Los Angeles What is Decidable about Gradual Types?
Tiffany MintzMintz, Tiffany Oak Ridge National Laboratory Extending Modern C++ for Heterogeneous Quantum-Classical Computing
Sasa MisailovicMisailovic, Sasa University of Illinois at Urbana-ChampaignUnited States Augmented Example-based Synthesis using Relational Perturbation Properties
Michael MisloveMislove, Michael Tulane Local Chair in Organizing Committee for POPL 2020 Quantum CPOs
Torben MogensenMogensen, Torben DIKU, University of Copenhagen Hermes: Implementing Cryptography without Side-channels
Anshuman MohanMohan, Anshuman National University of SingaporeSingapore A Functional Proof Pearl: Inverting the Ackermann Hierarchy
David MonniauxMonniaux, David CNRS, VERIMAGFrance PC Member in Program Committee within the VMCAI-track
Scott MooreMoore, Scott Galois, Inc Exploits as Insecure Compilation
Shirley MooreMoore, Shirley Oak Ridge National Laboratory Extending Modern C++ for Heterogeneous Quantum-Classical Computing
Edward MorehouseMorehouse, Edward Wesleyan University Recurrence Extraction for Functional Programs through Call-by-Push-Value
J. Garrett MorrisMorris, J. Garrett University of Kansas, USAUnited States Blame tracking at higher fidelity Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc
Madhavan MukundMukund, Madhavan Chennai Mathematical InstituteIndia Formalizing and Checking Multilevel Consistency
Stefan K. MullerMuller, Stefan K. Carnegie Mellon UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Cesar MunozMunoz, Cesar NASAUnited States Committee Member in Program Committee within the CPP-track
Adithya MuraliMurali, Adithya University of Illinois at Urbana-Champaign Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
Andrzej MurawskiMurawski, Andrzej University of OxfordUnited Kingdom Committee Member in Program Committee within the POPL Research Papers-track
Jeffrey MurphyMurphy, Jeffrey Panel: Memory and real-time programming in practice RTMLton: An SML Runtime for Real-Time Systems
Marco MuñizMuñiz, Marco Aalborg UniversityDenmark Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology, SwedenSweden Committee Member in Program Committee within the POPL Research Papers-track
Carlos Mão de FerroMão de Ferro, Carlos Lasige / Faculty of Sciences, Universidade de LisboaPortugal Student Volunteer Co-Chair in Organizing Committee for POPL 2020 Student Volunteer Co-Chair in Student Volunteers Committee within the POPL Student Volunteers-track
Anders MörtbergMörtberg, Anders Department of Mathematics, Stockholm UniversitySweden Cubical Synthetic Homotopy Theory
Jan Tobias MühlbergMühlberg, Jan Tobias imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium Securing Interruptible Enclaves
Christian MüllerMüller, Christian Technical University of MunichGermany How to Win First-Order Safety Games
N Santosh NagarakatteNagarakatte, Santosh Rutgers University, USAUnited States Committee Member in Steering Committee within the PriSC-track
Mayur NaikNaik, Mayur University of Pennsylvania Invited Talk: Learning Interpretable Rules from Structured Data Panel: Experience and Direction Provenance-Guided Synthesis of Datalog Programs [T1] Building Program Reasoning Tools using LLVM and Z3
Keisuke NakanoNakano, Keisuke Tohoku UniversityJapan Committee Member in Program Committee within the PEPM-track
Egor NamakonovNamakonov, Egor JetBrains Research, St Petersburg University Correctness of compilation of OCaml memory model to Power
Kedar NamjoshiNamjoshi, Kedar Bell Labs, NokiaUnited States Session Chair of Papers 2 (part of VMCAI) Witnessing Secure Compilation Synthesis of Coordination Programs from Linear Temporal Specifications PC Member in Program Committee within the VMCAI-track
Aleksandar NanevskiNanevski, Aleksandar IMDEA Software InstituteSpain Committee Member in Program Committee within the ADSL-track
Raja NatarajanNatarajan, Raja Tata Institute of Fundamental Research Mumbai A Constructive Formalization of the Weak Perfect Graph Theorem
Gil NeigerNeiger, Gil Intel CorporationUnited States Persistency Semantics of the Intel-x86 Architecture
Max NewNew, Max Northeastern University Graduality and Parametricity: Together Again for the First Time
Vinh The NguyenNguyen, Vinh The Texas Tech UniversityUnited States VRASP: A Virtual Reality Environment for Learning Answer Set Programming Panel: Programming with logic for the masses
Jakob Botsch NielsenNielsen, Jakob Botsch Concordium Blockchain Research Center, Aarhus University ConCert: A Smart Contract Certification Framework in Coq
Vivek NigamNigam, Vivek Federal University of Paraiba / fortissGermany Committee Member in Program Committee within the CPP-track
Tobias NipkowNipkow, Tobias Technische Universität München Session Chair of Formalized mathematics 2 (part of CPP) Proof Pearl: Braun Trees
Yannic NollerNoller, Yannic Humboldt-Universität zu Berlin Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Job NoormanNoorman, Job imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium Securing Interruptible Enclaves
Fredrik Nordvall ForsbergNordvall Forsberg, Fredrik University of Strathclyde Three equivalent ordinal notation systems in Cubical Agda
O Peter O'HearnO'Hearn, Peter Facebook Interactive Knowledge Shares Incorrectness Logic Committee Member in Program Committee within the ADSL-track
Fritz ObermeyerObermeyer, Fritz Invited talk: Nonstandard Interpretation in Pyro
Bruno C. d. S. OliveiraOliveira, Bruno C. d. S. The University of Hong Kong, Hong KongHong Kong Kind Inference for Datatypes Committee Member in Program Committee within the PEPM-track
Luca OlivieriOlivieri, Luca JuliaSoft SRLItaly BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results
Federico OlmedoOlmedo, Federico University of Chile & IMFD Chile Runtime Analysis of Quantum Programs: A Formal Approach A Mechanized Formalization of GraphQL
C.-H. Luke OngOng, C.-H. Luke University of OxfordUnited Kingdom Density Functions of Statistical Probabilistic Programs A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation
Wytse OortwijnOortwijn, Wytse ETH ZürichSwitzerland Practical Abstractions for Automated Verification of Shared-Memory Concurrency
Klaus OstermannOstermann, Klaus University of Tübingen, GermanyGermany Decomposition Diversity with Symmetric Data and Codata
Roy OverbeekOverbeek, Roy Vrije Universiteit AmsterdamNetherlands Formalizing Determinacy of Concurrent Revisions
Scott OwensOwens, Scott University of Kent, UKUnited Kingdom Panelist in Panel within the POPL mark 15 Year Retrospective Panel-track
P Saswat PadhiPadhi, Saswat University of California, Los AngelesUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Michele PaganiPagani, Michele IRIF - Université de ParisFrance Backpropagation in the Simply Typed Lambda-calculus with Linear Negation Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Jens PalsbergPalsberg, Jens University of California, Los Angeles Session Chair of Welcome + SIGPLAN Award Ceremony (part of POPL Research Papers) What is Decidable about Gradual Types? Committee Member in Program Committee within the PEPM-track
Jihyeok ParkPark, Jihyeok KAIST, South KoreaSouth Korea Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
James ParkerParker, James University of Maryland Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Bryan ParnoParno, Bryan Carnegie Mellon UniversityUnited States WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
Masoumeh ParsaParsa, Masoumeh A DSL for Integer Range Reasoning: Partition, Interval and Mapping Diagrams Panel: Reasoning for machine learning at large
Gaurav ParthasarathyParthasarathy, Gaurav ETH Zurich The Future is Ours: Prophecy Variables in Separation Logic
Pardis PashakhanlooPashakhanloo, Pardis University of PennsylvaniaUnited States [T1] Building Program Reasoning Tools using LLVM and Z3
Andrei PaskevichPaskevich, Andrei LRI, Université Paris-Sud & CNRS Deductive Verification with Ghost Monitors
Grant PassmorePassmore, Grant Imandra Inc. Invited Talk: An Introduction to the Imandra Automated Reasoning System Panel: Experience and Direction
Marco PatrignaniPatrignani, Marco Stanford University & CISPA United States Session Chair of Compartmentalization, memory safety, and isolation (part of PriSC) Universal Composability is Secure Compilation Memory Safety Preservation for WebAssembly Trace-Relating Compiler Correctness and Secure Compilation Exorcising Spectres with Secure Compilers
Daniel PattersonPatterson, Daniel Northeastern UniversityUnited States Foreign Function Typing: Semantic Type Soundness for FFIs Committee Member in Program Committee within the PriSC-track
Andreas PavlogiannisPavlogiannis, Andreas Aarhus University Fast, Sound, and Effectively Complete Dynamic Race Prediction
Dusko PavlovicPavlovic, Dusko University of HawaiiUnited States Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Jennifer PaykinPaykin, Jennifer Galois, Inc.United States Exploits as Insecure Compilation Invited Talk: Quantum Computing for Programming Languages Researchers Committee Member in Program Committee within the PLanQC-track
Barak A. PearlmutterPearlmutter, Barak A. Maynooth UniversityIreland Committee Member in Program Committee within the LAFI-track
Nicolas PeltierPeltier, Nicolas The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions
Álvaro García PerezPerez, Álvaro García IMDEA Software Institute Committee Member in Program Committee within the PEPM-track
Valentin PerrellePerrelle, Valentin CEA, LIST, France Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control Qbricks: formal verification in quantum computing
Dmitry PetrashkoPetrashko, Dmitry Stripe Committee Member in Program Committee within the WGT-track
David PichardiePichardie, David Univ Rennes, ENS Rennes, IRISAFrance Towards Formally Verified Just-in-Time compilation A CompCert Compiler that Preserves Cryptographic Constant-time Formal Verification of a Constant-Time Preserving C Compiler
Brigitte PientkaPientka, Brigitte McGill University General Chair in Organizing Committee for POPL 2020 Session Chair of Datalog, OO + Functional Programming (part of POPL Research Papers) Session Chair of Welcome + SIGPLAN Award Ceremony (part of POPL Research Papers) Session Chair of Invited Talk (part of POPL Research Papers) Session Chair of Invited Talk (part of POPL Research Papers) Opening Committee Member in Organizers within the POPL W@POPL Dinner-track Panelist in Panel within the POPL mark 15 Year Retrospective Panel-track
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States Session Chair of Mechanized metatheory (part of CPP) Interaction Trees: Representing Recursive and Impure Programs in Coq Committee Member in Program Committee within the CPP-track Organizing Committee in Organizing Committee within the POPL mark 15 Year Retrospective Panel-track Panelist in Panel within the POPL mark 15 Year Retrospective Panel-track
Frank PiessensPiessens, Frank KU Leuven Securing Interruptible Enclaves
Maciej PirógPiróg, Maciej University of WrocławPoland Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers
Ruzica PiskacPiskac, Ruzica Yale University, USAUnited States Session Chair of Papers 4 (part of VMCAI) Solving LIA* Using Approximations Industrial Relations Co-Chair in Steering Committee within the VMCAI-track
Gordon PlotkinPlotkin, Gordon Google A Simple Differentiable Programming Language
Andreas PodelskiPodelski, Andreas University of Freiburg, GermanyGermany Session Chair of Papers 6 (part of VMCAI) Panel "The Future of Software Verification" at VMCAI PC Member in Program Committee within the VMCAI-track Steering Committee Chair in Steering Committee within the VMCAI-track
Piotr PolesiukPolesiuk, Piotr University of Wrocław Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers
Nadia PolikarpovaPolikarpova, Nadia University of California, San DiegoUnited States Programs Synthesis with Separation Logic [T3] Synthesizing Programs from Types Program Synthesis by Type-Guided Abstraction Refinement PC Member in Program Committee within the VMCAI-track Committee Member in Program Committee within the ADSL-track
Hernan Ponce de LeonPonce de Leon, Hernan fortiss GmbHGermany Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Enrico PontelliPontelli, Enrico New Mexico State University On Repairing Web Services Workflows
Enrico PontelliPontelli, Enrico New Mexico State UniversityUnited States Committee Member in Program Committee within the PADL-track
Sorawee PorncharoenwasePorncharoenwase, Sorawee University of WashingtonUnited States Fixing Code That Explodes Under Symbolic Evaluation
Alex PotaninPotanin, Alex Victoria University of WellingtonNew Zealand Decidable Subtyping for Path Dependent Types
Kostiantyn PotomkinPotomkin, Kostiantyn Committee Member in Artifact-Evaluation Committee within the VMCAI-track
François PottierPottier, François Inria, FranceFrance Spy Game: Verifying a Local Generic Solver in Iris
Damien PousPous, Damien CNRS, ENS Lyon Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
Marc PouzetPouzet, Marc École normale supérieureFrance Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
Sarah PowersPowers, Sarah Oak Ridge National Laboratory Extending Modern C++ for Heterogeneous Quantum-Classical Computing
Jonathan ProtzenkoProtzenko, Jonathan Microsoft Research, RedmondUnited States Session Chair of Compartmentalization, memory safety, and isolation (part of PriSC) Working Sessions I Committee Member in Organizing Committee within the HASE-track Committee Member in Program Committee within the PriSC-track Committee Member in Steering Committee within the PriSC-track
Loïc PujetPujet, Loïc Gallinette Project-Team, Inria Cubical Synthetic Homotopy Theory
Sylvie PutotPutot, Sylvie École Polytechnique Committee Member in Program Committee within the POPL Research Papers-track
David PymPym, David University College London Committee Member in Program Committee within the ADSL-track
Pierre-Marie PédrotPédrot, Pierre-Marie INRIA The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects
Q Shaz QadeerQadeer, Shaz FacebookUnited States PC Member in Program Committee within the VMCAI-track
Xiaogang QiangQiang, Xiaogang Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
R Azalea RaadRaad, Azalea MPI-SWS, GermanyUnited Kingdom Session Chair of Program Logics (part of POPL Research Papers) Persistency Semantics of the Intel-x86 Architecture Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the POPL Research Papers-track
Gabriel RadanneRadanne, Gabriel University of Freiburg, GermanyFrance Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Mukund RaghothamanRaghothaman, Mukund University of Southern California Provenance-Guided Synthesis of Datalog Programs
Vincent RahliRahli, Vincent University of Birmingham Committee Member in Program Committee within the CPP-track
Tom RainforthRainforth, Tom Department of Statistics, University of Oxford Divide, Conquer, and Combine: a New Inference Strategy for Probabilistic Programs with Stochastic Support
Zvonimir RakamaricRakamaric, Zvonimir University of UtahUnited States Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Tahina RamananandroRamananandro, Tahina Microsoft Research, n.n.United States Short Talk: Everparse
Robert RandRand, Robert University of MarylandUnited States Session Chair of Introduction and Invited Talks (part of PLanQC) Tracking Errors through Types in Quantum Programs A Verified Optimizer for Quantum Circuits Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages Verified translation between low-level quantum languages [T2] Verified Quantum Computing Organizer in Organizing Committee within the PLanQC-track Chair in Program Committee within the PLanQC-track
Francesco RanzatoRanzato, Francesco University of PadovaItaly Committee Member in Program Committee within the POPL Research Papers-track
Marianna RapoportRapoport, Marianna University of WaterlooCanada The Future is Ours: Prophecy Variables in Separation Logic
Christoph RauchRauch, Christoph FAU Erlangen-Nürnberg, Lehrstuhl 8Germany Cheap CTL Compassion in NuSMV
Benoit RazetRazet, Benoit Galois, Inc Exploits as Insecure Compilation
Adrian Rebola PardoRebola Pardo, Adrian TU Wien Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs
Tamara RezkRezk, Tamara InriaFrance Committee Member in Steering Committee within the PriSC-track
Rojin RezvanRezvan, Rojin Sharif University Parameterized Verification under TSO is PSPACE-Complete
Francesco RiccaRicca, Francesco University of Calabria, ItalyItaly Committee Member in Program Committee within the PADL-track
Lionel RiegRieg, Lionel Verimag Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Manuel RiggerRigger, Manuel ETH ZurichSwitzerland Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Martin C. RinardRinard, Martin C. MITUnited States Optimal Approximate Sampling From Discrete Probability Distributions Synthesizing Replacement Classes
Noam RinetzkyRinetzky, Noam Tel Aviv UniversityIsrael Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation Committee Member in Program Committee within the POPL Research Papers-track
Talia RingerRinger, Talia University of WashingtonUnited States REPLICA: REPL Instrumentation for Coq Analysis Organizing Chair in Organizing Committee within the POPL mark 15 Year Retrospective Panel-track
Xavier RivalRival, Xavier INRIA/CNRS/ENS ParisFrance Session Chair of Abstract Interpretation (part of POPL Research Papers) Towards Verified Stochastic Variational Inference for Probabilistic Programs Committee Member in Program Committee within the POPL Research Papers-track
Exequiel RivasRivas, Exequiel Inria Paris The Next 700 Relational Program Logics
Christine RizkallahRizkallah, Christine The University of MelbourneAustralia Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the CoqPL-track
Christian RoldánRoldán, Christian University of Buenos AiresArgentina Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tiark RompfRompf, Tiark Purdue UniversityUnited States Committee Member in Program Committee within the POPL Research Papers-track
Neil Julien RossRoss, Neil Julien Dalhousie UniversityCanada Optimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation Committee Member in Program Committee within the PLanQC-track
Marc RothRoth, Marc Saarland University and MMCI and Merton College, Oxford University The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
Eric Rothstein-MorrisRothstein-Morris, Eric Singapore University of Technology and DesignSingapore Systematic Classification of Attackers via Bounded Model Checking
Arjen RouvoetRouvoet, Arjen Delft University of TechnologyNetherlands Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
Grigore RoşuRoşu, Grigore University of Illinois at Urbana-ChampaignUnited States Invited talk: Matching Logic: The Foundation of the K Framework
Sukyoung RyuRyu, Sukyoung KAIST, South Korea Committee Member in Program Committee within the POPL Research Papers-track
Yann Régis-GianasRégis-Gianas, Yann IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2France FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
S Marek S. BaranowskiS. Baranowski, Marek University of UtahUnited States Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Yaniv Sa'arSa'ar, Yaniv Nokia Bell Labs, Kfar Saba, Israel Synthesis of Coordination Programs from Linear Temporal Specifications
Feras SaadSaad, Feras Massachusetts Institute of TechnologyUnited States Optimal Approximate Sampling From Discrete Probability Distributions
Mooly SagivSagiv, Mooly Tel Aviv UniversityIsrael Complexity and Information in Invariant Inference
Konstantinos (Kostis) SagonasSagonas, Konstantinos (Kostis) Uppsala University, SwedenSweden Session Chair of Invited Experience and Direction Session (part of PADL) Session Chair of Invited Experience and Direction Session (Continued) (part of PADL) [T5] Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models
Mouhammad SakrSakr, Mouhammad Saarland UniversityGermany Promptness and Bounded Fairness in Concurrent and Parameterized Systems
Malavika SamakSamak, Malavika CSAIL, MITUnited States Synthesizing Replacement Classes
Roopsha SamantaSamanta, Roopsha Purdue University Session Chair of Complexity / Decision Procedures (part of POPL Research Papers) Session Chair of Synthesis and Decision Procedures (part of POPL Research Papers) Augmented Example-based Synthesis using Relational Perturbation Properties Committee Member in Program Committee within the POPL Research Papers-track
Michael SammlerSammler, Michael MPI-SWS The High-Level Benefits of Low-Level Sandboxing
Roland SamuelsonSamuelson, Roland Georgia Institute of Technology Internal Type-Theoretic Complexity Analysis
Alex Sanchez-SternSanchez-Stern, Alex University of California, San DiegoUnited States REPLICA: REPL Instrumentation for Coq Analysis
João SaraivaSaraiva, João University of Minho, Portugal Committee Member in Program Committee within the PEPM-track
Susmit SarkarSarkar, Susmit University of St. Andrews Session Chair of Concurrency / Memory (part of POPL Research Papers) Session Chair of Concurrent Programming & Session Types (part of POPL Research Papers) Committee Member in Program Committee within the POPL Research Papers-track
Isao SasanoSasano, Isao Shibaura Institute of TechnologyJapan An approach to generating text-based IDEs with syntax completion from syntax specification
Annabel SatinSatin, Annabel P.C.K. Treasurer & Conference Manager in Organizing Committee for POPL 2020
Yuhi SatoSato, Yuhi University of Tsukuba Module Generation without Regret
Christian SchillingSchilling, Christian IST AustriaAustria Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Bernhard ScholzScholz, Bernhard University of Sydney, Australia Provenance-Guided Synthesis of Datalog Programs
Tom SchrijversSchrijvers, Tom KU Leuven PλωNK: Functional Probabilistic NetKAT Committee Member in Program Committee within the PEPM-track
Daniel Schwartz-NarbonneSchwartz-Narbonne, Daniel Amazon, n.n. PC Member in Program Committee within the VMCAI-track
Helmut SeidlSeidl, Helmut Technische Universität MünchenGermany How to Win First-Order Safety Games
Martina SeidlSeidl, Martina Johannes Kepler University Linz, Austria PC Member in Program Committee within the VMCAI-track
Taro SekiyamaSekiyama, Taro National Institute of InformaticsJapan Panel Gradual Typing for Extensibility by Rows Panelist in Panelists within the PLMW-track
Peter SelingerSelinger, Peter Dalhousie University Invited Talk: Dependently Typed Quantum Programming in Proto-Quipper
Antoine SereSere, Antoine Ecole PolytechniqueFrance The Correctness of a Code Generator for a Functional Language
Ilya SergeySergey, Ilya Yale-NUS College and National University of SingaporeSingapore Committee Member in Program Committee within the CPP-track
Peter SewellSewell, Peter University of Cambridge Interactive Knowledge Shares Organizing Committee in Organizing Committee within the POPL mark 15 Year Retrospective Panel-track Panelist in Panel within the POPL mark 15 Year Retrospective Panel-track
Thomas SewellSewell, Thomas Chalmers University of Technology, SwedenSweden Proof Pearl: Braun Trees
Ramy ShahinShahin, Ramy Panel: Reasoning for machine learning at large Variability-aware Datalog
Farhad ShakerinShakerin, Farhad Whitebox Induction of Default Rules Using High-Utility Itemset Mining AQuA: ASP-based Visual Question Answering Panel: Programming with logic for the masses Panel: Reasoning for machine learning at large
Chung-chieh ShanShan, Chung-chieh Indiana University, USA Committee Member in Steering Committee within the LAFI-track
Natarajan ShankarShankar, Natarajan SRI International, USAUnited States The Correctness of a Code Generator for a Functional Language Panel "The Future of Software Verification" at VMCAI A Verified Packrat Parser Interpreter for Parsing Expression Grammars
Zhong ShaoShao, Zhong Yale UniversityUnited States Session Chair of Concurrency and linearity (part of CPP) Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Natasha SharyginaSharygina, Natasha USI Lugano, SwitzerlandSwitzerland Session Chair of Papers 1 (part of VMCAI) A Cooperative Parallelization Approach for Property-Directed k-Induction PC Member in Program Committee within the VMCAI-track
Gautham Shenoy RShenoy R, Gautham Chennai Mathematical InstituteIndia Formalizing and Checking Multilevel Consistency
Benjamin ShermanSherman, Benjamin Massachusetts Institute of Technology, USAUnited States MetaPPL: Inference Algorithms as First-Class Generative Models Gen and MetaGen Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages
Bhargav ShivkumarShivkumar, Bhargav Panel: Memory and real-time programming in practice RTMLton: An SML Runtime for Real-Time Systems
Sharon ShohamShoham, Sharon Tel Aviv universityIsrael Solving LIA* Using Approximations Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction Complexity and Information in Invariant Inference
Filip SieczkowskiSieczkowski, Filip University of WrocławPoland Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers
Jeremy G. SiekSiek, Jeremy G. Indiana University, USAUnited States Session Chair of Gradual Typing / Language Design (part of POPL Research Papers) Session Chair of Coercions (part of WGT) Space-Efficient Monotonic References Hypercoercions and a Framework for Equivalence of Cast Calculi Organizer in Organizing Committee within the WGT-track Co-chair in Program Committee within the WGT-track Committee Member in Program Committee within the POPL Research Papers-track
Jesse SigalSigal, Jesse University of EdinburghUnited Kingdom Denotational Semantics for Differentiable Programming with Manifolds
Mihaela SighireanuSighireanu, Mihaela IRIF, Université Paris Diderot, FranceFrance PC Member in Program Committee within the VMCAI-track Committee Member in Program Committee within the ADSL-track
Alexandra SilvaSilva, Alexandra University College LondonUnited Kingdom Accessibility Chair in Organizing Committee for POPL 2020 Session Chair of Semantics of Probabilistic & Quantum Programming (part of POPL Research Papers) Session Chair of Probabilistic Programming (part of POPL Research Papers) [T7] Programming and Reasoning with Kleene Algebra with Tests Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time Committee Member in Organizers within the POPL W@POPL Dinner-track Committee Member in Selection Committee within the POPL Student Research Competition-track Organizer in Organizers within the POPL Ally Skills Session-track Committee Member in Program Committee within the POPL Research Papers-track
Abhishek Kr SinghSingh, Abhishek Kr Tata Institute of Fundamental Research MumbaiIndia A Constructive Formalization of the Weak Perfect Graph Theorem
Rishabh SinghSingh, Rishabh Google BrainUnited States Augmented Example-based Synthesis using Relational Perturbation Properties
Satnam SinghSingh, Satnam Google ResearchUnited States Working Sessions II Committee Member in Organizing Committee within the HASE-track
Kartik SinghalSinghal, Kartik University of ChicagoUnited States Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages Verified translation between low-level quantum languages Quantum Hoare Types
Jeffrey Mark SiskindSiskind, Jeffrey Mark School of Electrical and Computer Engineering, Purdue University Committee Member in Steering Committee within the LAFI-track
Ingo SkupinSkupin, Ingo University of Tübingen Decomposition Diversity with Symmetric Data and Codata
Anna SlobodovaSlobodova, Anna Centaur Technology, Inc. Verifying x86 Instruction Implementations
Calvin SmithSmith, Calvin University of Wisconsin - MadisonUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Spencer SmithSmith, Spencer McMaster University, Computing and Software DepartmentCanada GOOL: A Generic Object-Oriented Language
Gert SmolkaSmolka, Gert Saarland University A Coq Library of Undecidable Problems
Steffen SmolkaSmolka, Steffen Cornell University Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time
Michael SoegtropSoegtrop, Michael Intel Committee Member in Program Committee within the CoqPL-track
Armando Solar-LezamaSolar-Lezama, Armando Massachusetts Institute of TechnologyUnited States Committee Member in Program Committee within the POPL Research Papers-track
Tran Cao SonSon, Tran Cao On Repairing Web Services Workflows
Youngju SongSong, Youngju Seoul National University CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Matthew SotoudehSotoudeh, Matthew University of California, Davis Bounded Model Checking of Deep Neural Network Controllers
Matthieu SozeauSozeau, Matthieu InriaFrance Session with the Coq Development Team A Tutorial on Equations Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
Simon SpiesSpies, Simon Saarland UniversityGermany A Coq Library of Undecidable Problems Undecidability of Higher-Order Unification Formalised in Coq
Martin SpießlSpießl, Martin LMU MunichGermany Committee Member in Artifact-Evaluation Committee within the VMCAI-track
Bas SpittersSpitters, Bas Concordium Blockchain Research Center, Aarhus University ConCert: A Smart Contract Certification Framework in Coq
Fausto SpotoSpoto, Fausto U. VeronaItaly BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results
Kathrin StarkStark, Kathrin Princeton University, USAGermany Session Chair of Decidability and complexity (part of CPP) Autosubst 2: Mechanising binders in Coq (Keynote) Coq à la Carte - A Practical Approach to Modular Syntax with Binders Committee Member in Program Committee within the CPP-track Invited Speaker in Invited speakers within the CoqPL-track
Sam StatonStaton, Sam University of Oxford A Monad for Point Processes Name generation and Higher-order Probabilistic Programming (Or is new=rnd?)
Deian StefanStefan, Deian University of California San Diego Program Co-Chair in Program Committee within the PriSC-track Committee Member in Steering Committee within the PriSC-track
Dario SteinStein, Dario University of Oxford Name generation and Higher-order Probabilistic Programming (Or is new=rnd?)
Gordon StewartStewart, Gordon Ohio University Coinductive Trees for Exact Inference of Probabilistic Programs
Jan StrejcekStrejcek, Jan Masaryk UniversityCzech Republic PC Member in Program Committee within the VMCAI-track
Pierre-Yves StrubStrub, Pierre-Yves Ecole PolytechniqueFrance Committee Member in Program Committee within the POPL Research Papers-track
Xing SuSu, Xing College of Meteorology and Oceanography, National University of Defense Technology, Changsha, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Zhendong SuSu, Zhendong ETH ZurichSwitzerland Detecting Floating-Point Errors via Atomic Conditions
Kohei SuenagaSuenaga, Kohei Graduate School of Informatics, Kyoto UniversityJapan Generalized Property-Directed Reachability for Hybrid Systems
Eijiro SumiiSumii, Eijiro Tohoku University Committee Member in Program Committee within the PEPM-track
Alexander J. SummersSummers, Alexander J. ETH Zurich PC Member in Program Committee within the VMCAI-track
Rob SumnersSumners, Rob Centaur Technology, Inc. Verifying x86 Instruction Implementations
Jun SunSun, Jun Singapore Management University, SingaporeSingapore Systematic Classification of Attackers via Bounded Model Checking
Samanvitha SundarSundar, Samanvitha Northwestern University Does Blame Shifting Work?
Joshua SunshineSunshine, Joshua Carnegie Mellon University Gradual Program Analysis Gradual Verification of Recursive Heap Data Structures
S.P. SureshSuresh, S.P. Chennai Mathematical InstituteIndia Formalizing and Checking Multilevel Consistency
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States Session Chair of Program verification (part of CPP) Committee Member in Program Committee within the CPP-track
David SwaseySwasey, David MPI-SWSGermany Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ian SweetSweet, Ian University of Maryland A Language for Probabilistically Oblivious Computation
Sol SwordsSwords, Sol Centaur Technology, Inc. Verifying x86 Instruction Implementations
T Lucas M. TabajaraTabajara, Lucas M. Rice UniversityUnited States Witnessing Secure Compilation
Nicolas TabareauTabareau, Nicolas InriaFrance Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects Committee Member in Program Committee within the CPP-track
Tomoya TabuchiTabuchi, Tomoya Kyoto UniversityJapan Space-Efficient Gradual Typing in Coercion-Passing Style
Walid TahaTaha, Walid Session Chair of Sessions 1 & 2 (part of PEPM) Acumen: A Domain-Specific Language for Cyber-Physical Systems (invited talk) Committee Member in Program Committee within the PEPM-track
Yong Kiam TanTan, Yong Kiam Carnegie Mellon University, USASingapore The Poincaré-Bendixson Theorem in Isabelle/HOL
Éric TanterTanter, Éric University of ChileChile Gradual Program Analysis Gradual Verification of Recursive Heap Data Structures Gradual Typing as if Types Mattered Gradual Algebraic Data Types Trace-Relating Compiler Correctness and Secure Compilation A Mechanized Formalization of GraphQL Committee Member in Program Committee within the WGT-track Committee Member in Program Committee within the CoqPL-track
Paul TarauTarau, Paul University of North TexasUnited States Interactive Text Graph Mining with a Prolog-based Dialog Engine Panel: Programming with logic for the masses
Thorsten TarrachTarrach, Thorsten Austrian Institute of TechnologyAustria Language Inclusion for Finite Prime Event Structures
Joseph TassarottiTassarotti, Joseph Boston College Session Chair of Contributed Talks & Coq Developers (part of CoqPL) Verifying concurrent Go code in Coq with Goose Committee Member in Program Committee within the CoqPL-track
Enrico TassiTassi, Enrico INRIAFrance Committee Member in Program Committee within the PADL-track
Christine TassonTasson, Christine University Paris Diderot Committee Member in Program Committee within the POPL Research Papers-track
Michael TautschnigTautschnig, Michael Amazon Web Services PC Member in Program Committee within the VMCAI-track
Hanneli TavanteTavante, Hanneli McGill University Student Volunteer Co-Chair in Organizing Committee for POPL 2020 Student Volunteer Co-Chair in Student Volunteers Committee within the POPL Student Volunteers-track
Jacob M. TaylorTaylor, Jacob M. University of Maryland Optimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation
Yee Whye TehTeh, Yee Whye University of Oxford Divide, Conquer, and Combine: a New Inference Strategy for Probabilistic Programs with Stochastic Support
K. Tuncay TekleTekle, K. Tuncay Stony Brook UniversityUnited States Committee Member in Program Committee within the PADL-track
Aditya V. ThakurThakur, Aditya V. University of California, DavisUnited States Deterministic Parallel Fixpoint Computation
The mathlib Community The mathlib Community The Lean mathematical library
Jérémy ThibaultThibault, Jérémy Inria Paris Trace-Relating Compiler Correctness and Secure Compilation
Peter ThiemannThiemann, Peter University of Freiburg, Germany Session Chair of Dynamic Program Analysis (part of POPL Research Papers) Session Chair of Type Systems (part of POPL Research Papers) Label-Dependent Session Types Committee Member in Program Committee within the POPL Research Papers-track
Patrick ThierThier, Patrick Exploiting Database Systems and Treewidth for Counting Panel: Reasoning for machine learning at large
Michael Kirkedal ThomsenThomsen, Michael Kirkedal DIKU, University of Copenhagen Hermes: Implementing Cryptography without Side-channels
Amin TimanyTimany, Amin imec-Distrinet KU-LeuvenBelgium Web Chair in Organizing Committee for POPL 2020 Session Chair of Language Design (part of POPL Research Papers) Session Chair of Contributed Talks (part of CoqPL) Fully Abstract from Static to Gradual The Future is Ours: Prophecy Variables in Separation Logic [T4] Proving Semantic Type Soundness in Iris
Sam Tobin-HochstadtTobin-Hochstadt, Sam Indiana UniversityUnited States Committee Member in Program Committee within the WGT-track
Andrew TolmachTolmach, Andrew Portland State University Flexible Tag-based Policies for Compartmentalized C Committee Member in Program Committee within the CoqPL-track
David TolpinTolpin, David PUB+Israel Probabilistic Programming around Gaussian Processes Committee Member in Program Committee within the LAFI-track
Yi TongTong, Yi Stony Brook University Publicity Chair in Publicity Chair within the PADL-track
Emina TorlakTorlak, Emina University of WashingtonUnited States Fixing Code That Explodes Under Symbolic Evaluation
Matías ToroToro, Matías University of Chile Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Linh TranTran, Linh National University of Singapore A Functional Proof Pearl: Inverting the Ackermann Hierarchy
Dmitriy TraytelTraytel, Dmitriy ETH ZurichSwitzerland Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Program Committee within the CPP-track
Mirco TribastoneTribastone, Mirco IMT Institute for Advanced Studies Lucca, Italy Committee Member in Program Committee within the POPL Research Papers-track
Alix TrieuTrieu, Alix Aarhus UniversityDenmark Mechanized Reasoning about a Capability Machine Formal Verification of a Constant-Time Preserving C Compiler
Ahto TruuTruu, Ahto Guardtime AS Verified Security of BLT Signature Scheme
Yuya TsudaTsuda, Yuya Kyoto UniversityJapan Space-Efficient Gradual Typing in Coercion-Passing Style
Mark TullsenTullsen, Mark Galois, Inc Exploits as Insecure Compilation
Milo TurnerTurner, Milo PLT @ Northeastern UniversityUnited States Dependent Type Systems as Macros
U Hiroshi UnnoUnno, Hiroshi University of TsukubaJapan Committee Member in Program Committee within the POPL Research Papers-track
Dominique UnruhUnruh, Dominique University of Tartu Session Chair of Formal Methods (part of PLanQC) Committee Member in Program Committee within the PLanQC-track
Caterina UrbanUrban, Caterina INRIA & École Normale SupérieureFrance PC Member in Program Committee within the VMCAI-track
Josef UrbanUrban, Josef Czech Technical University in PragueCzech Republic Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
V Viktor VafeiadisVafeiadis, Viktor MPI-SWS, GermanyGreece Persistency Semantics of the Intel-x86 Architecture Committee Member in Program Committee within the CoqPL-track
Benoit ValironValiron, Benoit LRI, CentraleSupelec, Univ. Paris SaclayFrance Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control Qbricks: formal verification in quantum computing Committee Member in Program Committee within the PLanQC-track
Jo Van BulckVan Bulck, Jo imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium Securing Interruptible Enclaves
Tijs van der Stormvan der Storm, Tijs CWI & University of Groningen, NetherlandsNetherlands High-Fidelity Metaprogramming with Separator Syntax Trees
Floris van Doornvan Doorn, Floris University of PittsburghUnited States Session Chair of Homotopy Type Theory and PC chairs' report (part of CPP) A Formal Proof of the Independence of the Continuum Hypothesis Committee Member in Program Committee within the CPP-track
Antoine Van MuylderVan Muylder, Antoine Inria Paris and Paris 7 The Next 700 Relational Program Logics
Alexander VandenbrouckeVandenbroucke, Alexander KU Leuven, BelgiumBelgium PλωNK: Functional Probabilistic NetKAT
Anthony VandikasVandikas, Anthony University of Toronto Reductions for Safety Proofs
Moshe VardiVardi, Moshe Rice University The Siren Song of Temporal Synthesis Invited Speaker in Invited Speakers within the VMCAI-track
Vasco T. VasconcelosVasconcelos, Vasco T. University of Lisbon, Portugal Label-Dependent Session Types
Marco VassenaVassena, Marco CISPA Helmholtz Center for Information SecurityGermany Session Chair of Foundations and timing channels (part of PriSC) Memory Safety Preservation for WebAssembly Short Talk: Automatically Eliminating Speculative Leaks With Blade Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Program Committee within the PriSC-track
Niki VazouVazou, Niki IMDEA Software Institute Student Research Competition Co-Chair in Organizing Committee for POPL 2020 Session Chair of SRC Presentations (part of POPL Student Research Competition) Session Chair of Analysis, verification, blame (part of WGT) Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell Committee Member in Program Committee within the WGT-track Co-chair in Selection Committee within the POPL Student Research Competition-track
Margus VeanesVeanes, Margus Microsoft Research Committee Member in Program Committee within the POPL Research Papers-track
Martin VechevVechev, Martin ETH Zürich Can Programming Languages Research impact Deep Learning 2.0?
Niccolò VeltriVeltri, Niccolò Tallinn University of Technology Formalizing π-calculus in Guarded Cubical Agda
Arnaud J. VenetVenet, Arnaud J. Facebook Deterministic Parallel Fixpoint Computation
Andrea VezzosiVezzosi, Andrea IT University Copenhagen Formalizing π-calculus in Guarded Cubical Agda
Muralidaran VijayaraghavanVijayaraghavan, Muralidaran SiFive Interactive Knowledge Shares
Eelco VisserVisser, Eelco Delft University of TechnologyNetherlands Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
Mahesh ViswanathanViswanathan, Mahesh University of Illinois at Urbana-Champaign Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
W Philip WadlerWadler, Philip University of Edinburgh, UKUnited Kingdom Blame tracking at higher fidelity Panel: Experience and Direction Invited Talk: We Are All Poor Schmucks: On the Value of Gradual Types
Riad S. WahbyWahby, Riad S. Stanford University, USA Universal Composability is Secure Compilation
David WalkerWalker, David Princeton UniversityUnited States Industrial Relations Co-Chair in Organizing Committee for POPL 2020 Abstract Interpretation of Distributed Network Control Planes
Eric WalkingshawWalkingshaw, Eric Oregon State UniversityUnited States Committee Member in Program Committee within the WGT-track
Toby WalshWalsh, Toby TU Berlin, UNSW Sydney and Data61 Germany Committee Member in Program Committee within the PADL-track
Andrea WaltherWalther, Andrea Humboldt-Universität zu BerlinGermany Committee Member in Program Committee within the LAFI-track
Chenglong WangWang, Chenglong University of Washington, USA Visualization by Example
Di WangWang, Di Carnegie Mellon UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Peixin WangWang, Peixin Shanghai Jiao Tong University Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
Qingxiang WangWang, Qingxiang University of Innsbruck Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Shuai WangWang, Shuai Hong Kong University of Science and Technology Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yuepeng WangWang, Yuepeng University of Texas at Austin Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Zhongye WangWang, Zhongye Shanghai Jiao Tong University Reentrancy? Yes. Reentrancy bug? No.
Ziteng WangWang, Ziteng University of California, San Diego Test-based Solution Filtering for Program Synthesis Program Synthesis by Type-Guided Abstraction Refinement
David WarrenWarren, David Stony Brook University Session Chair of Invited Experience and Direction Session (part of PADL) Session Chair of Invited Experience and Direction Session (Continued) (part of PADL)
Takahisa WatanabeWatanabe, Takahisa University of Tsukuba, Japan Module Generation without Regret
Dominik WehrWehr, Dominik Saarland University, Universiteit van Amsterdam A Coq Library of Undecidable Problems
Heike WehrheimWehrheim, Heike Paderborn UniversityGermany PC Member in Program Committee within the VMCAI-track
Richard WeiWei, Richard Apple Inc.United States Committee Member in Program Committee within the LAFI-track
Stephanie WeirichWeirich, Stephanie University of Pennsylvania, USAUnited States Organizing Committee in Organizing Committee within the POPL mark 15 Year Retrospective Panel-track Committee Member in Program Committee within the CoqPL-track
Georg WeissenbacherWeissenbacher, Georg Technische Universität WienAustria Language Inclusion for Finite Prime Event Structures
Sam WestrickWestrick, Sam Carnegie Mellon UniversityUnited States Disentanglement in Nested-Parallel Programs
Michael WhalenWhalen, Michael Amazon Web Services and the University of MinnesotaUnited States Panel "The Future of Software Verification" at VMCAI
John WickersonWickerson, John Imperial College LondonUnited Kingdom Persistency Semantics of the Intel-x86 Architecture
Jan WielemakerWielemaker, Jan Free University AmsterdamNetherlands Committee Member in Program Committee within the PADL-track
Thomas WiesWies, Thomas New York University Session Chair of Reasoning about Program Complexity/Efficiency (part of POPL Research Papers) Session Chair of Papers 7 (part of VMCAI) Local Reasoning for Global Graph Properties PC Member in Program Committee within the VMCAI-track Committee Member in Program Committee within the ADSL-track Committee Member in Program Committee within the POPL Research Papers-track
Dominik WintererWinterer, Dominik ETH ZürichSwitzerland Validating SMT Solvers via Test Fusion
Theo WinterhalterWinterhalter, Theo Inria — LS2N Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
Jenna Wise (DiVincenzo)Wise (DiVincenzo), Jenna Carnegie Mellon UniversityUnited States Gradual Program Analysis Gradual Verification of Recursive Heap Data Structures Gradual Verification of Recursive Heap Data Structures
Sebastian WolffWolff, Sebastian TU BraunschweigGermany Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Michael WolmanWolman, Michael McGill UniversityCanada Name generation and Higher-order Probabilistic Programming (Or is new=rnd?)
Stefan WoltranWoltran, Stefan Exploiting Database Systems and Treewidth for Counting Panel: Reasoning for machine learning at large
Hua WuWu, Hua Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Junjie WuWu, Junjie Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Xiaodi WuWu, Xiaodi University of Maryland, College ParkUnited States A Verified Optimizer for Quantum Circuits Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages Organizer in Organizing Committee within the PLanQC-track
Zhilin WuWu, Zhilin State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Committee Member in Program Committee within the ADSL-track
Maximilian WuttkeWuttke, Maximilian Saarland University A Coq Library of Undecidable Problems Verified Programming of Turing Machines in Coq
X Li-yao XiaXia, Li-yao University of Pennsylvania Interaction Trees: Representing Recursive and Impure Programs in Coq
Ningning XieXie, Ningning The University of Hong KongChina Kind Inference for Datatypes
Wanli XingXing, Wanli VRASP: A Virtual Reality Environment for Learning Answer Set Programming Panel: Programming with logic for the masses
Yingfei XiongXiong, Yingfei Peking UniversityChina Detecting Floating-Point Errors via Atomic Conditions
Chuangjie XuXu, Chuangjie Ludwig-Maximilians-Universität München Three equivalent ordinal notation systems in Cubical Agda
Jeffrey XuXu, Jeffrey UCLA Diagnosing Data Pipeline Failures Using Action Languages: A Progress Report Panel: Programming with logic for the masses
Le XuXu, Le School of Information Engineering, Zhengzhou University, Zhengzhou, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Ming XuXu, Ming East China Normal University Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
Ping XuXu, Ping Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Y Rohan YadavYadav, Rohan Carnegie Mellon University Disentanglement in Nested-Parallel Programs
Eran YahavYahav, Eran TechnionIsrael Committee Member in Program Committee within the POPL Research Papers-track
Jeremy YallopYallop, Jeremy University of Cambridge, UK Session Chair of Sessions 3 & 4 (part of PEPM)
Akihisa YamadaYamada, Akihisa National Institute of InformaticsJapan Committee Member in Program Committee within the CPP-track
Hongseok YangYang, Hongseok KAISTSouth Korea Divide, Conquer, and Combine: a New Inference Strategy for Probabilistic Programs with Stochastic Support Probabilistic Programming Towards Verified Stochastic Variational Inference for Probabilistic Programs
Weikun YangYang, Weikun Princeton UniversityUnited States Synthesizing Environment Invariants for Modular Hardware Verification
Yihang YangYang, Yihang School of Information Engineering, Zhengzhou University, Zhengzhou, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Qianchuan YeYe, Qianchuan Purdue University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Mingsheng YingYing, Mingsheng University of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University.Australia Relational Proofs for Quantum Programs Committee Member in Program Committee within the PLanQC-track
Irene YoonYoon, Irene University of PennsylvaniaUnited States Through the Interaction Forest: Modeling Concurrency in Coq with Interaction Trees
Man-Ki YoonYoon, Man-Ki Yale University Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Nobuko YoshidaYoshida, Nobuko Imperial College London Session Chair of Afternoon 2 (part of PLMW) Committee Member in Organizing Committee within the POPL Mentoring Breakfasts-track Organizer in Organizing Committee within the PLMW-track Committee Member in Program Committee within the PEPM-track
Hangyeol YuYu, Hangyeol KAIST Towards Verified Stochastic Variational Inference for Probabilistic Programs
Jintao YuYu, Jintao State Key Laboratory of Mathematical Engineering and Advanced Computing, Zhengzhou, China Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
Nengkun YuYu, Nengkun University of Technology Sydney, Australia Relational Proofs for Quantum Programs
Z Yannick ZakowskiZakowski, Yannick University of Pennsylvania An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction Interaction Trees: Representing Recursive and Impure Programs in Coq
Jakub ZalewskiZalewski, Jakub University of Edinburgh Blame tracking at higher fidelity
Francesco Zappa NardelliZappa Nardelli, Francesco InriaFrance Committee Member in Program Committee within the WGT-track
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction Interaction Trees: Representing Recursive and Impure Programs in Coq Committee Member in Program Committee within the POPL Research Papers-track
Nickolai ZeldovichZeldovich, Nickolai Massachusetts Institute of Technology, USA Verifying concurrent Go code in Coq with Goose
Muhan ZengZeng, Muhan Peking University Detecting Floating-Point Errors via Atomic Conditions
Will ZengZeng, Will Unitary FundUnited States Session Chair of NISQ (part of PLanQC) Committee Member in Program Committee within the PLanQC-track
Hongce ZhangZhang, Hongce Princeton UniversityUnited States Synthesizing Environment Invariants for Modular Hardware Verification
Jinrong ZhangZhang, Jinrong