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 Verification of Recursive Heap Data Structures Gradual Program Analysis 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 AppelAppel, Andrew 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 Verification of Recursive Heap Data Structures Gradual Program Analysis
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
Clement BlaudeauBlaudeau, Clement 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 BodikBodik, 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
Lélio BrunBrun, Lélio 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 Gen and MetaGen MetaPPL: Inference Algorithms as First-Class Generative Models Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages
Jacques CaretteCarette, Jacques McMaster UniversityCanada GOOL: A Generic Object-Oriented Language
Luis CarvalhoCarvalho, Luis 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
Fred ChongChong, Fred 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 W ChungChung, Benjamin W 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 Gen and MetaGen 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
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
Isil DilligDillig, Isil 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 DonaldsonDonaldson, Alastair 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 [T4] Proving Semantic Type Soundness in Iris The Future is Ours: Prophecy Variables in Separation Logic Stacked Borrows: An Aliasing Model for Rust 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 Coq à la Carte - A Practical Approach to Modular Syntax with Binders Undecidability of Higher-Order Unification Formalised in Coq Verified Programming of Turing Machines in Coq 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 Gen and MetaGen MetaPPL: Inference Algorithms as First-Class Generative Models
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 Whitebox Induction of Default Rules Using High-Utility Itemset Mining Opening 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 Verified translation between low-level quantum languages A Verified Optimizer for Quantum Circuits Merged Talk: A Verified Optimizer for Quantum Circuits & 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
Andrew HirschHirsch, Andrew 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 Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time Relational Proofs for Quantum Programs 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 Interaction Trees: Representing Recursive and Impure Programs in Coq CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification 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) Gradual Typing for Extensibility by Rows Space-Efficient Gradual Typing in Coercion-Passing Style 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 Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
Takuya IshizawaIshizawa, Takuya Kyoto UniversityJapan Generalized Property-Directed Reachability for Hybrid Systems
Shachar ItzhakyItzhaky, Shachar Technion, IsraelIsrael Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
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 RustBelt Meets Relaxed Memory Spy Game: Verifying a Local Generic Solver in Iris
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 The Future is Ours: Prophecy Variables in Separation Logic Stacked Borrows: An Aliasing Model for Rust
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 CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification Stacked Borrows: An Aliasing Model for Rust 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
Jonas Kastberg HinrichsenKastberg Hinrichsen, Jonas IT University of CopenhagenDenmark Actris: Session-Type Based Reasoning in Separation Logic
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 Actris: Session-Type Based Reasoning in Separation Logic [T4] Proving Semantic Type Soundness in Iris 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 LahiriLahiri, Shuvendu 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 II Working Sessions I 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 Gen and MetaGen MetaPPL: Inference Algorithms as First-Class Generative Models 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 MansinghkaMansinghka, Vikash 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 RTMLton: An SML Runtime for Real-Time Systems Panel: Memory and real-time programming in practice
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 [T1] Building Program Reasoning Tools using LLVM and Z3 Provenance-Guided Synthesis of Datalog Programs
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)