POPL 2021 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (744)

A Mridul AanjaneyaAanjaneya, Mridul Rutgers University An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
Martin AbadiAbadi, Martin Google Committee Member in Program Committee within the LAFI-track
Martín AbadiAbadi, Martín Google The Selection Monad and Decision-Making Languages
Carmine AbateAbate, Carmine Max Planck Institute for Security and Privacy, Bochum, Germany The Fox and the Hound: Comparing Fully Abstract and Robust Compilation
Parosh Aziz AbdullaAbdulla, Parosh Aziz Uppsala University, Sweden Deciding Reachability under Persistent x86-TSO Committee Member in Program Committee within the POPL -track
Umut A. AcarAcar, Umut A. Carnegie Mellon University Provably Space Efficient Parallel Functional Programming Committee Member in Program Committee within the POPL -track
Coşku AcayAcay, Coşku Cornell UniversityUnited States Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs
Beniamino AccattoliAccattoli, Beniamino Inria & Ecole Polytechnique The (In)Efficiency of Interaction
Nate AckermanAckerman, Nate Harvard University Committee Member in Program Committee within the LAFI-track
Reynald AffeldtAffeldt, Reynald National Institute of Advanced Industrial Science and Technology (AIST), Japan Committee Member in Program Committee within the CPP -track Committee Member in Program Committee within the CoqPL-track
Yuvraj AgarwalAgarwal, Yuvraj Carnegie Mellon UniversityUnited States Netter: Probabilistic, Stateful Network Models
Alejandro AguirreAguirre, Alejandro IMDEA Software Institute and T.U. of Madrid (UPM) A Pre-Expectation Calculus for Probabilistic Sensitivity
Danel AhmanAhman, Danel University of LjubljanaSlovenia Asynchronous Effects
Amal AhmedAhmed, Amal Northeastern University, USAUnited States Committee Member in Program Committee within the PriSC-track
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin-Madison, USA Session Chair of Synthesis and Repair (part of VMCAI) Committee Member in Program Committee within the VMCAI-track
Jonathan AldrichAldrich, Jonathan Carnegie Mellon UniversityUnited States Psamathe: A DSL with Flows for Safe Blockchain Assets (extended abstract)
Guillaume AllaisAllais, Guillaume University of St AndrewsUnited Kingdom Committee Member in Program Committee within the PEPM-track
Shaull AlmagorAlmagor, Shaull Technion Deciding ω-Regular Properties on Linear Recurrence Sequences
Michelle Aluf-MedinaAluf-Medina, Michelle Bar Ilan UniversityIsrael Formal Semantics and Verification of Network Based Biocomputation Circuits
Mario AlvianoAlviano, Mario University of CalabriaItaly Session Chair of Foundations and Programming Concepts at Work (part of PADL) Data validation meets Answer Set Programming Committee Member in Programme Committee within the PADL-track
Nada AminAmin, Nada Harvard UniversityUnited States Committee Member in Program Committee within the POPL -track Committee Member in Programme Committee within the PADL-track
Sean AndersonAnderson, Sean Portland State University Towards formally verified compilation of tag-based policy enforcement
June AndronickAndronick, June CSIRO's Data61 and UNSWAustralia Committee Member in Program Committee within the CPP -track Steering Committee Member in Steering Committee within the CPP -track
Carlo AngiuliAngiuli, Carlo Carnegie Mellon University Internalizing Representation Independence with Univalence
Danil AnnenkovAnnenkov, Danil Concordium Blockchain Research Center, Aarhus UniversityDenmark Extracting Smart Contracts Tested and Verified in Coq
Andrew W. AppelAppel, Andrew W. Princeton The B+-tree Index as a Verified Software Unit Committee Member in Program Committee within the PriSC-track
Mina Tahmasbi ArashlooArashloo, Mina Tahmasbi Cornell University Petr4: Formal Foundations for P4 Data Planes
Vincenzo ArceriArceri, Vincenzo Ca’ Foscari University of VeniceItaly Twinning automata and regular expressions for string static analysis
Zena M. AriolaAriola, Zena M. University of Oregon, USA Strictly Capturing Non-Strict Closures Committee Member in Program Committee within the PEPM-track
Jatin AroraArora, Jatin CMU Provably Space Efficient Parallel Functional Programming
Kenichi AsaiAsai, Kenichi Ochanomizu UniversityJapan A Functional Abstraction of Typed Trails
Mohamed Faouzi AtigAtig, Mohamed Faouzi Uppsala University, Sweden Deciding Reachability under Persistent x86-TSO Committee Member in Program Committee within the POPL -track
Robert AtkeyAtkey, Robert University of Strathclyde Session Chair of Session 3 (part of PEPM) Committee Member in Program Committee within the PEPM-track
Eric AtkinsonAtkinson, Eric MIT CSAIL Simplifying Multiple-Statement Reductions with the Polyhedral Model
Lennart AugustssonAugustsson, Lennart Epic Games Games Programming Languages BoF Session Committee Member in Program Committee within the PEPM-track
Sacha-Élie AyounAyoun, Sacha-Élie Imperial College LondonUnited Kingdom Panel: Navigating PhD studies Panelist in Panelists within the PLMW-track
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Carnegie Mellon University, USAUnited States Netter: Probabilistic, Stateful Network Models Committee Member in Program Committee within the CPP -track Committee Member in Program Committee within the CoqPL-track
Shaun AzzopardiAzzopardi, Shaun University of Gothenburg Committee Member in Artifact Evaluation Committee within the VMCAI-track
B Casper Bach PoulsenBach Poulsen, Casper Delft University of Technology Staged Effects and Handlers for Modular Languages with Abstraction Committee Member in Program Committee within the PEPM-track Committee Member in Steering Committee within the PEPM-track
Patrick BahrBahr, Patrick IT University of CopenhagenDenmark Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
Alexey BakhirkinBakhirkin, Alexey Committee Member in Artifact Evaluation Committee within the VMCAI-track
Stephanie BalzerBalzer, Stephanie Carnegie Mellon University, USAUnited States Session Chair of Tuesday Panel (part of PLMW) Co-chair in Organizing Committee within the PLMW-track
Anindya BanerjeeBanerjee, Anindya IMDEA Software InstituteSpain A Formal Proof of PAC Learnability for Decision Stumps On Algebraic Abstractions for Concurrent Separation Logics
Kshitij BansalBansal, Kshitij GoogleUnited States Decomposing Data Structure Commutativity Proofs with mn-Differencing
Aurèle BarrièreBarrière, Aurèle Univ Rennes, IRISA Formally Verified Speculation and Deoptimization in a JIT Compiler
Gilles BartheBarthe, Gilles MPI-SP, Germany / IMDEA Software Institute, Spain High-Assurance Cryptography in the Spectre Era Deciding Accuracy of Differential Privacy Schemes A Pre-Expectation Calculus for Probabilistic Sensitivity
Mark BattyBatty, Mark University of KentUnited Kingdom Committee Member in Program Committee within the POPL -track
Kevin BatzBatz, Kevin RWTH Aachen University Relatively Complete Verification of Probabilistic Programs
Guillaume BauBau, Guillaume Committee Member in Artifact Evaluation Committee within the VMCAI-track
Pascal BaumannBaumann, Pascal Max Planck Institute for Software Systems (MPI-SWS)Germany Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
Santiago BautistaBautista, Santiago Univ Rennes, ENS Rennes, Inria, IRISAFrance Petr4: Formal Foundations for P4 Data Planes
Johan BayBay, Johan Aarhus University Mechanized Logical Relations for Termination-Insensitive Noninterference
Felipe Bañados SchwerterBañados Schwerter, Felipe University of British ColumbiaCanada Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
Antonio Becerra-TeronBecerra-Teron, Antonio University of AlmeriaSpain Declarative Debugging of XML Queries
Bernd BeckerBecker, Bernd Albert-Ludwigs-University FreiburgGermany On Pre- and Inprocessing for Weighted MaxSAT
Heiko BeckerBecker, Heiko MPI-SWSGermany Lassie: HOL4 Tactics by Example Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
McCoy R. BeckerBecker, McCoy R. Charles River Analytics Genify.jl: Transforming Julia into Gen to enable programmable inference
Michael BenediktBenedikt, Michael University of Oxford, UK Generating Collection Transformations from Proofs
Jesper BengtsonBengtson, Jesper IT University of Copenhagen Machine-Checked Semantic Session Typing Committee Member in Program Committee within the CoqPL-track
Véronique BenzakenBenzaken, Véronique Université Paris SaclayFrance A Coq Formalization of Data Provenance
Josh BerdineBerdine, Josh Facebook Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the VMCAI-track
Emery D. BergerBerger, Emery D. University of Massachusetts AmherstUnited States Robin Milner Award Talk: "Structural Language Models of Code"
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States The B+-tree Index as a Verified Software Unit Chairs' report and community meeting Conference Co-Chair in Organization Committee within the CPP -track
Bruno BernardoBernardo, Bruno Nomadic Labs Formally Verified Decentralized Exchange with Mi-Cho-Coq
Nathalie BertrandBertrand, Nathalie INRIA RennesFrance A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
Dirk BeyerBeyer, Dirk LMU Munich, GermanyGermany Committee Member in Program Committee within the VMCAI-track
Cole BiaforeBiafore, Cole Georgia Institute of Technology Over-Approximating Reachability for Boolean Programs in Polynomial Time
Annette BieniusaBieniusa, Annette Technische Universität KaiserslauternGermany Committee Member in Program Committee within the POPL -track
Eli BinghamBingham, Eli Broad Institute Committee Member in Program Committee within the LAFI-track
Lars BirkedalBirkedal, Lars Aarhus University Toward Complete Stack Safety for Capability Machines Reasoning About Monotonicity in Separation Logic Contextual Refinement of the Michael-Scott Queue (Proof Pearl) Efficient and Provable Local Capability Revocation using Uninitialized Capabilities Mechanized Logical Relations for Termination-Insensitive Noninterference Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Nikolaj BjørnerBjørner, Nikolaj Microsoft Research Committee Member in Program Committee within the VMCAI-track
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands A Modular Isabelle Framework for Verifying Saturation Provers Steering Committee Member in Steering Committee within the CPP -track
Sandrine BlazyBlazy, Sandrine Univ Rennes, IRISAFrance Formally Verified Speculation and Deoptimization in a JIT Compiler
Sören BleikertzBleikertz, Sören Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
Roderick BloemBloem, Roderick Institute of Software Technology, Graz University of Technology Session Chair of Case Studies (part of VMCAI) Committee Member in Program Committee within the VMCAI-track
Martin BodinBodin, Martin InriaFrance Committee Member in Selection Committee within the POPL Student Research Competition-track
Nathaniel BosBos, Nathaniel McGill University Lassie: HOL4 Tactics by Example
Ahmed BouajjaniBouajjani, Ahmed IRIF, Université Paris DiderotFrance Deciding Reachability under Persistent x86-TSO Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the VMCAI-track
Dmitri BoulytchevBoulytchev, Dmitri Saint Petersburg State University / JetBrains ResearchRussia Efficient Fair Conjunction for Structurally-Recursive Relations Certified Semantics for miniKanren
Thomas BourgeatBourgeat, Thomas MIT CSAIL An experience report on writing usable DSLs in Coq
William J. BowmanBowman, William J. University of British ColumbiaCanada Compilation as Multi-Language Semantics Committee Member in Program Committee within the POPL -track
Edwin BradyBrady, Edwin University of St. Andrews, UKUnited Kingdom Committee Member in Programme Committee within the PADL-track
Joachim BreitnerBreitner, Joachim DFINITY FoundationGermany Committee Member in Program Committee within the CPP -track Committee Member in Programme Committee within the PADL-track
Patrick BrinichBrinich, Patrick Drexel University Verification of Algorithm and Code Generation for Signal Transforms
Martin BrombergerBromberger, Martin MPI-INFGermany Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
Fraser BrownBrown, Fraser Stanford University, USA Session Chair of Secure compilers & cryptography (part of PriSC) High-level high-speed high-assurance crypto Committee Member in Program Committee within the PriSC-track
Stefan BrunthalerBrunthaler, Stefan Universität der Bundeswehr MünchenGermany Towards Efficient and Verified Virtual Machines for Dynamic Languages
Javier BurroniBurroni, Javier University of Massachusetts Amherst Parametric Inversion of Non-Invertible Programs
Matteo BusiBusi, Matteo Università di Pisa - Dipartimento di Informatica The Fox and the Hound: Comparing Fully Abstract and Robust Compilation
William E. ByrdByrd, William E. University of Alabama at Birmingham, USAUnited States Semantics-based Synthesis in miniKanren
Pierre-Léo BégayBégay, Pierre-Léo Orange Labs & Verimag Developing and certifying Datalog optimizations in Coq/MathComp
C David CaoCao, David University of California, San Diego Automated Dependent Resource Analysis
Michael CarbinCarbin, Michael Massachusetts Institute of Technology On the Automatic Derivation of Importance Samplers from Pairs of Probabilistic Programs Simplifying Multiple-Statement Reductions with the Polyhedral Model λS: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
Jacques CaretteCarette, Jacques McMaster UniversityCanada Formalizing Category Theory in Agda
Harold CarrCarr, Harold Oracle Labs, USAUnited States Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Elliot CattCatt, Elliot ANU On the Formalisation of Kolmogorov Complexity
Raphaël CauderlierCauderlier, Raphaël Nomadic Labs Formally Verified Decentralized Exchange with Mi-Cho-Coq
Sunjay CauligiCauligi, Sunjay University of California at San Diego, USA High-Assurance Cryptography in the Spectre Era Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Evan CavalloCavallo, Evan Carnegie Mellon University Internalizing Representation Independence with Univalence
Ethan CecchettiCecchetti, Ethan Cornell UniversityUnited States Giving Semantics to Program-Counter Labels via Secure Effects
Pavol CernyCerny, Pavol TU WienAustria Committee Member in Program Committee within the POPL -track
Rohit ChadhaChadha, Rohit University of Missouri Deciding Accuracy of Differential Privacy Schemes
Tej ChajedChajed, Tej Massachusetts Institute of Technology, USAUnited States Record Updates in Coq [T4] Iris – A Modular Foundation for Higher-Order Concurrent Separation Logic Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Soham ChakrabortyChakraborty, Soham IIT DelhiIndia Panel: Navigating PhD studies Panel Discussion 3: Work/Life Balance Panel Discussion 2: Improving Peer Review Panelist in Panelists within the PLMW-track
Marek ChalupaChalupa, Marek Masaryk University Committee Member in Artifact Evaluation Committee within the VMCAI-track
Alexander ChangChang, Alexander Cornell University Petr4: Formal Foundations for P4 Data Planes
Swarat ChaudhuriChaudhuri, Swarat Rice University Committee Member in Program Committee within the VMCAI-track
Chao-Hong ChenChen, Chao-Hong Indiana UniversityTaiwan A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
Mingshuai ChenChen, Mingshuai RWTH AachenGermany Committee Member in Artifact Evaluation Committee within the VMCAI-track
Sheng ChenChen, Sheng University of Louisiana at Lafayette Committee Member in Program Committee within the POPL -track
Yu-Fang ChenChen, Yu-Fang Academia Sinica, Taiwan Committee Member in Program Committee within the VMCAI-track
Yu-Ting ChenChen, Yu-Ting Committee Member in Artifact Evaluation Committee within the VMCAI-track
CHR ChhakChhak, CHR Portland State University Towards formally verified compilation of tag-based policy enforcement
Wei-Ngan ChinChin, Wei-Ngan National University of SingaporeSingapore A Synchronous Effects Logic for Temporal Verification of Pure Esterel Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
Shardul ChiplunkarChiplunkar, Shardul Massachusetts Institute of Technology Automated Synthesis of Verified Firewalls
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Automated Synthesis of Verified Firewalls Steering Committee Member in Steering Committee within the CPP -track Committee Member in Program Committee within the POPL -track
Hana ChocklerChockler, Hana King's College London Committee Member in Program Committee within the VMCAI-track
Kwanghoon ChoiChoi, Kwanghoon Chonnam National UniversitySouth Korea A Text-based Syntax Completion Method Using LR Parsing
Pritam ChoudhuryChoudhury, Pritam University of Pennsylvania A Graded Dependent Type System with a Usage-Aware Semantics
Cheng-En ChuangChuang, Cheng-En University at BuffaloUnited States Synchronous Message-Passing with Priority
Ravi ChughChugh, Ravi University of Chicago Committee Member in Program Committee within the POPL -track
Valentin ChuravyChuravy, Valentin MIT CSAIL Enzyme: High-Performance Automatic Differentiation of LLVM
Alessandro CimattiCimatti, Alessandro Fondazione Bruno KesslerItaly Proving the existence of fair paths in infinite state systems
Stefan CiobacaCiobaca, Stefan Alexandru Ioan Cuza University of Iasi Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Alison M. ClarkClark, Alison M. University of British Columbia Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
Michael CoblenzCoblenz, Michael University of Maryland at College ParkUnited States Psamathe: A DSL with Flows for Safe Blockchain Assets (extended abstract)
Jesper CockxCockx, Jesper TU DelftNetherlands Session Chair of Proof Tactics (part of CPP ) The Taming of the Rew: A Type Theory with Computational Assumptions Committee Member in Program Committee within the CPP -track
Jonathan CoganCogan, Jonathan Stanford High-level high-speed high-assurance crypto
Albert CohenCohen, Albert GoogleFrance Secure Optimization Through Opaque Observations
Cyril CohenCohen, Cyril Université Côte d’Azur, Inria, France Session Chair of Rewriting and Automated Reasoning (part of CPP ) Committee Member in Program Committee within the CPP -track
Sarah Cohen-BoulakiaCohen-Boulakia, Sarah LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay A Coq Formalization of Data Provenance
Johan CommelinCommelin, Johan Universität Freiburg Formalizing the Ring of Witt Vectors
Youyou CongCong, Youyou Tokyo Institute of TechnologyJapan Session Chair of Session 2 (part of PEPM) A Functional Abstraction of Typed Trails Panel Discussion 4: Finding Friends and Collaborators in Academia Panel Discussion 2: Improving Peer Review Committee Member in Program Committee within the PEPM-track Committee Member in Programme Committee within the PADL-track
Evelyne ContejeanContejean, Evelyne CNRS A Coq Formalization of Data Provenance
Mistral ContrastinContrastin, Mistral Facebook LondonUnited Kingdom Committee Member in Programme Committee within the PADL-track
Victor CookCook, Victor University of Central FloridaUnited States Concurrent Correctness in Vector Space
Agostino CortesiCortesi, Agostino Università Ca' Foscari VeneziaItaly Twinning automata and regular expressions for string static analysis
Andreea CosteaCostea, Andreea School of Computing, National University Of SingaporeSingapore Panel Discussion 3: Work/Life Balance
Nathanaël CourantCourant, Nathanaël INRIA Verified Code Generation for the Polyhedral Model
Pierre CrégutCrégut, Pierre Orange Labs Developing and certifying Datalog optimizations in Coq/MathComp
Marco Cusumano-TownerCusumano-Towner, Marco MIT-CSAIL On the Automatic Derivation of Importance Samplers from Pairs of Probabilistic Programs
D Loris D'AntoniD'Antoni, Loris University of Wisconsin-Madison, USA Semantics-Guided Synthesis Committee Member in Program Committee within the POPL -track
Ugo Dal LagoDal Lago, Ugo University of Bologna, Italy / Inria, FranceItaly Intersection Types and (Positive) Almost-Sure Termination The (In)Efficiency of Interaction
Raj DandekarDandekar, Raj MIT Bayesian Neural Ordinary Differential Equations
Hoang-Hai DangDang, Hoang-Hai MPI-SWSGermany Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Nils Anders DanielssonDanielsson, Nils Anders University of Gothenburg, Chalmers University of Technology Committee Member in Program Committee within the CPP -track
Olivier DanvyDanvy, Olivier Yale-NUS College and School of Computing, SingaporeSingapore Committee Member in Program Committee within the PEPM-track
Eva DarulovaDarulova, Eva MPI-SWS Lassie: HOL4 Tactics by Example
Arnaud de Grandmaisonde Grandmaison, Arnaud ARM Secure Optimization Through Opaque Observations
Paulo Emílio de Vilhenade Vilhena, Paulo Emílio InriaFrance A Separation Logic for Effect Handlers
Damian DechevDechev, Damian University of Central FloridaUnited States Concurrent Correctness in Vector Space
Germán Andrés DelbiancoDelbianco, Germán Andrés Nomadic LabsFrance On Algebraic Abstractions for Concurrent Separation Logics Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Delphine DemangeDemange, Delphine Univ Rennes, Inria, CNRS, IRISAFrance Panel: Doing Research in PL Committee Member in Program Committee within the PriSC-track Panelist in Panelists within the PLMW-track
Pierre DenisDenis, Pierre independent scholarBelgium Probabilistic Inference Using Generators: the Statues Algorithm
Farzaneh DerakhshanDerakhshan, Farzaneh Carnegie Mellon UniversityUnited States Panel: Navigating PhD studies Panelist in Panelists within the PLMW-track
Martin DesharnaisDesharnais, Martin Universität der Bundeswehr MünchenGermany Towards Efficient and Verified Virtual Machines for Dynamic Languages
Dominique DevrieseDevriese, Dominique Vrije Universiteit BrusselBelgium A Categorical Approach to Secure Compilation (and others things) (short talk) On the Semantic Expressiveness of Recursive Types Efficient and Provable Local Capability Revocation using Uninitialized Capabilities Fully Abstract from Static to Gradual Committee Member in Program Committee within the CoqPL-track Committee Member in Steering Committee within the PriSC-track
Ivan Di LibertiDi Liberti, Ivan Czech Academy of Sciences Functorial Semantics for Partial Theories
Daniel DietschDietsch, Daniel University of FreiburgGermany Verification of Concurrent Programs Using Petri Net Unfoldings
Işil DilligDillig, Işil University of Texas at Austin Verifying Correct Usage of Context-Free API Protocols
Rayna DimitrovaDimitrova, Rayna CISPA Helmholtz Center for Information Security Session Chair of Applications (part of VMCAI) Committee Member in Program Committee within the VMCAI-track
Craig DisselkoenDisselkoen, Craig University of California at San Diego, USA Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Vaibhav DixitDixit, Vaibhav Julia Computing Bayesian Neural Ordinary Differential Equations
Carmine DodaroDodaro, Carmine Department of Mathematics and Computer Science, University of CalabriaItaly Data validation meets Answer Set Programming
Ryan DoengesDoenges, Ryan Cornell UniversityUnited States Petr4: Formal Foundations for P4 Data Planes
Alastair F. DonaldsonDonaldson, Alastair F. Imperial College London and GoogleUnited Kingdom The Lean Researcher Invited Speaker in Invited Speakers within the PLMW-track
Pierre Donat-BouilludDonat-Bouillud, Pierre Czech Technical University Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Brijesh DongolDongol, Brijesh University of Surrey Committee Member in Program Committee within the CPP -track
Paul DownenDownen, Paul University of Oregon, USA Strictly Capturing Non-Strict Closures
Dana Drachsler CohenDrachsler Cohen, Dana TechnionIsrael Session Chair of Concurrent and Distributed Systems (part of VMCAI) Committee Member in Program Committee within the VMCAI-track
Derek DreyerDreyer, Derek MPI-SWSGermany Transfinite Step-Indexing for Termination
Sophia DrossopoulouDrossopoulou, Sophia Imperial College LondonUnited Kingdom εσόμεθα πολλώ κάρρονες – making your way in a changing world Invited Speaker in Invited Speakers within the PLMW-track
Cezara DrăgoiDrăgoi, Cezara Inria / ENS / CNRS / PSL University / Informal Systems Committee Member in Program Committee within the VMCAI-track
Stefania DumbravaDumbrava, Stefania ENSIIE Paris-ÉvryFrance Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Aaron DutleDutle, Aaron NASA Langley Research CenterUnited States Formal Verification of Semi-algebraic Sets and Real Analytic Functions
Sandra DylusDylus, Sandra Cap3 GmbHGermany Committee Member in Programme Committee within the PADL-track
Emanuele D’OsualdoD’Osualdo, Emanuele MPI-SWSGermany Committee Member in Selection Committee within the POPL Student Research Competition-track
E Harley D. Eades IIIEades III, Harley D. Augusta UniversityUnited States A Graded Dependent Type System with a Usage-Aware Semantics
Susan EisenbachEisenbach, Susan Imperial College LondonUnited Kingdom Panel: Doing Research in PL Panelist in Panelists within the PLMW-track
Richard A. EisenbergEisenberg, Richard A. Tweag I/OUnited States A Graded Dependent Type System with a Usage-Aware Semantics
Julia EisentrautEisentraut, Julia TU MunichGermany Committee Member in Artifact Evaluation Committee within the VMCAI-track
Esra ErdemErdem, Esra Sabanci University, TurkeyTurkey Committee Member in Programme Committee within the PADL-track
F Claudia FaggianFaggian, Claudia Université de Paris & CNRS Intersection Types and (Positive) Almost-Sure Termination
František FarkaFarka, František IMDEA Software Institute, Spain On Algebraic Abstractions for Concurrent Separation Logics
Azadeh FarzanFarzan, Azadeh University of TorontoCanada Program Chair in Organizing Committee for POPL 2021 PC Chair in Program Committee within the POPL -track
Grigory FedyukovichFedyukovich, Grigory Florida State UniversityUnited States Session Chair of Hyperproperties (part of VMCAI) Unbounded Procedure Summaries from Bounded Environments Committee Member in Program Committee within the VMCAI-track
Yotam M. Y. FeldmanFeldman, Yotam M. Y. Tel Aviv University Learning the Boundary of Inductive Invariants
Bertram FelgenhauerFelgenhauer, Bertram A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Amy FeltyFelty, Amy University of OttawaCanada Steering Committee Member in Steering Committee within the CPP -track
Kostas FerlesFerles, Kostas UT AustinUnited States Verifying Correct Usage of Context-Free API Protocols
Vimuth FernandoFernando, Vimuth University of Illinois at Urbana-Champaign Committee Member in Artifact Evaluation Committee within the VMCAI-track
Pietro FerraraFerrara, Pietro Università Ca' Foscari, Venezia, ItalyItaly Twinning automata and regular expressions for string static analysis
Jean-Christophe FilliatreFilliatre, Jean-Christophe CNRSFrance Committee Member in Program Committee within the VMCAI-track
Bernd FinkbeinerFinkbeiner, Bernd CISPA Helmholtz Center for Information SecurityGermany Model Checking Hyperproperties Invited Speaker in Invited Speakers within the VMCAI-track
Alberto FioriFiori, Alberto Max Planck Institute for InformaticsGermany Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
Nick FitzgeraldFitzgerald, Nick Committee Member in Program Committee within the PriSC-track
Oliver FlattFlatt, Oliver University of Utah egg: Fast and Extensible Equality Saturation
Olivier FlückigerFlückiger, Olivier Northeastern University Formally Verified Speculation and Deoptimization in a JIT Compiler
Yannick ForsterForster, Yannick Saarland UniversityGermany Session Chair of Logic, Set Theory, and Category Theory (part of CPP ) Committee Member in Program Committee within the CPP -track
Nate FosterFoster, Nate Cornell UniversityUnited States Industrial Relations in Organizing Committee for POPL 2021 Petr4: Formal Foundations for P4 Data Planes
Matt FredriksonFredrikson, Matt Carnegie Mellon UniversityUnited States Netter: Probabilistic, Stateful Network Models
Cameron FreerFreer, Cameron Massachusetts Institute of TechnologyUnited States Committee Member in Steering Committee within the LAFI-track
Aymeric FromherzFromherz, Aymeric Carnegie Mellon University Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Roy FrostigFrostig, Roy Google Research Decomposing reverse-mode automatic differentiation
Nathan FultonFulton, Nathan IBM Research CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Ignacio FábregasFábregas, Ignacio Universidad Complutense de MadridSpain On Algebraic Abstractions for Concurrent Separation Logics
G Marco GaboardiGaboardi, Marco Boston UniversityUnited States A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis Committee Member in Program Committee within the PriSC-track Committee Member in Program Committee within the POPL -track
Joshua GancherGancher, Joshua Cornell University Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs
Pierre GantyGanty, Pierre IMDEA Software Institute, Spain Committee Member in Program Committee within the POPL -track
Ronald GarciaGarcia, Ronald University of British Columbia Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
Isabel Garcia-ContrerasGarcia-Contreras, Isabel IMDEA Software InstituteSpain Committee Member in Artifact Evaluation Committee within the VMCAI-track
Miriam García SotoGarcía Soto, Miriam IST Austria Committee Member in Artifact Evaluation Committee within the VMCAI-track
Deepak GargGarg, Deepak Max Planck Institute for Software SystemsGermany A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis Committee Member in Steering Committee within the PriSC-track Committee Member in Program Committee within the POPL -track
Jacques GarrigueGarrigue, Jacques Nagoya UniversityJapan Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
Ivan GavranGavran, Ivan MPI-SWS Lassie: HOL4 Tactics by Example
Martin GebserGebser, Martin University of Klagenfurt, AustriaAustria Committee Member in Programme Committee within the PADL-track
Aina Linn GeorgesGeorges, Aina Linn Aarhus University Toward Complete Stack Safety for Capability Machines Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Silvia GhilezanGhilezan, Silvia University of Novi Sad, Mathematical Institute SASASerbia Precise Subtyping for Asynchronous Multiparty Sessions
Nick GiannarakisGiannarakis, Nick University of Wisconsin-Madison Panel: Navigating PhD studies Panelist in Panelists within the PLMW-track
Paolo G. GiarrussoGiarrusso, Paolo G. Delft University of Technology Committee Member in Program Committee within the CoqPL-track
Andy GillGill, Andy University of Kansas, USAUnited States On Adding Pattern Matching to Haskell-based Deeply Embedded Domain Specific Languages
Klaus GleissenthallGleissenthall, Klaus University of California, San Diego Artifact Evaluation Co-Chair in Organizing Committee within the VMCAI-track
Klaus v. GleissenthallGleissenthall, Klaus v. Vrije Universiteit Amsterdam, Netherlands Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Christian GodiksenGodiksen, Christian Department of Computer Science, Aalborg University A Type-Safe Structure Editor Calculus
Aman GoelGoel, Aman University of MichiganUnited States Committee Member in Artifact Evaluation Committee within the VMCAI-track
Shilpi GoelGoel, Shilpi Centaur Technology, Inc. Committee Member in Program Committee within the CPP -track
Harrison GoldsteinGoldstein, Harrison University of PennsylvaniaUnited States Social Co-Chair in Organizing Committee for POPL 2021
Léon GondelmanGondelman, Léon Aarhus University Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Laure GonnordGonnord, Laure University of Lyon & LIP, FranceFrance Committee Member in Program Committee within the POPL -track
Georges GonthierGonthier, Georges Inria Steering Committee Member in Steering Committee within the CPP -track
Colin GonzálezGonzález, Colin Université de Paris, Irif -- Nomadic Labs Formally Verified Decentralized Exchange with Mi-Cho-Coq
Juan José González-AbrilGonzález-Abril, Juan José MiST, VRAIN, Universitat Politecnica de ValenciaSpain Causal-Consistent Reversible Debugging: Improving CauDEr
Andrew D. GordonGordon, Andrew D. Microsoft Research and University of EdinburghUnited Kingdom Committee Member in Steering Committee within the LAFI-track
Maria I. GorinovaGorinova, Maria I. The University of Edinburgh Committee Member in Program Committee within the LAFI-track
Ohad GoudsmidGoudsmid, Ohad Department of Computer Science, The TechnionIsrael Compositional Model Checking for Multi-Properties
Marc GourjonGourjon, Marc Hamburg University of Technology and NXP Semiconductors Germany GmbH Explicit Leakage: Handling Side-Channel Behavior in Program Rewriting and Analysis
Hari Govind V KGovind V K, Hari Committee Member in Artifact Evaluation Committee within the VMCAI-track
Christian Uldal GraulundGraulund, Christian Uldal IT University of CopenhagenDenmark Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
Mark GrebeGrebe, Mark University of Central Missouri, USAUnited States On Adding Pattern Matching to Haskell-based Deeply Embedded Domain Specific Languages
Michael GreenbergGreenberg, Michael Pomona College Publicity Chair and Virtualization Chair in Organizing Committee for POPL 2021
Simon Oddershede GregersenGregersen, Simon Oddershede Aarhus UniversityDenmark Mechanized Logical Relations for Termination-Insensitive Noninterference Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Benjamin GregoireGregoire, Benjamin INRIA High-Assurance Cryptography in the Spectre Era
Alberto GriggioGriggio, Alberto Fondazione Bruno KesslerItaly Proving the existence of fair paths in infinite state systems
Jason GrossGross, Jason MIT CSAILUnited States A Limited Case for Reification by Type Inference
Orna GrumbergGrumberg, Orna Technion – Israel Institute of TechnologyIsrael Session Chair of Infinite-State Systems and Compilation (part of VMCAI) Compositional Model Checking for Multi-Properties Committee Member in Program Committee within the VMCAI-track
Marco GuarnieriGuarnieri, Marco ETH Zurich, Switzerland Contract-aware Secure Compilation (short talk)
Marco GuarnieriGuarnieri, Marco IMDEA Software InstituteSpain Committee Member in Program Committee within the PriSC-track
Rachid GuerraouiGuerraoui, Rachid EPFL The road to a Universal Internet Machine (Demystifying Blockchain Protocols)
Christophe GuillonGuillon, Christophe STMicroelectronics Secure Optimization Through Opaque Observations
Wenxuan GuoGuo, Wenxuan Shanghai Jiao Tong University Effective Heuristics Learning via Program Synthesis
Aarti GuptaGupta, Aarti Princeton UniversityUnited States Unbounded Procedure Summaries from Bounded Environments Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
Gopal GuptaGupta, Gopal Committee Member in Programme Committee within the PADL-track
Arie GurfinkelGurfinkel, Arie University of WaterlooCanada Committee Member in Program Committee within the VMCAI-track
John GustafsonGustafson, John National University of Singapore An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
Jens Oliver GutsfeldGutsfeld, Jens Oliver Westfälische Wilhelm-Universität Münster (WWU), Germany Automata and Fixpoints for Asynchronous Hyperproperties
Armaël GuéneauGuéneau, Armaël Aarhus University Toward Complete Stack Safety for Capability Machines Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
H Sebastian HackHack, Sebastian Saarland University, Germany An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
William T. HallahanHallahan, William T. Yale University Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Pat HanrahanHanrahan, Pat Stanford University, USA Hardware DSLs
Michael HanusHanus, Michael Kiel UniversityGermany Lightweight Declarative Server-Side Web Programming
Max W. HaslbeckHaslbeck, Max W. University of Innsbruck An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR
Ichiro HasuoHasuo, Ichiro National Institute of Informatics, JapanJapan Think Abstractly, Work Concretely Committee Member in Program Committee within the POPL -track Invited Speaker in Invited Speakers within the PLMW-track
Daniel HausmannHausmann, Daniel Friedrich-Alexander-Universität Erlangen-NürnbergGermany Committee Member in Artifact Evaluation Committee within the VMCAI-track
Matthias HeizmannHeizmann, Matthias University of Freiburg, GermanyGermany Verification of Concurrent Programs Using Petri Net Unfoldings Committee Member in Program Committee within the POPL -track
Joseph M. HellersteinHellerstein, Joseph M. Toward a Programmable Cloud: CALM Foundations and Open Challenges
Fritz HengleinHenglein, Fritz Department of Computer Science, University of Copenhagen (DIKU) and Deon DigitalDenmark Local Arrangements Chair in Organizing Committee for POPL 2021 Committee Member in Steering Committee within the PEPM-track Conference Co-Chair in Organizing Committee within the VMCAI-track
Troels HenriksenHenriksen, Troels University of Copenhagen, DenmarkDenmark Artifact Evaluation Co-Chair in Organizing Committee within the VMCAI-track
Manuel HermenegildoHermenegildo, Manuel IMDEA Software Institute and T.U. of MadridSpain Committee Member in Steering Committee within the PEPM-track
Thomas HerrmannHerrmann, Thomas Department of Computer Science, Aalborg University A Type-Safe Structure Editor Calculus
Karine HeydemannHeydemann, Karine Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6 Secure Optimization Through Opaque Observations
Michael HicksHicks, Michael University of Maryland at College Park A Verified Optimizer for Quantum Circuits Committee Member in Steering Committee within the PriSC-track
Kesha HietalaHietala, Kesha University of Maryland A Verified Optimizer for Quantum Circuits
Jonas Kastberg HinrichsenHinrichsen, Jonas Kastberg IT University of CopenhagenDenmark Machine-Checked Semantic Session Typing
Andrew K. HirschHirsch, Andrew K. Max Planck Institute for Software SystemsGermany Giving Semantics to Program-Counter Labels via Secure Effects
Jochen HoenickeHoenicke, Jochen University of FreiburgGermany Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Workshops Co-Chair in Organizing Committee for POPL 2021 A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis Modeling and Analyzing Evaluation Cost of CUDA Kernels Committee Member in Tutorials Evaluation Committee within the POPL TutorialFest-track
Steven HoltzenHoltzen, Steven University of California at Los Angeles Committee Member in Program Committee within the LAFI-track
Štěpán HolubHolub, Štěpán Charles UniversityCzech Republic Formalization of Combinatorics on Words in Isabelle/HOL
Kuen-Bang Hou (Favonia)Hou (Favonia), Kuen-Bang University of Minnesota, Twin CitiesUnited States Panel: Doing Research in PL
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany Session Chair of Invited Talk (part of CPP ) Nanopass Back-Translation of Multiple Traces for Secure Compilation Proofs Chairs' report and community meeting Co-chair in Program Committee within the CPP -track PC and Conference Co-Chair in Organization Committee within the CPP -track Steering Committee Member in Steering Committee within the CPP -track Committee Member in Steering Committee within the PriSC-track
Justin HsuHsu, Justin University of Wisconsin-Madison, USAUnited States Session Chair of Session 0 (part of PLMW) Session Chair of Monday Panel (part of PLMW) A Pre-Expectation Calculus for Probabilistic Sensitivity Co-chair in Organizing Committee within the PLMW-track
Jason Z.S. HuHu, Jason Z.S. McGill UniversityCanada Formalizing Category Theory in Agda
Qinheping HuHu, Qinheping University of Wisconsin-Madison, USA Semantics-Guided Synthesis
Zhenjiang HuHu, Zhenjiang Peking University Committee Member in Steering Committee within the PEPM-track
Andreas HumenbergerHumenberger, Andreas Vienna University of Technology Algebra-based Synthesis of Loops and their Invariants
Shih-Han HungHung, Shih-Han University of Maryland, USA A Verified Optimizer for Quantum Circuits
Chung-Kil HurHur, Chung-Kil Seoul National University, South Korea Panel Discussion 1: Choosing Research Topics Committee Member in Program Committee within the CPP -track Committee Member in Program Committee within the PriSC-track
Sander HuyghebaertHuyghebaert, Sander Vrije Universiteit Brussel Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Hans HüttelHüttel, Hans Department of Computer Science, Aalborg UniversityDenmark A Type-Safe Structure Editor Calculus
I Atsushi IgarashiIgarashi, Atsushi Kyoto University, JapanJapan Panel Discussion 3: Work/Life Balance Panel Discussion 4: Finding Friends and Collaborators in Academia Committee Member in Steering Committee within the PEPM-track
Grant IraciIraci, Grant University at BuffaloUnited States Synchronous Message-Passing with Priority
Chiaki IshioIshio, Chiaki Ochanomizu UniversityJapan A Functional Abstraction of Typed Trails
Anastasiia IzychevaIzycheva, Anastasiia Technical University of MunichGermany Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
J Nouraldin JaberJaber, Nouraldin Purdue University, USAUnited States Committee Member in Artifact Evaluation Committee within the VMCAI-track
Bart JacobsJacobs, Bart imec-DistriNet, Dept. CS, KU LeuvenBelgium Committee Member in Program Committee within the POPL -track
Jules JacobsJacobs, Jules Radboud University Nijmegen Paradoxes of probabilistic programming
Koen JacobsJacobs, Koen KU Leuven Fully Abstract from Static to Gradual
Maxime JacqueminJacquemin, Maxime CEA LIST, FranceFrance Runtime Abstract Interpretation for Numerical Accuracy and Robustness
Khurram A. JaferyJafery, Khurram A. University of British Columbia Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
Arvid JakobssonJakobsson, Arvid Nomadic Labs Formally Verified Decentralized Exchange with Mi-Cho-Coq
Alan JeffreyJeffrey, Alan RobloxUnited States Games Programming Languages BoF Session
Somesh JhaJha, Somesh University of Wisconsin, MadisonUnited States Committee Member in Program Committee within the POPL -track
Ranjit JhalaJhala, Ranjit University of California at San Diego Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Limin JiaJia, Limin Carnegie Mellon UniversityUnited States Connecting Information Flow Types to Runtime Monitors via Gradual Typing Netter: Probabilistic, Stateful Network Models Invited Speaker in Invited Speakers within the PLMW-track
Moa JohanssonJohansson, Moa Chalmers University of TechnologySweden Committee Member in Program Committee within the CPP -track
Jeremy JohnsonJohnson, Jeremy Drexel University, USA Verification of Algorithm and Code Generation for Signal Transforms
Matthew J. JohnsonJohnson, Matthew J. Google BrainUnited States Decomposing reverse-mode automatic differentiation
Eddie JonesJones, Eddie University of BristolUnited Kingdom Intensional Datatype Refinement
Saurabh JoshiJoshi, Saurabh IIT HyderabadIndia GPURepair: Automated Repair of GPU Kernels
Jacques-Henri JourdanJourdan, Jacques-Henri Universersité Paris Saclay, CNRS, LRIFrance Committee Member in Program Committee within the CoqPL-track
Jaehwang JungJung, Jaehwang KAIST, South Korea Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ralf JungJung, Ralf MPI-SWSGermany [T4] Iris – A Modular Foundation for Higher-Order Concurrent Separation Logic
K Konstantinos KallasKallas, Konstantinos University of Pennsylvania Data-Parallel Shell Scripting Committee Member in Artifact Evaluation Committee within the VMCAI-track
Benjamin Lucien KaminskiKaminski, Benjamin Lucien RWTH Aachen University, GermanyGermany Relatively Complete Verification of Probabilistic Programs A Pre-Expectation Calculus for Probabilistic Sensitivity
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom Committee Member in Steering Committee within the LAFI-track
Marius KampKamp, Marius Friedrich-Alexander University Erlangen-NürnbergGermany Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
Jeehoon KangKang, Jeehoon KAISTSouth Korea Artifact Evaluation Co-Chair in Organizing Committee for POPL 2021 Panel: Doing Research in PL Panel Discussion 4: Finding Friends and Collaborators in Academia Committee Member in Program Committee within the POPL -track Panelist in Panelists within the PLMW-track Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tobias KappéKappé, Tobias Cornell University Monadic Second-Order Logic and Pomset Languages
Toghrul KarimovKarimov, Toghrul Max Planck Institute for Software Systems Deciding ω-Regular Properties on Linear Recurrence Sequences
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Relatively Complete Verification of Probabilistic Programs A Pre-Expectation Calculus for Probabilistic Sensitivity
Guy KatzKatz, Guy Hebrew UniversityIsrael Committee Member in Program Committee within the VMCAI-track
Ilya KaysinKaysin, Ilya National Research University Higher School of Economics, JetBrains ResearchRussia PerSeVerE: Persistency Semantics for Verification under Ext4
Chantal KellerKeller, Chantal LRI, Univ. Paris-SudFrance A Coq Formalization of Data Provenance
Edon KelmendiKelmendi, Edon University of Oxford Deciding ω-Regular Properties on Linear Recurrence Sequences
Artem KhyzhaKhyzha, Artem Tel Aviv University Taming x86-TSO Persistency
Rami Gökhan KıcıKıcı, Rami Gökhan University of California at San Diego, USA Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Eunhee KimKim, Eunhee 2e Consulting Corp.South Korea A Design of GPU-Based Quantitative Model Checking
Jinwoo KimKim, Jinwoo University of Wisconsin-Madison Semantics-Guided Synthesis
Zachary KincaidKincaid, Zachary Princeton University, USA Committee Member in Program Committee within the POPL -track
Dominik KirstKirst, Dominik Saarland UniversityGermany The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq
Gerwin KleinKlein, Gerwin CSIRO's Data61 and UNSW SydneyAustralia Steering Committee Member in Steering Committee within the CPP -track
Andrei KlimovKlimov, Andrei Keldysh Institute of Applied Mathematics of Russian Academy of SciencesRussia Committee Member in Program Committee within the PEPM-track
Dominik KlumppKlumpp, Dominik University of FreiburgGermany Verification of Concurrent Programs Using Petri Net Unfoldings
Hsiang-Shang ‘Josh’ KoKo, Hsiang-Shang ‘Josh’ Institute of Information Science, Academia Sinica, Taiwan Web Chair in Organizing Committee for POPL 2021 Committee Member in Steering Committee within the PEPM-track
Naoki KobayashiKobayashi, Naoki University of Tokyo, JapanJapan Counterexample Generation for Program Verification based on Ownership Refinement Types Committee Member in Program Committee within the POPL -track
Alexander KogtenkovKogtenkov, Alexander Schaffhausen Institute of Technology, SwitzerlandRussia Mechanically-checked soundness of type-based null safety
Michalis KokologiannakisKokologiannakis, Michalis MPI-SWS, GermanyGreece PerSeVerE: Persistency Semantics for Verification under Ext4
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University, UK Session Chair of AI and Machine Learning (part of CPP ) Session Chair of Applications of Declarative Languages (part of PADL) Committee Member in Program Committee within the CPP -track Committee Member in Programme Committee within the PADL-track
Igor KonnovKonnov, Igor Informal Systems IncAustria Eliminating Message Counters in Synchronous Threshold Automata Specification and model checking of Tendermint consensus in TLA+
Till KortenKorten, Till TU DresdenGermany Formal Semantics and Verification of Network Based Biocomputation Circuits
Eric KoskinenKoskinen, Eric Stevens Institute of TechnologyUnited States Decomposing Data Structure Commutativity Proofs with mn-Differencing
Nikolai KosmatovKosmatov, Nikolai Thales Research and TechnologyFrance Runtime Abstract Interpretation for Numerical Accuracy and Robustness
Adrien KoutsosKoutsos, Adrien INRIA Paris High-Assurance Cryptography in the Spectre Era
Angeliki Koutsoukou-ArgyrakiKoutsoukou-Argyraki, Angeliki University of Cambridge, Department of Computer Science and TechnologyUnited Kingdom Committee Member in Program Committee within the CPP -track
Laura KovacsKovacs, Laura Vienna University of Technology (TU Wien)Austria Algebra-based Synthesis of Loops and their Invariants Committee Member in Program Committee within the POPL -track Committee Member in Invited Speakers within the VMCAI-track
Dexter KozenKozen, Dexter Cornell UniversityUnited States Committee Member in Program Committee within the POPL -track
Anastasiya Kravchuk-KirilyukKravchuk-Kirilyuk, Anastasiya Harvard UniversityUnited States The B+-tree Index as a Verified Software Unit
Robbert KrebbersKrebbers, Robbert Radboud University Nijmegen Machine-Checked Semantic Session Typing Intrinsically Typed Compilation with Nameless Labels
Shriram KrishnamurthiKrishnamurthi, Shriram Brown University, United States SIGPLAN CARES SIGPLAN CARES
Neel KrishnaswamiKrishnaswami, Neel Computer Laboratory, University of Cambridge Transfinite Step-Indexing for Termination
Paul KrogmeierKrogmeier, Paul University of Illinois at Urbana-Champaign Deciding Accuracy of Differential Privacy Schemes
Hillel KuglerKugler, Hillel Bar Ilan UniversityIsrael Formal Semantics and Verification of Network Based Biocomputation Circuits
K Narayan KumarKumar, K Narayan Chennai Mathematical InstituteIndia Deciding Reachability under Persistent x86-TSO
Denis KuperbergKuperberg, Denis LIP, ENS de Lyon Cyclic Proofs, System T, and the Power of Contraction
YoungMin KwonKwon, YoungMin SUNY KoreaSouth Korea A Design of GPU-Based Quantitative Model Checking
Bettina KönighoferKönighofer, Bettina Committee Member in Artifact Evaluation Committee within the VMCAI-track
L Ori LahavLahav, Ori Tel Aviv University Student Research Competition Co-Chair in Organizing Committee for POPL 2021 Verifying Observational Robustness Against a C11-style Memory Model Taming x86-TSO Persistency Co-chair in Selection Committee within the POPL Student Research Competition-track
Stella LauLau, Stella MIT Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Olivier LaurentLaurent, Olivier CNRS & ENS LyonFrance An Anti-Locally-Nameless Approach to Formalizing Quantifiers
Théo LaurentLaurent, Théo INRIA Paris Refining Dependent Type Theory Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Mikkel Korup LauridsenLauridsen, Mikkel Korup Department of Computer Science, Aalborg University A Type-Safe Structure Editor Calculus
Julia LawallLawall, Julia Inria Program Manipulation of C Code: From Partial Evaluation to Semantic Patches for the Linux Kernel
Marijana LazicLazic, Marijana Technical University of MunichGermany A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
Quang Loc LeLe, Quang Loc University College London, UKUnited Kingdom Compositional Satisfiability Solving in Separation Logic
Woosuk LeeLee, Woosuk Hanyang University, South Korea Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis
Yunjeong LeeLee, Yunjeong Committee Member in Artifact Evaluation Committee within the VMCAI-track
Thomas LembergerLemberger, Thomas LMU MunichGermany Committee Member in Artifact Evaluation Committee within the VMCAI-track
Meven Lennon-BertrandLennon-Bertrand, Meven Inria – LS2N, Université de NantesFrance Gradualizing the Calculus of Inductive Constructions
Xavier LeroyLeroy, Xavier Collège de FranceFrance Verified Code Generation for the Polyhedral Model Committee Member in Program Committee within the PriSC-track
Alexander K. LewLew, Alexander K. Massachusetts Institute of Technology, USAUnited States On the Automatic Derivation of Importance Samplers from Pairs of Probabilistic Programs
Nicholas V. LewchenkoLewchenko, Nicholas V. University of Colorado BoulderUnited States Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Robert Y. LewisLewis, Robert Y. Vrije Universiteit AmsterdamNetherlands Formalizing the Ring of Witt Vectors Committee Member in Program Committee within the CPP -track
Yao LiLi, Yao University of PennsylvaniaUnited States Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yuanbo LiLi, Yuanbo Georgia Institute of Technology, USA On the Complexity of Bidirected Interleaved Dyck-Reachability
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 High-Assurance Cryptography in the Spectre Era
Yuliya LierlerLierler, Yuliya University of Nebraska SMT-based Constraint Answer Set Solver EZSMT
Paul LietarLietar, Paul Imperial College London Topological assertions for flexible isolation
Jay P. LimLim, Jay P. Rutgers University, USA An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
Jannis LimpergLimperg, Jannis Vrije Universiteit AmsterdamNetherlands A Novice-Friendly Induction Tactic for Lean
Sam LindleyLindley, Sam Heriot-Watt University, UK / The University of Edinburgh, UKUnited Kingdom Session Chair of Keynote 1 (part of PEPM) Session Chair of Keynote 3 (part of PEPM) Panel: Doing Research in PL Committee Member in Steering Committee within the PEPM-track Co-chair in Organizing Committee within the PEPM-track Panelist in Panelists within the PLMW-track
Andreas LochbihlerLochbihler, Andreas Digital AssetSwitzerland Session Chair of Security, Blockchains, and Smart Contracts (part of CPP ) A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers Committee Member in Program Committee within the CPP -track
Alexander LochmannLochmann, Alexander University of Innsbruck A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Fosco LoregianLoregian, Fosco Tallinn University of Technology Functorial Semantics for Partial Theories
Daniël LouwrinkLouwrink, Daniël University of Amsterdam Machine-Checked Semantic Session Typing
Petr LozovLozov, Petr Sain Petersburg State University, SPbGU Efficient Fair Conjunction for Structurally-Recursive Relations Certified Semantics for miniKanren
Kangjie LuLu, Kangjie University of Minnesota Cross-Architecture Testing for Compiler-Introduced Security Bugs
Kenny Zhuo Ming LuLu, Kenny Zhuo Ming ISTD, Singapore University of Technology and DesignSingapore Control Flow Obfuscation for Featherweight Java using Continuation Passing
Steven LyubomirskyLyubomirsky, Steven University of Washington, USAUnited States Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Andres LöhLöh, Andres Well-Typed LLP [T2] Liquid Haskell: Refinement Type Checker for Haskell
Andreas LööwLööw, Andreas Chalmers University of Technology Lutsig: A Verified Verilog Compiler for Verified Circuit Development
M Jesus M. Almendros-JimenezM. Almendros-Jimenez, Jesus Universidad de AlmeriaSpain Declarative Debugging of XML Queries
Dougal MaclaurinMaclaurin, Dougal Google Research Session Chair of Session 2 (part of LAFI) Decomposing reverse-mode automatic differentiation Committee Member in Organizing Committee within the LAFI-track
Enrico MagnagoMagnago, Enrico Fondazione Bruno KesslerItaly Proving the existence of fair paths in infinite state systems
Assia MahboubiMahboubi, Assia INRIAFrance Steering Committee Member in Steering Committee within the CPP -track Co-chair in Organizing Committee within the CoqPL-track
Kenji MaillardMaillard, Kenji Inria Nantes & University of Chile Gradualizing the Calculus of Inductive Constructions Committee Member in Program Committee within the CoqPL-track
Rupak MajumdarMajumdar, Rupak MPI-SWS Numbers, Logic, and Decidability Results for Cyber-Physical Systems Lassie: HOL4 Tactics by Example Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs Committee Member in Program Committee within the POPL -track Invited Speaker in Invited Speakers within the PLMW-track Committee Member in Program Committee within the VMCAI-track
Carol MakMak, Carol University of Oxford Binary Tree Hamiltonian Monte Carlo Committee Member in Program Committee within the LAFI-track
Petar MaksimovićMaksimović, Petar Imperial College London, UK Committee Member in Program Committee within the CPP -track
Sharad MalikMalik, Sharad Princeton UniversityUnited States Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
Louis MandelMandel, Louis IBM Research, USA Committee Member in Program Committee within the LAFI-track
Vikash K. MansinghkaMansinghka, Vikash K. MIT On the Automatic Derivation of Importance Samplers from Pairs of Probabilistic Programs Genify.jl: Transforming Julia into Gen to enable programmable inference
William ManskyMansky, William University of Illinois at ChicagoUnited States Session Chair of Program Logics (part of CPP ) Committee Member in Program Committee within the CPP -track
Bing MaoMao, Bing Nanjing University Cross-Architecture Testing for Compiler-Introduced Security Bugs
Luc MarangetMaranget, Luc Inria ParisFrance Committee Member in Program Committee within the POPL -track
Roy MargalitMargalit, Roy Tel Aviv University, Israel Verifying Observational Robustness Against a C11-style Memory Model
Ognjen MarićMarić, Ognjen Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
Eric Mark MartinMartin, Eric Mark Stanford On the Semantic Expressiveness of Recursive Types
Guido MartínezMartínez, Guido CIFASIS-CONICET, ArgentinaArgentina Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Christoph MathejaMatheja, Christoph ETH Zurich Relatively Complete Verification of Probabilistic Programs A Pre-Expectation Calculus for Probabilistic Sensitivity
Anders Alnor MathiasenMathiasen, Anders Alnor Aarhus University The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
Umang MathurMathur, Umang University of Illinois at Urbana-ChampaignUnited States Optimal Prediction of Synchronization-Preserving Races [T3] Dynamic Data-Race Prediction : Fundamentals, Theory and Practice
Damiano MazzaMazza, Damiano CNRSFrance Automatic Differentiation in PCF
Aastha MehtaMehta, Aastha MPI-SWS, Germany and University of British Columbia, Canada Session Chair of Secure compilers & cryptography (part of PriSC) Committee Member in Program Committee within the PriSC-track
Simon MeierMeier, Simon Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
Roland MeyerMeyer, Roland TU Braunschweig Committee Member in Program Committee within the POPL -track
Jesse MichelMichel, Jesse Massachusetts Institute of Technology λS: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
Aart MiddeldorpMiddeldorp, Aart University of Innsbruck A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Dale MillerMiller, Dale INRIA Saclay and LIXFrance Steering Committee Member in Steering Committee within the CPP -track
Mikkel MiloMilo, Mikkel Concordium Blockchain Research Center, Aarhus University Extracting Smart Contracts Tested and Verified in Coq
Zarko MilosevicMilosevic, Zarko Informal Systems Specification and model checking of Tendermint consensus in TLA+
Edgar MinasyanMinasyan, Edgar Princeton University Parametric Inversion of Non-Invertible Programs
Antoine MinéMiné, Antoine Sorbonne UniversitéFrance Committee Member in Program Committee within the VMCAI-track
Victor Cacciari MiraldoMiraldo, Victor Cacciari DFINITY Foundation Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Fabian MitterwallnerMitterwallner, Fabian University of Innsbruck A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Torben MogensenMogensen, Torben DIKU, University of CopenhagenDenmark Session Chair of Session 5 (part of PEPM) Session Chair of Session 1 (part of PEPM) Session Chair of Keynote 2 (part of PEPM) Committee Member in Steering Committee within the PEPM-track Co-chair in Organizing Committee within the PEPM-track
Sidi Mohamed BeillahiMohamed Beillahi, Sidi IRIF - Université de ParisFrance Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Mark MoirMoir, Mark Oracle Labs, New Zealand Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Simon MollMoll, Simon NEC Deutschland An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
Raphaël MonatMonat, Raphaël Sorbonne Université — LIP6France Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jean-François MoninMonin, Jean-François Verimag Developing and certifying Datalog optimizations in Coq/MathComp
David MonniauxMonniaux, David Grenoble Alps University / CNRS / Grenoble INP / VERIMAG Committee Member in Program Committee within the POPL -track
José MoralesMorales, José IMDEA Software Institute Session Chair of Keynote 2 (part of PADL) Co-chair in Programme Chairs within the PADL-track Co-chair in Programme Committee within the PADL-track
David MorejonMorejon, David Massachusetts Institute of Technology Parametric Inversion of Non-Invertible Programs
J. Garrett MorrisMorris, J. Garrett University of Kansas, USAUnited States Committee Member in Program Committee within the PEPM-track
Greg MorrisettMorrisett, Greg Cornell TechUnited States Panel: Doing Research in PL Panelist in Panelists within the PLMW-track
Cameron MoyMoy, Cameron Northeastern UniversityUnited States Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
Gautam MudugantiMuduganti, Gautam IIT HyderabadIndia GPURepair: Automated Repair of GPU Kernels
Stefan K. MullerMuller, Stefan K. Illinois Institute of TechnologyUnited States Modeling and Analyzing Evaluation Cost of CUDA Kernels
Charlie MurphyMurphy, Charlie Princeton UniversityUnited States Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Alnis MurtoviMurtovi, Alnis TU DortmundGermany Generative Program Analysis and Beyond: The Power of Domain-Specific Languages
Andrew MyersMyers, Andrew Cornell University Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology A Minimalistic Verified Bootstrapped Compiler (Proof Pearl) Steering Committee Member in Steering Committee within the CPP -track
Anders MörtbergMörtberg, Anders Department of Mathematics, Stockholm UniversitySweden Internalizing Representation Independence with Univalence Committee Member in Program Committee within the CPP -track
Rasmus Ejlers MøgelbergMøgelberg, Rasmus Ejlers IT University of CopenhagenDenmark Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
Markus Müller-OlmMüller-Olm, Markus University of MünsterGermany Automata and Fixpoints for Asynchronous Hyperproperties
N Santosh NagarakatteNagarakatte, Santosh Rutgers University, USA An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants Committee Member in Steering Committee within the PriSC-track Committee Member in Program Committee within the PriSC-track
Kedar NamjoshiNamjoshi, Kedar Nokia Bell LabsUnited States A Self-Certifying Compilation Framework for WebAssembly Committee Member in Program Committee within the POPL -track
Chandrakana NandiNandi, Chandrakana University of Washington, USAUnited States egg: Fast and Extensible Equality Saturation
Aleksandar NanevskiNanevski, Aleksandar IMDEA Software Institute On Algebraic Abstractions for Concurrent Separation Logics
Mehdi NaouarNaouar, Mehdi University of FreiburgGermany Verification of Concurrent Programs Using Petri Net Unfoldings
Monal NarasimhamurthyNarasimhamurthy, Monal University of Colorado, BoulderUnited States Committee Member in Artifact Evaluation Committee within the VMCAI-track
Enrique NaudonNaudon, Enrique BloombergUnited States Putting gradual types to work
Jorge A. NavasNavas, Jorge A. SRI InternationalUnited States Committee Member in Program Committee within the VMCAI-track
Luca NegriniNegrini, Luca Ca’ Foscari University of Venice, Julia S.r.l.Italy Twinning automata and regular expressions for string static analysis
Antonina NepeivodaNepeivoda, Antonina Program Systems Institute of RAS, RussiaRussia Committee Member in Program Committee within the PEPM-track
Robert NessNess, Robert Altdeep.aiUnited States Committee Member in Program Committee within the LAFI-track
Chad NesterNester, Chad Tallinn University of Technology Functorial Semantics for Partial Theories
Thanh-Toan NguyenNguyen, Thanh-Toan National University of SingaporeSingapore Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
Phúc C. NguyễnNguyễn, Phúc C. Google Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
Newton NiNi, Newton Cornell University Petr4: Formal Foundations for P4 Data Planes
Phoebe NicholsNichols, Phoebe Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
Dan Nicolau Jr.Nicolau Jr., Dan Molecular SenseUnited Kingdom Formal Semantics and Verification of Network Based Biocomputation Circuits
Benjamin Barslev NielsenNielsen, Benjamin Barslev Aarhus University Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jakob Botsch NielsenNielsen, Jakob Botsch Concordium Blockchain Research Center, Aarhus University Extracting Smart Contracts Tested and Verified in Coq
Abel NietoNieto, Abel Aarhus UniversityCanada Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Henrik NilssonNilsson, Henrik University of Nottingham, UK Committee Member in Programme Committee within the PADL-track
Tobias NipkowNipkow, Tobias Technische Universität München Invited Talk: Teaching Algorithms and Data Structures with a Proof Assistant Steering Committee Member in Steering Committee within the CPP -track
James NobleNoble, James Victoria University of WellingtonNew Zealand Panel Discussion 2: Improving Peer Review Panel Discussion 1: Choosing Research Topics
Michael NorrishNorrish, Michael Data61, CSIRO & ANUAustralia On the Formalisation of Kolmogorov Complexity
Andreas NuytsNuyts, Andreas KU Leuven, BelgiumBelgium A Categorical Approach to Secure Compilation (and others things) (short talk)
O Sabine OechsnerOechsner, Sabine Aarhus University Formalising MPC-in-the-head-based zero-knowledge
Reed OeiOei, Reed University of Illinois at Urbana-ChampaignUnited States Psamathe: A DSL with Flows for Safe Blockchain Assets (extended abstract)
Christoph OhremOhrem, Christoph Westfälische Wilhelms-Universität Münster (WWU), Germany Automata and Fixpoints for Asynchronous Hyperproperties
Tiago OliveiraOliveira, Tiago University of Porto (FCUP) and INESC TEC High-Assurance Cryptography in the Spectre Era
C.-H. Luke OngOng, C.-H. Luke University of OxfordUnited Kingdom Binary Tree Hamiltonian Monte Carlo
Dominic OrchardOrchard, Dominic University of Kent, UKUnited Kingdom Session Chair of Foundations and Programming Concepts (part of PADL) Session Chair of Keynote 1 (part of PADL) Co-chair in Programme Chairs within the PADL-track Co-chair in Programme Committee within the PADL-track
Abdelraouf OuadjaoutOuadjaout, Abdelraouf Sorbonne UniversitéFrance Committee Member in Artifact Evaluation Committee within the VMCAI-track
Joël OuaknineOuaknine, Joël Max Planck Institute for Software Systems and University of Oxford Deciding ω-Regular Properties on Linear Recurrence Sequences
Iman OwliaieOwliaie, Iman Department of Computer Science, Aalborg University A Type-Safe Structure Editor Calculus
Sam OwreOwre, Sam SRI InternationalUnited States Committee Member in Program Committee within the CPP -track
Alex OzdemirOzdemir, Alex Stanford High-level high-speed high-assurance crypto
P Sumit PadhiyarPadhiyar, Sumit Indian Institue Of Technology, MadrasIndia ConFuzz: Coverage-guided Property Fuzzing for Event-driven Programs
Oded PadonPadon, Oded VMware ResearchUnited States Committee Member in Program Committee within the VMCAI-track
Michele PaganiPagani, Michele IRIF - Université de ParisFrance Automatic Differentiation in PCF
Karl PalmskogPalmskog, Karl KTH Royal Institute of TechnologySweden Committee Member in Program Committee within the CPP -track
Pavel PanchekhaPanchekha, Pavel University of UtahUnited States Artifact Evaluation Co-Chair in Organizing Committee for POPL 2021 egg: Fast and Extensible Equality Saturation Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jovanka PantovićPantović, Jovanka University of Novi SadSerbia Precise Subtyping for Asynchronous Multiparty Sessions
Zoe ParaskevopoulouParaskevopoulou, Zoe Princeton UniversityUnited States Committee Member in Program Committee within the PriSC-track
Samwise ParkinsonParkinson, Samwise Cornell University Petr4: Formal Foundations for P4 Data Planes
Corina S. PasareanuPasareanu, Corina S. Carnegie Mellon University Silicon Valley, NASA Ames Research Center Committee Member in Program Committee within the VMCAI-track
Adam PaszkePaszke, Adam Google ResearchPoland Decomposing reverse-mode automatic differentiation
Marco PatrignaniPatrignani, Marco Stanford University, USA / CISPA, Germany Session Chair of Formal analysis & proof techniques (part of PriSC) Contract-aware Secure Compilation (short talk) On the Semantic Expressiveness of Recursive Types
Zvonimir PavlinovicPavlinovic, Zvonimir Google, USAUnited States Data Flow Refinement Type Inference
Andreas PavlogiannisPavlogiannis, Andreas Aarhus UniversityDenmark Optimal Prediction of Synchronization-Preserving Races The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis [T3] Dynamic Data-Race Prediction : Fundamentals, Theory and Practice Committee Member in Program Committee within the POPL -track
Tobias PaxianPaxian, Tobias University of FreiburgGermany On Pre- and Inprocessing for Weighted MaxSAT
Jennifer PaykinPaykin, Jennifer Galois, Inc.United States Committee Member in Program Committee within the PriSC-track
Barak A. PearlmutterPearlmutter, Barak A. Maynooth UniversityIreland [T1] The Current State of Automatic Differentiation
Hila PelegPeleg, Hila University of California at San Diego Panel: Navigating PhD studies Committee Member in Selection Committee within the POPL Student Research Competition-track Panelist in Panelists within the PLMW-track
Yuanfeng PengPeng, Yuanfeng Google Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yuxiang PengPeng, Yuxiang University of Maryland Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra
Mário PereiraPereira, Mário NOVA LINCS & Nova School of Sciences and Tecnhology Cameleer: a Deductive Verification Tool for OCaml
Vasily PestunPestun, Vasily IBM Research; IHES CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Christina PetersonPeterson, Christina University of Central FloridaUnited States Concurrent Correctness in Vector Space
Rudy PetersonPeterson, Rudy Cornell University Petr4: Formal Foundations for P4 Data Planes
Simon Peyton JonesPeyton Jones, Simon Microsoft, UK Committee Member in Program Committee within the POPL -track
Frank PfenningPfenning, Frank Carnegie Mellon University, USA Committee Member in Program Committee within the POPL -track
Loc PhamPham, Loc New Mexico State UniversityUnited States A Logic Programming Approach to Regression Based Repair of Incorrect Initial Belief States
Michael PhilippsenPhilippsen, Michael Friedrich-Alexander University Erlangen-Nürnberg (FAU)Germany Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
David PichardiePichardie, David Univ Rennes, ENS Rennes, IRISAFrance Formally Verified Speculation and Deoptimization in a JIT Compiler
Lauren PickPick, Lauren Princeton UniversityUnited States Unbounded Procedure Summaries from Bounded Environments
Frank PiessensPiessens, Frank KU Leuven A Categorical Approach to Secure Compilation (and others things) (short talk)
Laureline PinaultPinault, Laureline LIP, ENS de Lyon Cyclic Proofs, System T, and the Power of Contraction
Ruzica PiskacPiskac, Ruzica Yale University, USA Workshops Co-Chair in Organizing Committee for POPL 2021 Committee Member in Tutorials Evaluation Committee within the POPL TutorialFest-track
Clément Pit-ClaudelPit-Claudel, Clément Massachusetts Institute of Technology, USA An experience report on writing usable DSLs in Coq Automated Synthesis of Verified Firewalls
Gordon PlotkinPlotkin, Gordon Google The Selection Monad and Decision-Making Languages
Adam PocockPocock, Adam Oracle LabsUnited States Committee Member in Program Committee within the LAFI-track
Andreas PodelskiPodelski, Andreas University of Freiburg, GermanyGermany General Chair in Organizing Committee for POPL 2021 Verification of Concurrent Programs Using Petri Net Unfoldings
Nadia PolikarpovaPolikarpova, Nadia University of California at San Diego Committee Member in Program Committee within the POPL -track
Nika PonaPona, Nika Digamma.ai How to verify an ASN.1 Protocol C-language Stack in Coq?
Enrico PontelliPontelli, Enrico New Mexico State University A Logic Programming Approach to Regression Based Repair of Incorrect Initial Belief States Committee Member in Programme Committee within the PADL-track
Andrei PopescuPopescu, Andrei University of SheffieldUnited Kingdom Session Chair of Invited Talk (part of CPP ) Chairs' report and community meeting Co-chair in Program Committee within the CPP -track PC Co-Chair in Organization Committee within the CPP -track
François PottierPottier, François Inria, FranceFrance A Separation Logic for Effect Handlers
Damien PousPous, Damien CNRS Cyclic Proofs, System T, and the Power of Contraction Committee Member in Program Committee within the CPP -track
Pierre PradicPradic, Pierre Oxford University Generating Collection Transformations from Proofs
Matija PretnarPretnar, Matija University of Ljubljana, SloveniaSlovenia Asynchronous Effects
Swarn PriyaPriya, Swarn Purdue University High-Assurance Cryptography in the Spectre Era
Ivan ProkićProkić, Ivan University of Novi SadSerbia Precise Subtyping for Asynchronous Multiparty Sessions
Jonathan ProtzenkoProtzenko, Jonathan Microsoft Research, RedmondUnited States Session Chair of Formal analysis & proof techniques (part of PriSC) Committee Member in Steering Committee within the PriSC-track Committee Member in Program Committee within the PriSC-track
George PîrleaPîrlea, George National University of Singapore, Singapore Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Q Xuanrui QiQi, Xuanrui Nagoya UniversityJapan Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
R Azalea RaadRaad, Azalea Imperial College London Student Research Competition Co-Chair in Organizing Committee for POPL 2021 Session Chair of Session 1 (part of PLMW) Session Chair of Session 3 (part of PLMW) PerSeVerE: Persistency Semantics for Verification under Ext4 Co-chair in Selection Committee within the POPL Student Research Competition-track Co-chair in Organizing Committee within the PLMW-track Committee Member in Program Committee within the VMCAI-track
Chris RackauckasRackauckas, Chris MIT Bayesian Neural Ordinary Differential Equations
Gabriel RadanneRadanne, Gabriel InriaFrance Committee Member in Program Committee within the PEPM-track
Arjun RadhakrishnaRadhakrishna, Arjun Microsoft Committee Member in Program Committee within the POPL -track
Alexey RadulRadul, Alexey Google Research Decomposing reverse-mode automatic differentiation
Pascal RaiolaRaiola, Pascal University of FreiburgGermany On Pre- and Inprocessing for Weighted MaxSAT
Vineet RajaniRajani, Vineet MPI-SPGermany A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
Tahina RamananandroRamananandro, Tahina Microsoft ResearchUnited States Committee Member in Program Committee within the CPP -track
Steven RamsayRamsay, Steven University of BristolUnited Kingdom Intensional Datatype Refinement
Robert RandRand, Robert University of ChicagoUnited States A Verified Optimizer for Quantum Circuits
Aseem RastogiRastogi, Aseem Microsoft ResearchIndia Panel Discussion 4: Finding Friends and Collaborators in Academia Committee Member in Program Committee within the POPL -track
Antonio RavaraRavara, Antonio Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCSPortugal Cameleer: a Deductive Verification Tool for OCaml
Avraham RavivRaviv, Avraham Bar Ilan UniversityIsrael Formal Semantics and Verification of Network Based Biocomputation Circuits
Felix RechRech, Felix Saarland UniversityGermany The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq
Rolph RectoRecto, Rolph Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs
Thomas RepsReps, Thomas University of Wisconsin--Madison Semantics-Guided Synthesis On the Complexity of Bidirected Interleaved Dyck-Reachability Committee Member in Selection Committee within the POPL Student Research Competition-track
Alban ReynaudReynaud, Alban ENS Lyon A Practical Mode System for Recursive Definitions
Tamara RezkRezk, Tamara Inria, France High-Assurance Cryptography in the Spectre Era Committee Member in Steering Committee within the PriSC-track Committee Member in Program Committee within the PriSC-track
Lionel RiegRieg, Lionel Verimag Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Xavier RivalRival, Xavier INRIA/CNRS/ENS ParisFrance Session Chair of Abstract Interpretation (part of VMCAI) Committee Member in Program Committee within the VMCAI-track
Christine RizkallahRizkallah, Christine The University of MelbourneAustralia Panel Discussion 4: Finding Friends and Collaborators in Academia Panel Discussion 1: Choosing Research Topics
Tiark RompfRompf, Tiark Purdue University Committee Member in Steering Committee within the PEPM-track
Simona Ronchi Della RoccaRonchi Della Rocca, Simona University of TorinoItaly Intersection Types and (Positive) Almost-Sure Termination
Julian RosemannRosemann, Julian Saarland University, Saarland Informatics CampusGermany An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
Andreas RossbergRossberg, Andreas Dfinity StiftungGermany Committee Member in Program Committee within the PriSC-track
Arjen RouvoetRouvoet, Arjen Delft University of Technology Intrinsically Typed Compilation with Nameless Labels
Dmitry RozplokhasRozplokhas, Dmitry Saint Petersburg State University and JetBrains Research Certified Semantics for miniKanren
S William S. MosesS. Moses, William Massachusetts Institute of Technology Enzyme: High-Performance Automatic Differentiation of LLVM
Marcin SabokSabok, Marcin McGill University Probabilistic Programming Semantics for Name Generation
Amr SabrySabry, Amr Indiana UniversityEgypt A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
Mooly SagivSagiv, Mooly Tel Aviv University Learning the Boundary of Inductive Invariants
Prakash SaivasanSaivasan, Prakash The Institute of Mathematical Sciences, India Deciding Reachability under Persistent x86-TSO
Sriram SankaranarayananSankaranarayanan, Sriram University of Colorado, BoulderUnited States Committee Member in Program Committee within the POPL -track
Isao SasanoSasano, Isao Shibaura Institute of TechnologyJapan A Text-based Syntax Completion Method Using LR Parsing
Alceste ScalasScalas, Alceste Technical University of DenmarkDenmark Precise Subtyping for Asynchronous Multiparty Sessions
Gabriel SchererScherer, Gabriel INRIA SaclayFrance Session Chair of Session 2 (part of PLMW) A Practical Mode System for Recursive Definitions Co-chair in Organizing Committee within the PLMW-track Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tanja SchindlerSchindler, Tanja University of FreiburgGermany Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching Committee Member in Artifact Evaluation Committee within the VMCAI-track
Matthias SchmalzSchmalz, Matthias Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
David SchmidtSchmidt, David Kansas State UniversityUnited States Generative Program Analysis and Beyond: The Power of Domain-Specific Languages Invited Speaker in Invited Speakers within the VMCAI-track
Alan SchmittSchmitt, Alan InriaFrance Committee Member in Program Committee within the POPL -track
Anne-Kathrin SchmuckSchmuck, Anne-Kathrin MPI-SWSGermany Panel: Navigating PhD studies Panelist in Panelists within the PLMW-track
Bernhard ScholzScholz, Bernhard The University of Sydney Abstracting Large-scale Datalog: A Scalable Provenance Evaluation Strategy
Bernhard ScholzScholz, Bernhard University of Sydney, Australia Debugging Large-Scale Datalog: A Scalable Provenance Evaluation Strategy
Tom SchrijversSchrijvers, Tom KU Leuven Staged Effects and Handlers for Modular Languages with Abstraction
Ulrik Pagh SchultzSchultz, Ulrik Pagh University of Southern Denmark Committee Member in Steering Committee within the PEPM-track
Peter SchwabeSchwabe, Peter Max Planck Institute for Security and Privacy High-Assurance Cryptography in the Spectre Era
Claus SchätzleSchätzle, Claus University of FreiburgGermany Verification of Concurrent Programs Using Petri Net Unfoldings
Taro SekiyamaSekiyama, Taro National Institute of InformaticsJapan Committee Member in Program Committee within the POPL -track
Ilya SergeySergey, Ilya Yale-NUS College and National University of SingaporeSingapore Social Co-Chair in Organizing Committee for POPL 2021 Automated Repair of Heap-Manipulating Programs using Deductive Synthesis Panel Discussion 2: Improving Peer Review Panel Discussion 1: Choosing Research Topics Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the CPP -track Committee Member in Program Committee within the PriSC-track Committee Member in Program Committee within the VMCAI-track
Peter SewellSewell, Peter University of Cambridge Invited Talk: Underpinning the foundations: Sail-based semantics, testing, and reasoning, for production and CHERI-enabled architectures
Chung-chieh ShanShan, Chung-chieh Indiana University, USA Committee Member in Steering Committee within the LAFI-track
Natarajan ShankarShankar, Natarajan SRI International, USA Session Chair of Lightning Talks (part of CPP ) Committee Member in Program Committee within the CPP -track
Zhong ShaoShao, Zhong Yale University Steering Committee Chair in Steering Committee within the CPP -track Committee Member in Program Committee within the POPL -track
Rahul SharmaSharma, Rahul Microsoft Research Committee Member in Program Committee within the POPL -track
Sarai SheinvaldSheinvald, Sarai Department of Software Engineering, ORT Braude College of EngineeringIsrael Compositional Model Checking for Multi-Properties
Ben ShermanSherman, Ben On the Automatic Derivation of Importance Samplers from Pairs of Probabilistic Programs
Benjamin ShermanSherman, Benjamin Massachusetts Institute of Technology, USA λS: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
Elaine ShiShi, Elaine Cornell University Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs
Shweta ShindeShinde, Shweta ETH ZurichSwitzerland Committee Member in Program Committee within the PriSC-track
Avraham ShinnarShinnar, Avraham IBM Research CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Bhargav ShivkumarShivkumar, Bhargav State University of New York - University at BuffaloUnited States Putting gradual types to work
Sharon ShohamShoham, Sharon Tel Aviv University Learning the Boundary of Inductive Invariants Conference Co-Chair in Organizing Committee within the VMCAI-track
Nikolaj SidorencoSidorenco, Nikolaj Aarhus University Formalising MPC-in-the-head-based zero-knowledge
Jesse SigalSigal, Jesse University of EdinburghUnited Kingdom Automatic Differentiation via Effects and Handlers: An Implementation in Frank
Julien SignolesSignoles, Julien CEA LISTFrance Runtime Abstract Interpretation for Numerical Accuracy and Robustness
Alexandra SilvaSilva, Alexandra University College LondonUnited Kingdom Accessibility Chair in Organizing Committee for POPL 2021 SIGPLAN CARES
Lisandra SilvaSilva, Lisandra University of Minho Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Lucas SilverSilver, Lucas University of Pennsylvania Dijkstra Monads Forever
Rishabh SinghSingh, Rishabh Google BrainUnited States Committee Member in Program Committee within the POPL -track
Kartik SinghalSinghal, Kartik University of ChicagoUnited States Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jeffrey Mark SiskindSiskind, Jeffrey Mark School of Electrical and Computer Engineering, Purdue UniversityUnited States Committee Member in Steering Committee within the LAFI-track
A. Prasad SistlaSistla, A. Prasad University of Illinois at Chicago Deciding Accuracy of Differential Privacy Schemes
KC SivaramakrishnanSivaramakrishnan, KC IIT MadrasIndia ConFuzz: Coverage-guided Property Fuzzing for Event-driven Programs Panel Discussion 3: Work/Life Balance Committee Member in Programme Committee within the PADL-track
J Tanner SlagelSlagel, J Tanner NASA Langley Research CenterUnited States Formal Verification of Semi-algebraic Sets and Real Analytic Functions
Gus Henry SmithSmith, Gus Henry University of Washington Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Pawel SobocinskiSobocinski, Pawel Tallinn University of Technology Functorial Semantics for Partial Theories
Ana SokolovaSokolova, Ana University of SalzburgAustria Committee Member in Program Committee within the POPL -track
Armando Solar-LezamaSolar-Lezama, Armando Massachusetts Institute of Technology Parametric Inversion of Non-Invertible Programs
Alaia Solko-BreslinSolko-Breslin, Alaia Cornell University Petr4: Formal Foundations for P4 Data Planes
Tran Cao SonSon, Tran Cao New Mexico State UniversityUnited States A Logic Programming Approach to Regression Based Repair of Incorrect Initial Belief States
Yahui SongSong, Yahui National University of SingaporeSingapore A Synchronous Effects Logic for Temporal Verification of Pure Esterel
Matthieu SozeauSozeau, Matthieu InriaFrance Session with the Coq Development Team Committee Member in Program Committee within the POPL -track
Simon SpiesSpies, Simon MPI-SWS and University of Cambridge Transfinite Step-Indexing for Termination
Bas SpittersSpitters, Bas Concordium Blockchain Research Center, Aarhus University Formalising MPC-in-the-head-based zero-knowledge Extracting Smart Contracts Tested and Verified in Coq
Caleb StanfordStanford, Caleb University of Pennsylvania Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Kathrin StarkStark, Kathrin Princeton University, USAUnited States Committee Member in Program Committee within the CPP -track Committee Member in Program Committee within the CoqPL-track Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Štěpán StarostaStarosta, Štěpán Faculty of Information Technology, Czech Technical University in PragueCzech Republic Formalization of Combinatorics on Words in Isabelle/HOL
Sam StatonStaton, Sam University of Oxford An algebraic theory of conditioning Probabilistic Programming Semantics for Name Generation
Guy L. Steele Jr.Steele Jr., Guy L. Oracle LabsUnited States Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Deian StefanStefan, Deian University of California at San Diego, USA Session Chair of Short talks (part of PriSC) Session Chair of Invited talk (part of PriSC) Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade Committee Member in Steering Committee within the PriSC-track Committee Member in Program Committee within the PriSC-track
Bernhard SteffenSteffen, Bernhard TU DortmundGermany Generative Program Analysis and Beyond: The Power of Domain-Specific Languages Invited Speaker in Invited Speakers within the VMCAI-track
Dario SteinStein, Dario University of Oxford An algebraic theory of conditioning Probabilistic Programming Semantics for Name Generation
Jon StephensStephens, Jon University of Texas at Austin Verifying Correct Usage of Context-Free API Protocols
Ilina StoilkovskaStoilkovska, Ilina Vienna University of Technology Austria Eliminating Message Counters in Synchronous Threshold Automata
Yusen SuSu, Yusen New York University, University of WaterlooCanada Data Flow Refinement Type Inference
Pavle SuboticSubotic, Pavle Microsoft and Mathematical Institute, Serbian Academy of Sciences and Arts (SASA)Serbia Abstracting Large-scale Datalog: A Scalable Provenance Evaluation Strategy Debugging Large-Scale Datalog: A Scalable Provenance Evaluation Strategy
Zachary SullivanSullivan, Zachary University of Oregon Strictly Capturing Non-Strict Closures
Eijiro SumiiSumii, Eijiro Tohoku University Committee Member in Program Committee within the PEPM-track
Alexander J. SummersSummers, Alexander J. University of British Columbia Session Chair of Decision Procedures (part of VMCAI) Committee Member in Program Committee within the VMCAI-track
T Quang-Trung TaTa, Quang-Trung National University of SingaporeSingapore Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
Nicolas TabareauTabareau, Nicolas InriaFrance Gradualizing the Calculus of Inductive Constructions The Taming of the Rew: A Type Theory with Computational Assumptions
Yoshiki TakashimaTakashima, Yoshiki Committee Member in Artifact Evaluation Committee within the VMCAI-track
Akira TanakaTanaka, Akira National Institute of Advanced Industrial Science and Technology (AIST) Coq to C Translation with Partial Evaluation
Éric TanterTanter, Éric University of Chile Gradualizing the Calculus of Inductive Constructions
Paul TarauTarau, Paul University of North TexasUnited States Session Chair of Declarative Approaches to Testing and Debugging (part of PADL) A Family of Unification-oblivious Program Transformations and Their Applications Committee Member in Programme Committee within the PADL-track
Fabio TardivoTardivo, Fabio New Mexico State UniversityUnited States A Logic Programming Approach to Regression Based Repair of Incorrect Initial Belief States
Mohamed TarekTarek, Mohamed UNSW Canberra, Australia Bayesian Neural Ordinary Differential Equations
Joseph TassarottiTassarotti, Joseph Boston College A Formal Proof of PAC Learnability for Decision Stumps [T4] Iris – A Modular Foundation for Higher-Order Concurrent Separation Logic
Enrico TassiTassi, Enrico INRIAFrance Session with the Coq Development Team
Zachary TatlockTatlock, Zachary University of Washington, SeattleUnited States egg: Fast and Extensible Equality Saturation
Hanneli TavanteTavante, Hanneli McGill University Student Volunteer Co-Chair in Organizing Committee for POPL 2021 Committee Member in Student Volunteers Committee within the POPL Student Volunteers-track
Zenna TavaresTavares, Zenna Massachusetts Institute of Technology Parametric Inversion of Non-Invertible Programs
Matúš TejiščákTejiščák, Matúš Chordify Erasure In Dependently Typed Programming
Jérémy ThibaultThibault, Jérémy MPI-SPGermany Nanopass Back-Translation of Multiple Traces for Secure Compilation Proofs
René ThiemannThiemann, René University of Innsbruck An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR Committee Member in Program Committee within the CPP -track
Ramanathan S. ThinniyamThinniyam, Ramanathan S. Max Planck Institute for Software Systems (MPI-SWS) Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
Amin TimanyTimany, Amin Aarhus UniversityDenmark Web Chair in Organizing Committee for POPL 2021 Session Chair of Formalized Mathematics (part of CPP ) Reasoning About Programs in Higher-Order Concurrent Separation Logic Reasoning About Monotonicity in Separation Logic Efficient and Provable Local Capability Revocation using Uninitialized Capabilities Fully Abstract from Static to Gradual Mechanized Logical Relations for Termination-Insensitive Noninterference Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic Committee Member in Program Committee within the CPP -track Co-chair in Organizing Committee within the CoqPL-track Invited Speaker in Invited Speakers within the PLMW-track
Sam Tobin-HochstadtTobin-Hochstadt, Sam Indiana University Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
Andrew TolmachTolmach, Andrew Portland State University Towards formally verified compilation of tag-based policy enforcement
John TomanToman, John Certora, inc. Counterexample Generation for Program Verification based on Ownership Refinement Types
Sever TopanTopan, Sever McGill University On the Interpretability of SATNet Clauses
Sophie TourretTourret, Sophie Max Planck Institute for Informatics A Modular Isabelle Framework for Verifying Saturation Provers
Barry TragerTrager, Barry IBM Research CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Alix TrieuTrieu, Alix Aarhus UniversityDenmark Toward Complete Stack Safety for Capability Machines Efficient and Provable Local Capability Revocation using Uninitialized Capabilities Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jean-Baptiste TristanTristan, Jean-Baptiste Boston CollegeUnited States Session Chair of Session 1 (part of LAFI) Session Chair of Invited talk: Vikash K. Mansinghka (part of LAFI) A Formal Proof of PAC Learnability for Decision Stumps Committee Member in Organizing Committee within the LAFI-track
Stelios TsampasTsampas, Stelios A Categorical Approach to Secure Compilation (and others things) (short talk)
Takeshi TsukadaTsukada, Takeshi Chiba University, JapanJapan Counterexample Generation for Program Verification based on Ownership Refinement Types
Dean TullsenTullsen, Dean University of California at San Diego, USA Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Aaron TuronTuron, Aaron Fastly Emotional Machines Invited Speaker in Invited Speakers within the PLMW-track
U Hideto UenoUeno, Hideto The Univeristy of Tokyo Counterexample Generation for Program Verification based on Ownership Refinement Types
Josef UrbanUrban, Josef Czech Technical University in PragueCzech Republic Committee Member in Program Committee within the CPP -track
V Viktor VafeiadisVafeiadis, Viktor MPI-SWSGermany PerSeVerE: Persistency Semantics for Verification under Ext4 Committee Member in Program Committee within the POPL -track
Koundinya VajjhaVajjha, Koundinya University of Pittsburgh CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq A Formal Proof of PAC Learnability for Decision Stumps
Aslan Garcia ValadezValadez, Aslan Garcia National Autonomous University of Mexico Bayesian Neural Ordinary Differential Equations
Cas van der Restvan der Rest, Cas Delft University of Technology Staged Effects and Handlers for Modular Languages with Abstraction
Floris van Doornvan Doorn, Floris University of PittsburghUnited States Committee Member in Program Committee within the CPP -track
David Van HornVan Horn, David University of Maryland, USAUnited States Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification Committee Member in Program Committee within the POPL -track
Thomas Van StrydonckVan Strydonck, Thomas KULeuven Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Gabriele VanoniVanoni, Gabriele University of Bologna & INRIA Sophia Antipolis The (In)Efficiency of Interaction
Marco VassenaVassena, Marco CISPA Helmholtz Center for Information SecurityGermany Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Niki VazouVazou, Niki IMDEA Software Institute [T2] Liquid Haskell: Refinement Type Checker for Haskell Committee Member in Program Committee within the PEPM-track Committee Member in Program Committee within the VMCAI-track
Ratko G. VeprekVeprek, Ratko G. Digital Asset A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers
Darya VerzhbinskyVerzhbinsky, Darya UC San Diego Petsy: Polymorphic Enumerative Type-Guided Synthesis
Pierre VialVial, Pierre Inria Paris-Saclay Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
German VidalVidal, German Universitat Politecnica de ValenciaSpain Causal-Consistent Reversible Debugging: Improving CauDEr
Hugo VincentVincent, Hugo Arm ResearchUnited Kingdom Frontiers in Secure Compilation – an Industrial Perspective (invited talk)
Simon Friis VindumVindum, Simon Friis Aarhus UniversityDenmark Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
Eelco VisserVisser, Eelco Delft University of Technology Intrinsically Typed Compilation with Nameless Labels Committee Member in Program Committee within the PEPM-track
Mahesh ViswanathanViswanathan, Mahesh University of Illinois at Urbana-Champaign Deciding Accuracy of Differential Privacy Schemes Optimal Prediction of Synchronization-Preserving Races
Jan VitekVitek, Jan Northeastern University / Czech Technical University Formally Verified Speculation and Deoptimization in a JIT Compiler
Yakir VizelVizel, Yakir Technion—Israel Institute of TechnologyIsrael Session Chair of Invited talk (part of VMCAI) Session Chair of Invited talk (part of VMCAI) Conference Co-Chair in Organizing Committee within the VMCAI-track
Son Tuan VuVu, Son Tuan Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6 Secure Optimization Through Opaque Observations
Andrey VyatkinVyatkin, Andrey Saint Petersburg State University Certified Semantics for miniKanren
Dimitrios VytiniotisVytiniotis, Dimitrios DeepMindUnited Kingdom Committee Member in Program Committee within the LAFI-track
Franck VédrineVédrine, Franck CEA LISTFrance Runtime Abstract Interpretation for Numerical Accuracy and Robustness
W Riad S. WahbyWahby, Riad S. Stanford University, USA High-level high-speed high-assurance crypto
David WalkerWalker, David Princeton University, USA SIGPLAN CARES SIGPLAN CARES
Daniel WangWang, Daniel UC San Diego Petsy: Polymorphic Enumerative Type-Guided Synthesis
Peixin WangWang, Peixin Shanghai Jiao Tong University Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yisu Remy WangWang, Yisu Remy University of WashingtonUnited States egg: Fast and Extensible Equality Saturation
Mark WassellWassell, Mark University of Cambridge Formalising MiniSail in Isabelle
Conrad WattWatt, Conrad University of Cambridge, UK Committee Member in Program Committee within the PriSC-track
Christoph WeidenbachWeidenbach, Christoph MPI-INFGermany Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories Committee Member in Program Committee within the CPP -track
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States A Graded Dependent Type System with a Usage-Aware Semantics SIGPLAN CARES SIGPLAN CARES
Aaron WeissWeiss, Aaron Northeastern UniversityUnited States Student Volunteer Co-Chair in Organizing Committee for POPL 2021 Committee Member in Student Volunteers Committee within the POPL Student Volunteers-track
Sam WestrickWestrick, Sam Carnegie Mellon UniversityUnited States Provably Space Efficient Parallel Functional Programming
Michael WhalenWhalen, Michael University of Minnesota, USAUnited States Committee Member in Program Committee within the VMCAI-track
Lauren WhiteWhite, Lauren Kansas State UniversityUnited States Formal Verification of Semi-algebraic Sets and Real Analytic Functions
Josef WidderWidder, Josef Informal Systems A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries Eliminating Message Counters in Synchronous Threshold Automata Specification and model checking of Tendermint consensus in TLA+
Freek WiedijkWiedijk, Freek Radboud University NijmegenNetherlands Session Chair of Compilers and Interpreters (part of CPP ) Committee Member in Program Committee within the CPP -track
Jan WielemakerWielemaker, Jan Committee Member in Programme Committee within the PADL-track
Thomas WiesWies, Thomas New York University, USA Data Flow Refinement Type Inference
James R. WilcoxWilcox, James R. University of WashingtonUnited States Session Chair of Model Checking (part of VMCAI) Learning the Boundary of Inductive Invariants Committee Member in Program Committee within the VMCAI-track
Max WillseyWillsey, Max University of Washington, USA egg: Fast and Extensible Equality Saturation
Theo WinterhalterWinterhalter, Theo Inria — LS2N The Taming of the Rew: A Type Theory with Computational Assumptions
Dylan WolffWolff, Dylan ETH Zurich Value Mutation Testing for SMT Solvers
Sebastian WolffWolff, Sebastian TU BraunschweigGermany Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Michael WolmanWolman, Michael McGill UniversityCanada Probabilistic Programming Semantics for Name Generation
James WorrellWorrell, James University of OxfordUnited Kingdom Dynamical Systems and Program Analysis Deciding ω-Regular Properties on Linear Recurrence Sequences
Xiaodi WuWu, Xiaodi University of Maryland, USAUnited States [T5] An Invitation to the Intersection of Quantum Computing and Programming Languages A Verified Optimizer for Quantum Circuits
X Ningning XieXie, Ningning The University of Hong KongChina Committee Member in Programme Committee within the PADL-track
Amanda XuXu, Amanda Cornell University Petr4: Formal Foundations for P4 Data Planes
Jianhao XuXu, Jianhao Nanjing University Cross-Architecture Testing for Compiler-Introduced Security Bugs
Anton XueXue, Anton University of Pennsylvania A Self-Certifying Compilation Framework for WebAssembly
Y Eran YahavYahav, Eran Technion Robin Milner Award Talk: "Structural Language Models of Code"
Jeremy YallopYallop, Jeremy University of CambridgeUnited Kingdom Session Chair of Session 4 (part of PEPM) A Practical Mode System for Recursive Definitions Committee Member in Program Committee within the PEPM-track Steering Committee Chair in Steering Committee within the PEPM-track
Cambridge YangYang, Cambridge MIT CSAIL Simplifying Multiple-Statement Reductions with the Polyhedral Model
Hongseok YangYang, Hongseok KAISTSouth Korea SIGPLAN CARES Panel Discussion 2: Improving Peer Review Panel Discussion 1: Choosing Research Topics
Nobuko YoshidaYoshida, Nobuko Imperial College London Precise Subtyping for Asynchronous Multiparty Sessions Committee Member in Program Committee within the POPL -track
David YoungYoung, David University of Kansas, USAUnited States On Adding Pattern Matching to Haskell-based Deeply Embedded Domain Specific Languages
Z Fabian ZaiserZaiser, Fabian University of Oxford Binary Tree Hamiltonian Monte Carlo
Yannick ZakowskiZakowski, Yannick InriaFrance Session Chair of Semantics (part of CPP ) Verifying a compiler through equational means Committee Member in Program Committee within the CPP -track Invited Speaker in Invited speaker within the CoqPL-track
Vadim ZalivaZaliva, Vadim Carnegie Mellon University, USAUnited States How to verify an ASN.1 Protocol C-language Stack in Coq?
Arnel ZamaylaZamayla, Arnel University of Calabria, ItalyItaly Data validation meets Answer Set Programming
Santiago Zanella-BéguelinZanella-Béguelin, Santiago Microsoft Research, CambridgeUnited Kingdom Committee Member in Program Committee within the POPL -track
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Dijkstra Monads Forever
Georg ZetzscheZetzsche, Georg Max Planck Institute for Software Systems (MPI-SWS)Germany Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
Max ZeunerZeuner, Max Stockholm University Internalizing Representation Independence with Univalence
Chi ZhangZhang, Chi CMUChina Netter: Probabilistic, Stateful Network Models
Han ZhangZhang, Han Carnegie Mellon UniversityUnited States Netter: Probabilistic, Stateful Network Models
Hongce ZhangZhang, Hongce Princeton UniversityUnited States Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
Qirun ZhangZhang, Qirun Georgia Institute of Technology, USA On the Complexity of Bidirected Interleaved Dyck-Reachability
Zhenya ZhangZhang, Zhenya National Institute of Informatics Artifact Evaluator in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
David ZhaoZhao, David The University of Sydney Abstracting Large-scale Datalog: A Scalable Provenance Evaluation Strategy Debugging Large-Scale Datalog: A Scalable Provenance Evaluation Strategy
Tan Zhi-XuanZhi-Xuan, Tan Massachusetts Institute of Technology Genify.jl: Transforming Julia into Gen to enable programmable inference
Neng-Fa ZhouZhou, Neng-Fa CUNY Brooklyn College and Graduate Center Committee Member in Programme Committee within the PADL-track
Lukasz ZiarekZiarek, Lukasz SUNY Buffalo, USAUnited States Synchronous Message-Passing with Priority Putting gradual types to work
Rébecca ZucchiniZucchini, Rébecca LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay A Coq Formalization of Data Provenance
Lenore ZuckZuck, Lenore UICUnited States Committee Member in Program Committee within the VMCAI-track
Damien ZuffereyZufferey, Damien MPI-SWS Committee Member in Program Committee within the POPL -track
Florian ZulegerZuleger, Florian Vienna University of TechnologyAustria Eliminating Message Counters in Synchronous Threshold Automata
Å Johannes Åman PohjolaÅman Pohjola, Johannes Data61 at CSIRO / UNSW Committee Member in Program Committee within the CPP -track
Ö Joakim ÖhmanÖhman, Joakim IMDEA Software Institute Committee Member in Artifact Evaluation Committee within the VMCAI-track

POPL 2021 Contributors

Results (744)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia