POPL 2022 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (848)

A Joshua A. BockenekA. Bockenek, Joshua Virginia Tech Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Carmine AbateAbate, Carmine Max Planck Institute for Security and Privacy, Bochum, Germany The Fox and the Hound (Episode 2): Fully Abstract, Robust Compilation and How to Reconcile the Two, Abstractly
Mohammad AbdulazizAbdulaziz, Mohammad Technische Universität MünchenGermany Committee Member in Program Committee within the CPP-track
Michael D. AdamsAdams, Michael D. University of MichiganUnited States Committee Member in Program Committee within the POPL -track
Amal AhmedAhmed, Amal Northeastern University, USAUnited States Committee Member in Program Committee within the POPL -track
Alfred V. AhoAho, Alfred V. Columbia UniversityUnited States Principles of Programming Language Translators
Benedikt AhrensAhrens, Benedikt TU Delft, The NetherlandsNetherlands Implementing a category-theoretic framework for typed abstract syntax
Alex AikenAiken, Alex Stanford UniversityUnited States Induction Duality: Primal-Dual Search for Invariants
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin-MadisonUnited States Interval Universal Approximation for Neural Networks PC Member in Program Committee within the VMCAI-track
Jade AlglaveAlglave, Jade University College LondonFrance Armed cats: formal concurrency modelling at Arm
Guillaume AllaisAllais, Guillaume University of St AndrewsUnited Kingdom Using Dependent Types at Scale: Maintaining the Agda Standard Library
Bernardo AlmeidaAlmeida, Bernardo LASIGE, Faculty of Sciences, University of Lisbon Deciding type equivalence with simple grammars
María AlpuenteAlpuente, María U.P. ValenciaSpain Committee Member in Program Committee within the PEPM-track
Rajeev AlurAlur, Rajeev University of Pennsylvania General Chair in Organizing Committee for POPL 2022 Session Chair of Invited Talk (part of POPL ) Session Chair of POPL Business Meeting and SIGPLAN Awards (part of POPL ) Session Chair of Welcome (part of POPL ) General Chair Report Open Forum for Q&A Committee Member in Selection Committee within the POPL Virtual Workshop-track
Guillaume AmbalAmbal, Guillaume Univ. Rennes Certified Abstract Machines for Skeletal Semantics
Nada AminAmin, Nada Harvard UniversityUnited States Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion
Abhishek AnandAnand, Abhishek Cornell UniversityUnited States Committee Member in Program Committee within the CoqPL-track
June AndronickAndronick, June Proofcraft, UNSW and seL4 FoundationAustralia The seL4 verification: the art and craft of proof and the reality of commercial support
Timos AntonopoulosAntonopoulos, Timos Yale University Committee Member in Program Committee within the ProLaLa-track
Andrew W. AppelAppel, Andrew W. Princeton Coq’s vibrant ecosystem for verification engineering
Vincenzo ArceriArceri, Vincenzo University of Parma - Department of Mathematical, Physical, and Computer SciencesItaly Session Chair of Privacy and Security (part of VMCAI) Relational String Abstract Domains
Owen ArdenArden, Owen UC Santa CruzUnited States Committee Member in Program Committee within the PriSC-track
Joaquín AriasArias, Joaquín Universidad Rey Juan CarlosSpain Modeling and Verification of Real-Time Systems with the Event Calculus and s(CASP) Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming Modeling Administrative Discretion Using Goal-Directed Answer Set Programming Committee Member in Program Committee within the ProLaLa-track
Zena M. AriolaAriola, Zena M. University of OregonUnited States Proving and Programming Welcome & Announcement Invited Speaker in Invited speakers within the PLMW-track Committee Member in Organizing Committee within the PEPM-track Co-chair in Program Committee within the PEPM-track
Alasdair ArmstrongArmstrong, Alasdair University of Cambridge Committee Member in Selection Committee within the POPL Student Research Competition-track
Robert AtkeyAtkey, Robert University of Strathclyde Committee Member in Program Committee within the POPL -track
Jeremy AvigadAvigad, Jeremy Carnegie Mellon University, USA A verified algebraic representation of Cairo program execution
Mauricio Ayala-RinconAyala-Rincon, Mauricio University of BrasíliaBrazil Committee Member in Program Committee within the CPP-track
Sacha-Élie AyounAyoun, Sacha-Élie Amazon and Imperial College LondonUnited Kingdom Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Boston UniversityUnited States Session Chair of Systems (part of POPL ) Session Chair of Secure compilation theory (part of PriSC) On Incorrectness Logic and Kleene Algebra with Top and Tests Committee Member in Program Committee within the PriSC-track
B Casper Bach PoulsenBach Poulsen, Casper Delft University of Technology Committee Member in Steering Committee within the PEPM-track
Christel BaierBaier, Christel TU Dresden, GermanyGermany PC Member in Program Committee within the VMCAI-track
Chris BaileyBailey, Chris University of Illinois College of Law A General Library of Legal Components
Marcello BalducciniBalduccini, Marcello Saint Joseph's University, USA People, Ideas, and the Path Ahead
Stephanie BalzerBalzer, Stephanie Carnegie Mellon UniversityUnited States Session Chair of Afternoon 1 (part of PLMW) Session Chair of Morning 3 (live only, no recording) (part of PLMW) Panel 2: the future of concurrency and parallelism Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic Committee Member in Organizing Committee within the PLMW-track
Nikola BanovicBanovic, Nikola University of Michigan Cod(e)ifying The Law
Jialu BaoBao, Jialu Cornell UniversityUnited States A Separation Logic for Negative Dependence
Earl BarrBarr, Earl UCLUnited Kingdom High Assurance Software for Financial Regulation and Business Platforms
Clark BarrettBarrett, Clark Stanford UniversityUnited States Bit-Precise Reasoning via Int-Blasting
Noah Lev Bartell-MangelBartell-Mangel, Noah Lev Filling a Niche: Using Spare Bits to Optimize Data Representations
Adam D. BarwellBarwell, Adam D. Imperial College London, UK Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Iulia BastysBastys, Iulia Chalmers University of TechnologySweden Committee Member in Program Committee within the PriSC-track
Kinjal BasuBasu, Kinjal The University of Texas at DallasUnited States Modeling and Verification of Real-Time Systems with the Event Calculus and s(CASP)
Shrutarshi BasuBasu, Shrutarshi Harvard UniversityUnited States Session Chair of Long talks #6 (part of ProLaLa) Littleton: An Educational Environment for Property Law Legal Calculi Committee Member in Program Committee within the ProLaLa-track
Mark BattyBatty, Mark University of KentUnited Kingdom The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Kevin BatzBatz, Kevin RWTH Aachen University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Andrej BauerBauer, Andrej University of LjubljanaSlovenia Committee Member in Program Committee within the CPP-track
Thomas BauereissBauereiss, Thomas University of Cambridge Committee Member in Program Committee within the CPP-track
Pascal BaumannBaumann, Pascal MPI-SWSGermany Context-Bounded Verification of Thread Pools
David BayaniBayani, David Carnegie Mellon University's School of Computer ScienceUnited States Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned Systems
Atılım Güneş BaydinBaydin, Atılım Güneş Department of Engineering Science, University of Oxford Probabilistic and Differentiable Programming in Scientific Simulators
Janis BeckedorfBeckedorf, Janis Ruprecht-Karls-Universität Heidelberg, Heidelberg, Germany Law Smells: Defining and Detecting Problematic Patterns in Legal Drafting
Heiko BeckerBecker, Heiko MPI-SWSGermany Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Pierpaolo BellusciBellusci, Pierpaolo University of CalabriaItaly Modelling the Outlier Detection Problem in QASP
Josh BerdineBerdine, Josh MetaUnited Kingdom Concurrent Incorrectness Separation Logic
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States Session Chair of Verification 1 (part of POPL ) Session Chair of Chairs' Report and Business Meeting (part of CPP) Session Chair of Welcome from the chairs (part of CPP) Conference Chair in Organization Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
Gilbert BernsteinBernstein, Gilbert University of California at BerkeleyUnited States Session Chair of Foundation and Verification of Machine-Learning Systems (part of POPL ) Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
Yves BertotBertot, Yves INRIAFrance Session with the Coq Development Team Committee Member in Program Committee within the CPP-track
Frédéric BessonBesson, Frédéric Inria Type-directed Program Transformation for Constant-Time Enforcement
Raven BeutnerBeutner, Raven CISPA Helmholtz Center for Information Security, Germany Rigorous Approximation of Posterior Inference for Probabilistic Programs
Dirk BeyerBeyer, Dirk LMU Munich, GermanyGermany PC Member in Program Committee within the VMCAI-track
Jeffrey BilikBilik, Jeffrey University of Michigan Cod(e)ifying The Law
Nicolas BiriBiri, Nicolas Luxembourg Institute of Science and Technology Dependent tagless final
Lars BirkedalBirkedal, Lars Aarhus University mitten: A Flexible Multimodal Proof Assistant Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library Committee Member in Program Committee within the CPP-track
Stefano BistarelliBistarelli, Stefano University of PerugiaItaly Timed Concurrent Language for Argumentation: an Interleaving Approach
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands Committee Member in Steering Committee within the CPP-track
Roberto BlancoBlanco, Roberto Max Planck Institute for Security and Privacy (MPI-SP) SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation Committee Member in Program Committee within the PriSC-track
Olivier BlanvillainBlanvillain, Olivier EPFLSwitzerland Type-Level Programming with Match Types
Sandrine BlazyBlazy, Sandrine Univ Rennes, IRISAFrance Committee Member in Program Committee within the POPL -track
Sylvie BoldoBoldo, Sylvie Inria and Université Paris-SaclayFrance Committee Member in Program Committee within the CPP-track
CF Bolz-TereickBolz-Tereick, CF Heinrich-Heine-Universität DüsseldorfGermany Two-level Just-in-Time Compilation with One Interpreter and One Engine
Daniel BorkmannBorkmann, Daniel Isovalent BPF and Spectre: Mitigating transient execution attacks
Ahmed BouajjaniBouajjani, Ahmed IRIF, Université Paris DiderotFrance PC Member in Program Committee within the VMCAI-track
Sylvain BoulméBoulmé, Sylvain Grenoble Alps University / CNRS / Grenoble INP / VERIMAG A CompCert backend with symbolic encryption Formally Verified Superblock Scheduling
William J. BowmanBowman, William J. University of British ColumbiaCanada Session Chair of Keynote 2 (part of PEPM) Committee Member in Program Committee within the PEPM-track Committee Member in Program Committee within the WITS-track
Jonathan Immanuel BrachthäuserBrachthäuser, Jonathan Immanuel University of TübingenGermany Session Chair of Contributed Talks 2 (part of PEPM) Type-Level Programming with Match Types Committee Member in Program Committee within the PEPM-track
Ana BrendelBrendel, Ana University of Texas at AustinUnited States Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Tegan BrennanBrennan, Tegan Stevens Institute of TechnologyUnited States PC Member in Program Committee within the PriSC-track
Antonio BrogiBrogi, Antonio Università di PisaItaly Session Chair of Invited talk (part of PADL) Green Application Placement in the Cloud-IoT Continuum
David BromanBroman, David KTHSweden Committee Member in Program Committee within the POPL -track
Christopher BrownBrown, Christopher University of St. Andrews, UK Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Lei BuBu, Lei Nanjing UniversityChina Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata
Lukas BuecherlBuecherl, Lukas University of Colorado, BoulderUnited States STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model Checking
Tobias BurghardtBurghardt, Tobias University of TübingenGermany Functional Programming on Top of SQL Engines
Matteo BusiBusi, Matteo Università di Pisa - Dipartimento di InformaticaItaly The Fox and the Hound (Episode 2): Fully Abstract, Robust Compilation and How to Reconcile the Two, Abstractly Committee Member in Program Committee within the PriSC-track
Kevin BuzzardBuzzard, Kevin Imperial College London Panel 1: proof assistants for PL and math
William E. ByrdByrd, William E. University of Alabama at Birmingham, USAUnited States Committee Member in Program Committee within the PEPM-track
Maximilian BötherBöther, Maximilian Hasso Plattner Institute, University of Potsdam, Potsdam, Germany Law Smells: Defining and Detecting Problematic Patterns in Legal Drafting
C Pedro CabalarCabalar, Pedro University of CorunnaSpain Committee Member in Programme Committee within the PADL-track
Nina CahillCahill, Nina University of Michigan Cod(e)ifying The Law
Miguel CalejoCalejo, Miguel logicalcontracts.com Logical English as a Programming Language for the Law
Francesco CalimeriCalimeri, Francesco University of CalabriaItaly Session Chair of Declarative Solutions (part of PADL) Smart Devices and Large Scale Reasoning via ASP: Tools and Applications Committee Member in Programme Committee within the PADL-track
Eric CampbellCampbell, Eric Cornell UniversityUnited States Dependently-Typed Data Plane Programming
Marco CampionCampion, Marco University of VeronaItaly Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis
Ali Can ArıcıCan Arıcı, Ali Ekol LogisticsTurkey Multi-Agent Pick and Delivery with Capacities: Action Planning vs Path Finding
Paulo CanelasCanelas, Paulo LASIGE, Faculdade de Ciências da Universidade de Lisboa Understandable and Useful Error Messages for Liquid Types
Qinxiang CaoCao, Qinxiang Shanghai Jiao Tong UniversityChina Committee Member in Program Committee within the CPP-track
Michael CarbinCarbin, Michael Massachusetts Institute of TechnologyUnited States Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs Committee Member in Program Committee within the POPL -track
Quentin CarbonneauxCarbonneaux, Quentin MetaFrance Applying Formal Verification to Microkernel IPC at Meta
Manuel CarroCarro, Manuel IMDEA Software Institute and T.U. of Madrid (UPM)Spain Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming
Giuseppe CastagnaCastagna, Giuseppe CNRS; Université de ParisFrance On Type-Cases, Union Elimination, and Occurrence Typing
Claudia CauliCauli, Claudia Amazon Web ServicesSweden Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Sunjay CauligiCauligi, Sunjay University of California at San Diego, USA Committee Member in Program Committee within the PriSC-track
Tej ChajedChajed, Tej Massachusetts Institute of Technology, USAUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Hing Lun ChanChan, Hing Lun Australian National University Windmills of the minds: an algorithm for Fermat's Two Squares Theorem
Jonathan ChanChan, Jonathan University of British Columbia (UBC)Canada Towards a Syntactic Model of Sized Dependent Types
Arun ChandrasekharanChandrasekharan, Arun OneSpin Solutions, MunichGermany Making PROGRESS in Property Directed Reachability
Arthur CharguéraudCharguéraud, Arthur InriaFrance Specification and Verification of a Transient Stack
Swarat ChaudhuriChaudhuri, Swarat University of Texas at AustinUnited States Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Eason ChenChen, Eason Accord ProjectTaiwan Ergo - a programming language for Smart Legal Contracts
Taolue ChenChen, Taolue Birkbeck University of LondonUnited Kingdom Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Yixuan ChenChen, Yixuan Yale University, USA Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yu-Fang ChenChen, Yu-Fang Academia Sinica, Taiwan Committee Member in Program Committee within the VMCAI-track
James CheneyCheney, James University of Edinburgh; Alan Turing InstituteUnited Kingdom Session Chair of Invited talk (part of PADL) Probabilistic programming for Employment Tribunal remedies Program Co-Chair in Programme Chairs within the PADL-track
Alvin CheungCheung, Alvin University of California, Berkeley Committee Member in Program Committee within the POPL -track
Louis CheungCheung, Louis University of Melbourne Overcoming Restraint: Composing Verification of Foreign Functions with Cogent
Maria Chiara MeoChiara Meo, Maria University “G. d’Annunzio” of Chieti-PescaraItaly Timed Concurrent Language for Argumentation: an Interleaving Approach
Wei-Ngan ChinChin, Wei-Ngan National University of Singapore Committee Member in Program Committee within the POPL -track
Dmitry ChistikovChistikov, Dmitry University of WarwickUnited Kingdom Subcubic Certificates for CFL Reachability
Pavan Kumar ChittimalliChittimalli, Pavan Kumar TCS ResearchIndia Committee Member in Programme Committee within the PADL-track
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Virtualization Co-Chair in Organizing Committee for POPL 2022 Session Chair of Invited Talk (part of POPL ) Certifying Derivation of State Machines from Coroutines Virtualization Chair Report Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites Co-chair in Selection Committee within the POPL Virtual Workshop-track Committee Member in Steering Committee within the CPP-track
Kyeongmin ChoCho, Kyeongmin KAISTSouth Korea Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Wonhyuk ChoiChoi, Wonhyuk Columbia University Artifact Evalation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Vikraman ChoudhuryChoudhury, Vikraman Indiana University; University of CambridgeUnited States Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
Maria ChristakisChristakis, Maria MPI-SWSGermany Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
Jan ChristiansenChristiansen, Jan Flensburg University of Applied Sciences, Germany Committee Member in Programme Committee within the PADL-track
Lukas ChrpaChrpa, Lukas Czech Technical University in Prague Determining Action Reversibility in STRIPS Using Answer Set Programming with Quantifiers
Luca CicconeCiccone, Luca University of TurinItaly Fair Termination of Binary Sessions
Cristina CifuentesCifuentes, Cristina Oracle LabsAustralia PLMW Panel (on Zoom)
Pierre ClairambaultClairambault, Pierre CNRS & ENS LyonFrance Committee Member in Program Committee within the POPL -track
Jesper CockxCockx, Jesper TU DelftNetherlands Session Chair of Session 1 (part of WITS) Session Chair of Session 2 (part of WITS) Session Chair of Session 4 (part of WITS) Session Chair of Session 5 (part of WITS) Session Chair of Session 3 (part of WITS) Fancy module systems (discussion) Elaborator reflection APIs (discussion) Organizer in Program Committee within the WITS-track
Norine CoenenCoenen, Norine CISPA Helmholtz Center for Information Security Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Youyou CongCong, Youyou Tokyo Institute of TechnologyJapan Virtualization Co-Chair in Organizing Committee for POPL 2022 Session Chair of Keynote 4 (part of PEPM) Session Chair of Contributed Talks 3 (part of PEPM) Welcome & Announcement Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion) PLMW Panel (on Zoom) Committee Member in Organizing Committee within the PEPM-track Co-chair in Program Committee within the PEPM-track Co-chair in Selection Committee within the POPL Virtual Workshop-track
Esther ConradConrad, Esther NASA LaRC A Compositional Proof Framework for FRETish Requirements
Scott ConstableConstable, Scott Intel Corporation Towards Understanding Spectre-PHT in Memory-Safe Languages
Evelyne ContejeanContejean, Evelyne Committee Member in Program Committee within the CPP-track
Simon CookseyCooksey, Simon University of KentUnited Kingdom The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Agostino CortesiCortesi, Agostino Università Ca' Foscari VeneziaItaly Relational String Abstract Domains
Andreea CosteaCostea, Andreea School of Computing, National University Of SingaporeSingapore PLMW Panel (on Zoom)
Corinna CoupetteCoupette, Corinna Max Planck Institute for Informatics, Saarbrücken, Germany Law Smells: Defining and Detecting Problematic Patterns in Legal Drafting
Patrick CousotCousot, Patrick PC Member in Program Committee within the VMCAI-track
Silvia CrafaCrafa, Silvia University of PadovaItaly Stipula: a domain specific language for legal contracts
Raphaëlle CrubilléCrubillé, Raphaëlle Committee Member in Program Committee within the LAFI-track
D Loris D'AntoniD'Antoni, Loris University of Wisconsin-Madison, USA Publicity Chair in Organizing Committee for POPL 2022
Matthew L. DaggittDaggitt, Matthew L. Heriot-Watt University Using Dependent Types at Scale: Maintaining the Agda Standard Library
Ugo Dal LagoDal Lago, Ugo University of Bologna; InriaItaly A Relational Theory of Effects and Coeffects Effectful Program Distancing
Mila Dalla PredaDalla Preda, Mila University of VeronaItaly Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis
Hoang-Hai DangDang, Hoang-Hai MPI-SWSGermany Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Ian DardikDardik, Ian Northeastern University Formal Verification of a Distributed Dynamic Reconfiguration Protocol
Spandan DasDas, Spandan Kansas State UniversityIndia Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
João DavidDavid, João LASIGE, Faculdade de Ciências da Universidade de Lisboa Understandable and Useful Error Messages for Liquid Types
Surend DayalDayal, Surend Australian National University Industry keynote -- What does a toolchain for legislation eventually become?
Leonardo de Mourade Moura, Leonardo Microsoft Research, n.n. PC Member in Program Committee within the VMCAI-track Committee Member in Program Committee within the WITS-track
Marina De VosDe Vos, Marina University of BathUnited Kingdom Committee Member in Programme Committee within the PADL-track
Will DeaconDeacon, Will ARM Ltd. Armed cats: formal concurrency modelling at Arm
Benjamin DelawareDelaware, Benjamin Purdue UniversityUnited States Session Chair of Semantics and Program Verification (part of CPP) Scrap your boilerplate definitions in 10 lines of Ltac! Oblivious Algebraic Data Types Committee Member in Program Committee within the CPP-track
Alain DelaëtDelaët, Alain INRIA, ENS Lyon Turning Catala into a Proof Platform for the Law
Brian DemskyDemsky, Brian University of California at IrvineUnited States Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not Terminate
Dominique DevrieseDevriese, Dominique Vrije Universiteit BrusselBelgium Committee Member in Steering Committee within the PriSC-track
Henry DeYoungDeYoung, Henry CMU Panel (live only, no recording) Panelist in Panelists within the PLMW-track
Işıl DilligDillig, Işıl University of Texas at AustinUnited States Simplifying Concurrent Programming via Synchronization Synthesis SIGPLAN Reynolds Dissertation Award Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution SIGPLAN Programming Languages Achievements Award SolType: Refinement Types for Arithmetic Overflow in Solidity
Rayna DimitrovaDimitrova, Rayna CISPA Helmholtz Center for Information Security PC Member in Program Committee within the VMCAI-track
Christos DimoulasDimoulas, Christos PLT @ Northwestern UniversityUnited States Committee Member in Program Committee within the POPL -track
Dino DistefanoDistefano, Dino Facebook London PC Member in Program Committee within the VMCAI-track
Pablo DonatoDonato, Pablo Ecole polytechnique A Drag-and-Drop Proof Tactic
Paul DownenDownen, Paul University of Massachusetts LowellUnited States Session Chair of Synthesis (part of POPL ) Session Chair of Morning 2 (part of PLMW) Session Chair of Afternoon 2 (part of PLMW) Committee Member in Organizing Committee within the PLMW-track
Derek DreyerDreyer, Derek MPI-SWSGermany Concurrent Incorrectness Separation Logic VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lawrence DunnDunn, Lawrence University of PennsylvaniaUnited States Tealeaves: Categorical structures for syntax
Adrien DurierDurier, Adrien Max Planck Institute for Security and Privacy (MPI-SP) SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation
Aaron DutleDutle, Aaron NASA Langley Research CenterUnited States A Compositional Proof Framework for FRETish Requirements
Jacinto DávilaDávila, Jacinto Contratos Lógicos. C.A. and Universidad de Los Andes Logical English as a Programming Language for the Law
Emanuele D’OsualdoD’Osualdo, Emanuele MPI-SWSGermany TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
E Derek EgolfEgolf, Derek Northeastern University Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives
Matthias EichholzEichholz, Matthias TU DarmstadtGermany Dependently-Typed Data Plane Programming
Richard A. EisenbergEisenberg, Richard A. TweagFrance Session Chair of Session 1 (part of WITS) Session Chair of Session 2 (part of WITS) Session Chair of Session 4 (part of WITS) Session Chair of Session 5 (part of WITS) Session Chair of Session 3 (part of WITS) Invisible arguments: language design (discussion) Type-aware equational rewriting (discussion) Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation Organizer in Program Committee within the WITS-track
Akram El-KorashyEl-Korashy, Akram Max Planck Institute for Software Systems (MPI-SWS) SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation
Tom EllisEllis, Tom Microsoft ResearchUnited Kingdom Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Tosha EllisonEllison, Tosha Fintech Open Source FoundationUnited States High Assurance Software for Financial Regulation and Business Platforms
Michael EmmiEmmi, Michael Amazon Web ServicesUnited States Committee Member in Program Committee within the POPL -track
Andres ErbsenErbsen, Andres Massachusetts Institute of TechnologyUnited States Certifying Derivation of State Machines from Coroutines
Esra ErdemErdem, Esra Sabanci University, TurkeyTurkey Session Chair of Languages, Methods and Tools (part of PADL) Multi-Agent Pick and Delivery with Capacities: Action Planning vs Path Finding Committee Member in Programme Committee within the PADL-track
Joseph EremondiEremondi, Joseph University of British ColumbiaCanada Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Gidon ErnstErnst, Gidon Ludwig Maximilian University of MunichGermany Loop Verification with Invariants and Contracts
Martin ErwigErwig, Martin Oregon State UniversityUnited States Committee Member in Programme Committee within the PADL-track
Nel EscherEscher, Nel University of Michigan Cod(e)ifying The Law
Guilherme EspadaEspada, Guilherme LASIGE, Faculdade de Ciências da Universidade de Lisboa Understandable and Useful Error Messages for Liquid Types
Javier EsparzaEsparza, Javier Back to the Future: A Fresh Look at Linear Temporal Logic
Riley EvansEvans, Riley University of BristolUnited Kingdom CircuitFlow: : A Domain Specific Language for Dataflow Programming
F Wolfgang FaberFaber, Wolfgang University of KlagenfurtAustria Determining Action Reversibility in STRIPS Using Answer Set Programming with Quantifiers
Claudia FaggianFaggian, Claudia IRIFFrance Committee Member in Program Committee within the LAFI-track
Azadeh FarzanFarzan, Azadeh University of TorontoCanada Panel (live only, no recording) TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs Panelist in Panelists within the PLMW-track
Justus FasseFasse, Justus Université Grenoble-Alpes; KU Leuven Formally Verified Superblock Scheduling
Jim FehrleFehrle, Jim None A Visual Ltac Debugger in CoqIDE
Yotam M. Y. FeldmanFeldman, Yotam M. Y. Tel Aviv UniversityIsrael Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Marco A. FeliuFeliu, Marco A. National Institute of Aerospace Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Yu FengFeng, Yu University of California at Santa BarbaraUnited States SolType: Refinement Types for Arithmetic Overflow in Solidity
Pietro FerraraFerrara, Pietro Università Ca' Foscari, Venezia, ItalyItaly Relational String Abstract Domains
Davin FifieldFifield, Davin Oracle Industry keynote -- What does a toolchain for legislation eventually become?
Jean-Christophe FilliatreFilliatre, Jean-Christophe CNRSFrance PC Member in Program Committee within the VMCAI-track
Bernd FinkbeinerFinkbeiner, Bernd CISPA Helmholtz Center for Information SecurityGermany Session Chair of Invited Talk (part of VMCAI) Session Chair of Invited Talk (part of VMCAI) Program Co-Chair in Organizing Committee within the VMCAI-track
Marcelo FioreFiore, Marcelo University of CambridgeUnited Kingdom Formal Metatheory of Second-Order Abstract Syntax
Denis FirsovFirsov, Denis Tallinn University of TechnologyEstonia Reflection, Rewinding, and Coin-Toss in EasyCrypt
Kathleen FisherFisher, Kathleen Tufts UniversityUnited States Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives
Andrew FitzgibbonFitzgibbon, Andrew GraphcoreUnited Kingdom Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Michael FitzgibbonsFitzgibbons, Michael CapableWasm: Bringing Better Interop Down to WebAssembly
Alcides FonsecaFonseca, Alcides LASIGE, Faculdade de Ciências da Universidade de LisboaPortugal Understandable and Useful Error Messages for Liquid Types
Yannick ForsterForster, Yannick InriaFrance The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoq
Stefano FortiForti, Stefano University of PisaItaly Green Application Placement in the Cloud-IoT Continuum
Nate FosterFoster, Nate Cornell UniversityUnited States Industrial Relations in Organizing Committee for POPL 2022 Littleton: An Educational Environment for Property Law Legal Calculi Dependently-Typed Data Plane Programming Committee Member in Program Committee within the ProLaLa-track
Simon FosterFoster, Simon University of YorkUnited Kingdom Committee Member in Program Committee within the CPP-track
Cameron FreerFreer, Cameron Massachusetts Institute of TechnologyUnited States Session Chair of Keynote (part of LAFI) Committee Member in Steering Committee within the LAFI-track
Samantha FrohlichFrohlich, Samantha University of BristolUnited Kingdom CircuitFlow: : A Domain Specific Language for Dataflow Programming
Aymeric FromherzFromherz, Aymeric Inria Turning Catala into a Proof Platform for the Law
Roy FrostigFrostig, Roy Google Research JAX: accelerating ML research with composable function transformations
Daniel FruminFrumin, Daniel University of Groningen Semantic cut elimination for the logic of bunched implications, formalized in Coq Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
Chen FuFu, Chen Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of SciencesChina EPMC Gets Knowledge in Multi-Agent Systems
Wachara FungwacharakornFungwacharakorn, Wachara National Institute of InformaticsJapan Introduction of PROLEG (PROlog-based LEGal reasoning support system)
Michael FärberFärber, Michael Universität Innsbruck, AustriaAustria Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
G Marco GaboardiGaboardi, Marco Boston UniversityUnited States Session Chair of Semantics 2 (part of POPL ) On Incorrectness Logic and Kleene Algebra with Top and Tests A Separation Logic for Negative Dependence
Emilio Jesús Gallego AriasGallego Arias, Emilio Jesús INRIAFrance Session with the Coq Development Team
Catarina GamboaGamboa, Catarina LASIGE, Faculdade de Ciências da Universidade de Lisboa Understandable and Useful Error Messages for Liquid Types
Ronald GarciaGarcia, Ronald University of British Columbia Committee Member in Program Committee within the POPL -track
Philippa GardnerGardner, Philippa Imperial College LondonUnited Kingdom TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
Deepak GargGarg, Deepak MPI-SWSGermany SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation Pirouette: Higher-Order Typed Functional Choreographies Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI Committee Member in Steering Committee within the PriSC-track
Francesco GavazzoGavazzo, Francesco University of Bologna; InriaItaly A Relational Theory of Effects and Coeffects Effectful Program Distancing
Martin GebserGebser, Martin University of Klagenfurt, AustriaAustria Session Chair of Answer Set Programming (part of PADL) Decomposition-based job-shop scheduling with constrained clustering Committee Member in Programme Committee within the PADL-track
Aina Linn GeorgesGeorges, Aina Linn Aarhus University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jad Elkhaleq GhalayiniGhalayini, Jad Elkhaleq University of CambridgeUnited Kingdom Typechecking up to Congruence
Enrico GhiorziGhiorzi, Enrico Italian Institute of TechnologyItaly (Deep) Induction Rules for GADTs
Roberto GiacobazziGiacobazzi, Roberto University of VeronaItaly Session Chair of Automated Verification (part of POPL ) Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis
Dimitra GiannakopoulouGiannakopoulou, Dimitra NASA Ames Research Center A Compositional Proof Framework for FRETish Requirements
Paolo G. GiarrussoGiarrusso, Paolo G. BedRock Systems A Case for Lightweight Interfaces in Coq
Vladimir GladsteinGladstein, Vladimir MPI-SWS; St. Petersburg University; JetBrains ResearchGermany Truly Stateless, Optimal Dynamic Partial Order Reduction
Robert GlückGlück, Robert University of CopenhagenDenmark Committee Member in Program Committee within the PEPM-track
Stephen GoldbaumGoldbaum, Stephen Morgan StanleyUnited States High Assurance Software for Financial Regulation and Business Platforms
Lior GoldbergGoldberg, Lior Starkware Industries Ltd. A verified algebraic representation of Cairo program execution
Georges GonthierGonthier, Georges Inria Committee Member in Steering Committee within the CPP-track
Lourdes del Carmen González-HuescaGonzález-Huesca, Lourdes del Carmen National Autonomous University of MexicoMexico Committee Member in Program Committee within the CoqPL-track
Alwyn GoodloeGoodloe, Alwyn NASA Langley Research Center Session Chair of Security and Distributed Systems (part of CPP) Committee Member in Program Committee within the CPP-track
Andrew D. GordonGordon, Andrew D. Microsoft Research and University of EdinburghUnited Kingdom Session Chair of Invited talks (part of LAFI) Committee Member in Steering Committee within the LAFI-track
Maria I. GorinovaGorinova, Maria I. The University of Edinburgh Program Analysis of Probabilistic Programs
Léo GourdinGourdin, Léo Université Grenoble-Alpes Formally Verified Superblock Scheduling
Hari Govind V KGovind V K, Hari University of WaterlooCanada Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions
Sebastian GrafGraf, Sebastian Karlsruhe Institute of TechnologyGermany Tries that match
Daniel GratzerGratzer, Daniel Aarhus UniversityDenmark mitten: A Flexible Multimodal Proof Assistant
Ben GreenGreen, Ben University of Michigan Cod(e)ifying The Law
Michael GreenbergGreenberg, Michael Stevens Institute of TechnologyUnited States Committee Member in Programme Committee within the PADL-track
Simon Oddershede GregersenGregersen, Simon Oddershede Aarhus UniversityDenmark Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Radu GrigoreGrigore, Radu FacebookUnited Kingdom Committee Member in Program Committee within the POPL -track
James GrimmelmannGrimmelmann, James Cornell University Research keynote -- Programming Languages and Law: A Research Agenda for a New Field Littleton: An Educational Environment for Property Law Legal Calculi Committee Member in Program Committee within the ProLaLa-track
Richard GrisenthwaiteGrisenthwaite, Richard Armed cats: formal concurrency modelling at Arm
Harrison GrodinGrodin, Harrison Carnegie Mellon UniversityUnited States A Cost-Aware Logical Framework
Jason GrossGross, Jason MIT CSAILUnited States Session with the Coq Development Team Committee Member in Program Committee within the CoqPL-track
Orna GrumbergGrumberg, Orna Technion – Israel Institute of Technology PC Member in Program Committee within the VMCAI-track
Torsten GrustGrust, Torsten University of TübingenGermany Functional Programming on Top of SQL Engines Committee Member in Programme Committee within the PADL-track
Chen GuGu, Chen Hefei University of Technology, China Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Ronghui GuGu, Ronghui Columbia UniversityUnited States Committee Member in Program Committee within the POPL -track
Marco GuarnieriGuarnieri, Marco IMDEA Software InstituteSpain Session Chair of Secure systems (part of PriSC) Session Chair of Short talks (part of PriSC) Session Chair of Keynote II (part of PriSC) Co-chair in Program Committee within the PriSC-track Committee Member in Steering Committee within the PriSC-track
Zheng GuoGuo, Zheng University of California, San Diego Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Gopal GuptaGupta, Gopal The University of Texas at DallasUnited States Modeling and Verification of Real-Time Systems with the Event Calculus and s(CASP) Graph-based Interpretation of Normal Logic Programs Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming
Arie GurfinkelGurfinkel, Arie University of WaterlooCanada Session Chair of Model Checking (part of VMCAI) Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions
Jens Oliver GutsfeldGutsfeld, Jens Oliver Westfälische Wilhelm-Universität Münster (WWU), Germany Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Armaël GuéneauGuéneau, Armaël Aarhus University Committee Member in Program Committee within the PriSC-track Committee Member in Program Committee within the CPP-track
Lennard GäherGäher, Lennard MPI-SWSGermany Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Samuel GélineauGélineau, Samuel SimSpaceCanada Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself
H Thomas HaasHaas, Thomas Technical University of BraunschweigGermany Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Antoine HacquardHacquard, Antoine EPITA, LRDEFrance Armed cats: formal concurrency modelling at Arm
Liana HadareanHadarean, Liana Amazon Web ServicesUnited States PC Member in Program Committee within the VMCAI-track
Matthew HagueHague, Matthew Royal Holloway University of LondonUnited Kingdom Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Committee Member in Program Committee within the POPL -track
Ernst Moritz HahnHahn, Ernst Moritz University of TwenteNetherlands EPMC Gets Knowledge in Multi-Agent Systems
William T. HallahanHallahan, William T. Yale University Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Zhilei HanHan, Zhilei Tsinghua UniversityChina Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Shivam HandaHanda, Shivam Massachusetts Institute of Technology, USA Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Robert HarperHarper, Robert Carnegie Mellon UniversityUnited States A Cost-Aware Logical Framework
William HarrisHarris, William Galois, Inc. PC Member in Program Committee within the VMCAI-track
John HarrisonHarrison, John Intel Committee Member in Program Committee within the CPP-track
Dirk HartungHartung, Dirk Center for Legal Technology and Data Science, Bucerius Law School, Hamburg, Germany Law Smells: Defining and Detecting Problematic Patterns in Legal Drafting
Paul HeHe, Paul University of PennsylvaniaUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Pinjia HeHe, Pinjia The Chinese University of Hong Kong, ShenzhenChina Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Wenlei HeHe, Wenlei FacebookUnited States Profile Inference Revisited
Linus HeckHeck, Linus RWTH Aachen UniversityGermany Gradient-Descent for Randomized Controllers under Partial Observability
İdil Helin ÖzenHelin Özen, İdil Ekol LogisticsTurkey Multi-Agent Pick and Delivery with Capacities: Action Planning vs Path Finding
Joe HendrixHendrix, Joe SRI International Committee Member in Program Committee within the CPP-track
Fritz HengleinHenglein, Fritz Department of Computer Science, University of Copenhagen (DIKU) and Deon DigitalDenmark Welcome & Announcement Committee Member in Steering Committee within the PEPM-track
Thomas A. HenzingerHenzinger, Thomas A. IST Austria, Austria Sequential Information Flow
Kihong HeoHeo, Kihong KAISTSouth Korea Committee Member in Program Committee within the POPL -track
Hugo HerbelinHerbelin, Hugo Session with the Coq Development Team
Manuel HermenegildoHermenegildo, Manuel IMDEA Software Institute and T.U. of Madrid (UPM) Committee Member in Steering Committee within the PEPM-track
Walter HernandezHernandez, Walter Mishcon de Reya,Accord Project Ergo - a programming language for Smart Legal Contracts
Chris HeunenHeunen, Chris University of EdinburghUnited Kingdom Quantum Information Effects
Michael HicksHicks, Michael University of Maryland at College Park Session Chair of Invited Talk (part of POPL ) Session Chair of Quantum Computing (part of POPL ) Session Chair of Junior Faculty Mentoring Breakfast (part of POPL Diversity, Equity and Inclusion) Committee Member in Steering Committee within the PriSC-track
Jonas Kastberg HinrichsenHinrichsen, Jonas Kastberg Aarhus University, DenmarkDenmark Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ralf HinzeHinze, Ralf Technische Universität Kaiserslautern Committee Member in Program Committee within the POPL -track
Denis HirnHirn, Denis University of TübingenGermany Functional Programming on Top of SQL Engines
Andrew K. HirschHirsch, Andrew K. MPI-SWSGermany Pirouette: Higher-Order Typed Functional Choreographies
Aquinas HoborHobor, Aquinas Committee Member in Program Committee within the CPP-track
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the POPL -track
Rasmus Holdsbjerg-LarsenHoldsbjerg-Larsen, Rasmus Aarhus University A Verified Pipeline from a Specification Language to Optimized, Safe Rust
Tony HoskingHosking, Tony Australian National UniversityAustralia POPL Most Influential Paper Award
Kuen-Bang Hou (Favonia)Hou (Favonia), Kuen-Bang University of MinnesotaUnited States Session Chair of Type Theory (part of POPL ) Session Chair of Category Theory, HoTT, Number Theory (part of CPP) Logarithm and Program Testing Panel 1: proof assistants for PL and math
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation Committee Member in Steering Committee within the PriSC-track Steering Committee Chair in Steering Committee within the CPP-track
Justin HsuHsu, Justin Cornell UniversityUnited States A Separation Logic for Negative Dependence Committee Member in Program Committee within the POPL -track
Denghang HuHu, Denghang Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of SciencesChina Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Zhenjiang HuHu, Zhenjiang Peking UniversityChina Committee Member in Steering Committee within the PEPM-track Committee Member in Program Committee within the PEPM-track
Daniel HuangHuang, Daniel Harvard University Committee Member in Program Committee within the LAFI-track
John HuiHui, John Columbia University, New YorkUnited States art in Artifact Evaluation Committee within the VMCAI-track
Mathieu HuotHuot, Mathieu Oxford University Towards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic Languages
Chung-Kil HurHur, Chung-Kil Seoul National UniversitySouth Korea Committee Member in Program Committee within the CoqPL-track
Jennifer Jiyoung HusebyHuseby, Jennifer Jiyoung University of Michigan Cod(e)ifying The Law
I Atsushi IgarashiIgarashi, Atsushi Kyoto University, JapanJapan Committee Member in Steering Committee within the PEPM-track Committee Member in Program Committee within the POPL -track
Mirai IkebuchiIkebuchi, Mirai National Institute of InformaticsJapan Certifying Derivation of State Machines from Coroutines
Daniela InclezanInclezan, Daniela Miami UniversityUnited States Committee Member in Programme Committee within the PADL-track
Apoorv IngleIngle, Apoorv University of IowaUnited States Video Chair in Organizing Committee for POPL 2022
Ahmed IrfanIrfan, Ahmed Stanford UniversityUnited States Bit-Precise Reasoning via Int-Blasting
Yusuke IzawaIzawa, Yusuke Tokyo Institute of TechnologyJapan Two-level Just-in-Time Compilation with One Interpreter and One Engine
J Jules JacobsJacobs, Jules Radboud University NijmegenNetherlands Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic
Junyoung JangJang, Junyoung McGill UniversityCanada Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself
Tomi JanhunenJanhunen, Tomi Tampere UniversityFinland Implementing Stable-Unstable Semantics with ASPTOOLS and Clingo
Alan JeffreyJeffrey, Alan RobloxUnited States Session Chair of Semantics 1 (part of POPL ) Session Chair of Functional and Logic Programming (part of PADL) The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Nikolaj Jensen UlrikJensen Ulrik, Nikolaj Aalborg UniversityDenmark Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking
Peter Gjøl JensenJensen, Peter Gjøl Aalborg University, DenmarkDenmark Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking
Thomas P. JensenJensen, Thomas P. INRIA Rennes Type-directed Program Transformation for Constant-Time Enforcement
Minseok JeonJeon, Minseok Korea UniversitySouth Korea Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented Programs
Somesh JhaJha, Somesh University of WisconsinUnited States Interval Universal Approximation for Neural Networks
Ranjit JhalaJhala, Ranjit University of California at San DiegoUnited States Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI Committee Member in Program Committee within the POPL -track
Xiaodong JiaJia, Xiaodong Hunan UniversityChina Semantics for Variational Quantum Programming
Patricia JohannJohann, Patricia Appalachian State University (Deep) Induction Rules for GADTs
Brittany JohnsonJohnson, Brittany George Mason UniversityUnited States Designing and Developing for the Black Experience
Daniel D. JohnsonJohnson, Daniel D. Google ResearchCanada Parallel Algebraic Effect Handlers
Evan JohnsonJohnson, Evan University of California at San DiegoUnited States Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Ralf JungJung, Ralf MPI-SWSGermany Panel (live only, no recording) Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Panelist in Panelists within the PLMW-track Committee Member in Program Committee within the CPP-track
Sebastian JungesJunges, Sebastian University of California, BerkeleyUnited States Gradient-Descent for Randomized Controllers under Partial Observability
David JustoJusto, David Microsoft AzureUnited States Session Chair of ShutdownPL (part of POPL Diversity, Equity and Inclusion)
K Robin KaarsgaardKaarsgaard, Robin University of EdinburghUnited Kingdom Quantum Information Effects
David M. KahnKahn, David M. Carnegie Mellon UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Łukasz KaiserKaiser, Łukasz OpenAI Keynote 1: OpenAI Codex presentation & demo
Cezary KaliszykKaliszyk, Cezary University of Innsbruck Committee Member in Program Committee within the CPP-track
Konstantinos KallasKallas, Konstantinos University of Pennsylvania Student Volunteer Co-Chair in Organizing Committee for POPL 2022
Yukiyoshi KameyamaKameyama, Yukiyoshi University of TsukubaJapan Committee Member in Program Committee within the PEPM-track Committee Member in Programme Committee within the PADL-track
Benjamin Lucien KaminskiKaminski, Benjamin Lucien Saarland University and University College LondonGermany Committee Member in Program Committee within the POPL -track
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom Session Chair of Keynote (part of LAFI) Session Chair of Keynote (part of LAFI) Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations Committee Member in Steering Committee within the LAFI-track
Shuanglong KanKan, Shuanglong TU KaiserslauternGermany CertiStr: A Certified String Solver Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Jeehoon KangKang, Jeehoon KAISTSouth Korea Student Research Competition Co-Chair in Organizing Committee for POPL 2022 Session Chair of Verified Data Structures and Semantics (part of CPP) Panel 2: the future of concurrency and parallelism Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Co-chair in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the CPP-track
Toghrul KarimovKarimov, Toghrul MPI-SWSGermany What’s Decidable about Linear Loops?
Jacek KarwowskiKarwowski, Jacek University of WarsawPoland Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Gradient-Descent for Randomized Controllers under Partial Observability Out of Control: Reducing Probabilistic Models by Control-State Elimination
Shin-ya KatsumataKatsumata, Shin-ya National Institute of InformaticsJapan Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations Committee Member in Program Committee within the POPL -track
Daniel Martin KatzKatz, Daniel Martin Illinois Tech – Chicago Kent College of Law, Chicago, IL, USA Law Smells: Defining and Detecting Problematic Patterns in Legal Drafting
Ryan KavanaghKavanagh, Ryan McGill UniversityCanada Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Alex KavvosKavvos, Alex University of BristolUnited Kingdom Committee Member in Program Committee within the POPL -track
Ilya KaysinKaysin, Ilya JetBrains Research; University of CambridgeRussia The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Gabriele KellerKeller, Gabriele Utrecht UniversityNetherlands Committee Member in Program Committee within the PEPM-track
Ariel E. KellisonKellison, Ariel E. Cornell UniversityUnited States A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem
Andrew KennedyKennedy, Andrew Facebook LondonUnited Kingdom Committee Member in Program Committee within the POPL -track
Delia KesnerKesner, Delia Université de Paris; CNRS; IRIF; Institut Universitaire de FranceFrance A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-Nets
Johannes KinderKinder, Johannes Bundeswehr University MunichGermany Committee Member in Program Committee within the PriSC-track
Dominik KirstKirst, Dominik Saarland UniversityGermany Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq
Oleg KiselyovKiselyov, Oleg Tohoku University, Japan let (rec) insertion without Effects, Lights or Magic
Maxime KjaerKjaer, Maxime EPFLSwitzerland Type-Level Programming with Match Types
Adam Husted KjelstrømKjelstrøm, Adam Husted Aarhus UniversityDenmark The Decidability and Complexity of Interleaved Bidirected Dyck Reachability
Christoph KleeKlee, Christoph Facebook Applying Formal Verification to Microkernel IPC at Meta
Gerwin KleinKlein, Gerwin Proofcraft and UNSW SydneyAustralia Committee Member in Steering Committee within the CPP-track
Andrei KlimovKlimov, Andrei Keldysh Institute of Applied Mathematics of Russian Academy of SciencesRussia Why are partial evaluation and supercompilation still not widely used in practice? Reflections in light of Russian work on metacomputation.
Hsiang-Shang ‘Josh’ KoKo, Hsiang-Shang ‘Josh’ Institute of Information Science, Academia SinicaTaiwan Committee Member in Steering Committee within the PEPM-track
Naoki KobayashiKobayashi, Naoki University of Tokyo, JapanJapan On Type-Based Techniques for Program Manipulation
Mark KochKoch, Mark Saarland University Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq
Jason R. KoenigKoenig, Jason R. Stanford UniversityUnited States Induction Duality: Primal-Dual Search for Invariants
Jérémie KoenigKoenig, Jérémie Yale UniversityUnited States Layered and Object-Based Game Semantics Verified Compilation of C Programs with a Nominal Memory Model
Wen KokkeKokke, Wen University of Edinburgh Panel (live only, no recording) Panelist in Panelists within the PLMW-track
Michalis KokologiannakisKokologiannakis, Michalis MPI-SWSGermany Truly Stateless, Optimal Dynamic Partial Order Reduction
Matthew KolosickKolosick, Matthew University of California at San DiegoUnited States Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University, UK Committee Member in Programme Committee within the PADL-track
Chaitanya S. KoparkarKoparkar, Chaitanya S. Indiana UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Andre KornellKornell, Andre Tulane UniversityUnited States Semantics for Variational Quantum Programming
Paulette KoronkevichKoronkevich, Paulette University of British Columbia Dependent-Type-Preserving Memory Allocation
Adrien KoutsosKoutsos, Adrien INRIA Paris Committee Member in Program Committee within the PriSC-track
Laura KovacsKovacs, Laura Vienna University of Technology (TU Wien)Austria PC Member in Program Committee within the VMCAI-track
András KovácsKovács, András Eötvös Loránd University Committee Member in Program Committee within the WITS-track
Robert KowalskiKowalski, Robert Imperial College London Logical English as a Programming Language for the Law
Elisavet KozyriKozyri, Elisavet Arctic University of NorwayNorway Committee Member in Program Committee within the PriSC-track
Faustyna KrawiecKrawiec, Faustyna University of CambridgeUnited Kingdom Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands Session Chair of Chairs' Report and Business Meeting (part of CPP) Session Chair of Welcome from the chairs (part of CPP) Session Chair of Morning 1 (part of PLMW) VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic Committee Member in Organizing Committee within the PLMW-track Conference Chair in Organization Committee within the CPP-track
Matthias KrebsKrebs, Matthias TU DarmstadtGermany Dependently-Typed Data Plane Programming
Jan KretinskyKretinsky, Jan Technical University of MunichGermany PC Member in Program Committee within the VMCAI-track
Siddharth KrishnaKrishna, Siddharth Microsoft ResearchUnited Kingdom PC Member in Program Committee within the VMCAI-track
Shriram KrishnamurthiKrishnamurthi, Shriram Brown University, United States Declarative Programming and Education
Neel KrishnaswamiKrishnaswami, Neel University of CambridgeUnited Kingdom CN: A Refinement Type System for C Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation Committee Member in Program Committee within the POPL -track
Paul KrogmeierKrogmeier, Paul University of Illinois at Urbana-ChampaignUnited States Learning Formulas in Finite Variable Logics
Matthis KruseKruse, Matthis CISPA Helmholtz Center for Information SecurityGermany Composing Secure Compilers
Piotr KrysiukKrysiuk, Piotr Symantec, Threat Hunter Team BPF and Spectre: Mitigating transient execution attacks
Viktor KunčakKunčak, Viktor EPFL, SwitzerlandSwitzerland Session Chair of Synthesis (part of VMCAI) NP Satisfiability for Arrays as Powers Generalized Arrays for Stainless Frames
L Ori LahavLahav, Ori Tel Aviv UniversityIsrael Committee Member in Program Committee within the POPL -track
Shuvendu K. LahiriLahiri, Shuvendu K. Microsoft ResearchUnited States SolType: Refinement Types for Arithmetic Overflow in Solidity
Alejandro Flores LamasLamas, Alejandro Flores Royal Holloway University of LondonUnited Kingdom Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Leonidas LampropoulosLampropoulos, Leonidas University of Maryland, College ParkGreece Committee Member in Program Committee within the CoqPL-track Committee Member in Program Committee within the POPL -track
Cosimo LaneveLaneve, Cosimo University of Bologna Stipula: a domain specific language for legal contracts
Sam LasserLasser, Sam Tufts UniversityUnited States Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives
Jacob LaurelLaurel, Jacob University of Illinois at Urbana-ChampaignUnited States A Dual Number Abstraction for Static Analysis of Clarke Jacobians
Mickaël LaurentLaurent, Mickaël Université de ParisFrance On Type-Cases, Union Elimination, and Occurrence Typing
Julia LawallLawall, Julia InriaFrance Session Chair of Keynote 5 (part of PEPM) Committee Member in Program Committee within the PEPM-track
Sarah LawskyLawsky, Sarah Northwestern UniversityUnited States Program Co-Chair in Program Committee within the ProLaLa-track
Xuan-Bach LeLe, Xuan-Bach Nanyang Technological UniversitySingapore A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
Woosuk LeeLee, Woosuk Hanyang UniversitySouth Korea Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the POPL -track
Engel LefaucheuxLefaucheux, Engel MPI-SWSGermany What’s Decidable about Linear Loops?
Johannes LehmannLehmann, Johannes RWTH Aachen UniversityGermany Out of Control: Reducing Probabilistic Models by Control-State Elimination
K. Rustan M. LeinoLeino, K. Rustan M. AmazonUnited States Tutorial 2: some advanced features of the Dafny verification tool
Michael LeMayLeMay, Michael Intel LabsUnited States Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthieu LemerreLemerre, Matthieu CEA LIST, FranceFrance Lightweight Shape Analysis based on Physical Types
Sergueï LengletLenglet, Sergueï Université de Lorraine, France Certified Abstract Machines for Skeletal Semantics
Meven Lennon-BertrandLennon-Bertrand, Meven Inria – LS2N, Université de NantesFrance À bas l’η — Coq’s troublesome η-conversion The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoq Gradualizing the Calculus of Inductive Constructions
Nicola LeoneLeone, Nicola University of Calabria, ItalyItaly Smart Devices and Large Scale Reasoning via ASP: Tools and Applications
Rodolphe LepigreLepigre, Rodolphe MPI-SWSGermany VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Xavier LeroyLeroy, Xavier Collège de FranceFrance Committee Member in Program Committee within the CoqPL-track
David LevitLevit, David Starkware Industries Ltd. A verified algebraic representation of Cairo program execution
Alexander K. LewLew, Alexander K. Massachusetts Institute of Technology, USAUnited States Towards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic Languages
Fang LiLi, Fang The University of Texas at DallasUnited States Modeling and Verification of Real-Time Systems with the Event Calculus and s(CASP) Graph-based Interpretation of Normal Logic Programs
Xuandong LiLi, Xuandong Nanjing UniversityChina Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata
Yao LiLi, Yao University of PennsylvaniaUnited States Effect-Oblivious Equivalence The Expression Problem and Theorem Proving (discussion) Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yong LiLi, Yong Institute of Software, Chinese Academy of SciencesChina EPMC Gets Knowledge in Multi-Agent Systems
Yuanbo LiLi, Yuanbo Georgia Institute of TechnologyUnited States Efficient Algorithms for Dynamic Bidirected Dyck-Reachability Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Hongjin LiangLiang, Hongjin Nanjing UniversityChina Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the CPP-track
Jay P. LimLim, Jay P. Rutgers UniversityUnited States One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes
Anthony Widjaja LinLin, Anthony Widjaja TU Kaiserslautern; MPI-SWSGermany CertiStr: A Certified String Solver Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Committee Member in Program Committee within the POPL -track
Shang-Wei LinLin, Shang-Wei Nanyang Technological UniversitySingapore A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
Bert LindenhoviusLindenhovius, Bert JKU LinzAustria Semantics for Variational Quantum Programming
Sam LindleyLindley, Sam The University of Edinburgh, UKUnited Kingdom Session Chair of Keynote 1 (part of PEPM) Committee Member in Steering Committee within the PEPM-track
Alice LiuLiu, Alice University of Michigan Cod(e)ifying The Law
Amanda LiuLiu, Amanda Massachusetts Institute of TechnologyUnited States Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
Depeng LiuLiu, Depeng Institute of Software, Chinese Academy of SciencesChina Verifying Pufferfish Privacy in Hidden Markov Models
Fangfei LiuLiu, Fangfei Intel Corporation Towards Understanding Spectre-PHT in Memory-Safe Languages
Y. Annie LiuLiu, Y. Annie Stony Brook UniversityUnited States From meta frameworks and transformations to distributed computing and more Committee Member in Program Committee within the PEPM-track
Devon LoehrLoehr, Devon Princeton UniversityUnited States Safe, Modular Packet Pipeline Programming
Fan LongLong, Fan University of Toronto, Canada Committee Member in Program Committee within the POPL -track
Anna LukinaLukina, Anna TU Delft PC Member in Program Committee within the VMCAI-track
Linghui LuoLuo, Linghui Amazon Web ServicesGermany Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ning LuoLuo, Ning Session Chair of Tutorials 1 (part of POPL TutorialFest) Session Chair of Tutorials 2 (part of POPL TutorialFest)
Weiyu LuoLuo, Weiyu University of California, IrvineUnited States Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not Terminate
Matthew LutzeLutze, Matthew Université de ParisFrance On Type-Cases, Union Elimination, and Occurrence Typing
Andres LöhLöh, Andres Well-Typed LLPUnited Kingdom Staging with Class: A Specification for Typed Template Haskell Committee Member in Programme Committee within the PADL-track
M Mohammed M. S. El-KholanyM. S. El-Kholany, Mohammed University of KlagenfurtAustria Decomposition-based job-shop scheduling with constrained clustering
Dougal MaclaurinMaclaurin, Dougal Google Research Parallel Algebraic Effect Handlers
P. MadhusudanMadhusudan, P. University of Illinois at Urbana-ChampaignUnited States Learning Formulas in Finite Variable Logics Committee Member in Program Committee within the POPL -track
Jean-Marie MadiotMadiot, Jean-Marie InriaFrance A Separation Logic for Heap Space under Garbage Collection
Avishkar MahajanMahajan, Avishkar Singapore Management University Overview of the CCLAW L4 project
Assia MahboubiMahboubi, Assia INRIAFrance Committee Member in Steering Committee within the CPP-track
Kenji MaillardMaillard, Kenji Inria Nantes & University of Chile Gradualizing the Calculus of Inductive Constructions
Rupak MajumdarMajumdar, Rupak MPI-SWSGermany Session Chair of Formal Methods in Machine Learning (part of VMCAI) Context-Bounded Verification of Thread Pools Subcubic Certificates for CFL Reachability
Carol MakMak, Carol University of Oxford Nonparametric Involutive Markov Chain Monte Carlo
Gleb MakarchukMakarchuk, Gleb ETH ZurichSwitzerland PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
Dhruv MakwanaMakwana, Dhruv University of Cambridge CN: A Refinement Type System for C
Gregory MalechaMalecha, Gregory BedRock SystemsUnited States A Case for Lightweight Interfaces in Coq Committee Member in Program Committee within the CPP-track
Makai MannMann, Makai Stanford UniversityUnited States Bit-Precise Reasoning via Int-Blasting
Vikash K. MansinghkaMansinghka, Vikash K. MIT Towards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic Languages
Luc MarangetMaranget, Luc InriaFrance Armed cats: formal concurrency modelling at Arm Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores
Marco MarateaMaratea, Marco DIBRIS, University of GenovaItaly Committee Member in Programme Committee within the PADL-track
Roy MargalitMargalit, Roy Tel Aviv University, Israel Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Benjamin MarianoMariano, Benjamin University of Texas at AustinUnited States SolType: Refinement Types for Arithmetic Overflow in Solidity
Iason MarmanisMarmanis, Iason MPI-SWSGermany Truly Stateless, Optimal Dynamic Partial Order Reduction
Yoann MarquerMarquer, Yoann INRIA, Rennes, France Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Mark MarronMarron, Mark Microsoft ResearchUnited States High Assurance Software for Financial Regulation and Business Platforms
Danielle MarshallMarshall, Danielle University of Kent, UKUnited Kingdom Linearity, Uniqueness, Ownership: An Entente Cordiale
Hidehiko MasuharaMasuhara, Hidehiko Tokyo Institute of TechnologyJapan Two-level Just-in-Time Compilation with One Interpreter and One Engine Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)
Nicholas MatsakisMatsakis, Nicholas AWSUnited States Implementing Languages for Fun and Profit Invited Speaker in Invited speakers within the PLMW-track
Ralph MatthesMatthes, Ralph IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, ToulouseFrance Implementing a category-theoretic framework for typed abstract syntax
Damiano MazzaMazza, Damiano CNRSFrance Session Chair of Invited talks (part of LAFI) Programming Languages for Automatic Differentiation: What Now?
Giuseppe MazzottaMazzotta, Giuseppe University of CalabriaItaly Modelling the Outlier Detection Problem in QASP
L. Thorne McCartyMcCarty, L. Thorne Rutgers, The State University of New Jersey Position Paper: LLD is All You Need
Kenneth L. McMillanMcMillan, Kenneth L. University of Texas at AustinUnited States Induction Duality: Primal-Dual Search for Invariants Committee Member in Program Committee within the POPL -track
Christopher McNallyMcNally, Christopher Massachusetts Institute of TechnologyUnited States Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
Simon Mejlby VirenfeldtMejlby Virenfeldt, Simon Aalborg UniversityDenmark Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking
Paul-André MellièsMelliès, Paul-André CNRS; Université de ParisFrance Layered and Object-Based Game Semantics
Kayvan MemarianMemarian, Kayvan University of CambridgeUnited Kingdom CN: A Refinement Type System for C VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
Baoluo MengMeng, Baoluo GE Research Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Denis MerigouxMerigoux, Denis INRIAFrance Turning Catala into a Proof Platform for the Law Committee Member in Program Committee within the ProLaLa-track
Julián MestreMestre, Julián Facebook; University of SydneyUnited States Profile Inference Revisited
Roland MeyerMeyer, Roland TU Braunschweig PC Member in Program Committee within the VMCAI-track
Mira MeziniMezini, Mira TU DarmstadtGermany Dependently-Typed Data Plane Programming
Attila MihalyMihaly, Attila Morgan StanleyUnited States High Assurance Software for Financial Regulation and Business Platforms
Sam MikellMikell, Sam University of Michigan Cod(e)ifying The Law
Mae MilanoMilano, Mae University of California, Berkeley Session Chair of Weak Memory Models (part of POPL )
Mihails MilehinsMilehins, Mihails An Extension of the Framework Types-To-Sets for Isabelle/HOL
Alexander MillerMiller, Alexander University of Michigan Cod(e)ifying The Law
Dale MillerMiller, Dale INRIA Saclay and LIXFrance Committee Member in Steering Committee within the CPP-track
Mikkel MiloMilo, Mikkel Concordium Blockchain Research Center, Aarhus University A Verified Pipeline from a Specification Language to Optimized, Safe Rust
Anders MiltnerMiltner, Anders University of Texas at AustinUnited States Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Solène MirliazMirliaz, Solène ENS Rennes / IRISA / InriaFrance A Flow-Insensitive-Complete Program Representation
Matthew MirmanMirman, Matthew ETH ZurichSwitzerland Formal Methods and Deep Learning [Part A]
Sasa MisailovicMisailovic, Sasa University of Illinois at Urbana-ChampaignUnited States A Dual Number Abstraction for Static Analysis of Clarke Jacobians
Michael MisloveMislove, Michael Tulane UniversityUnited States Semantics for Variational Quantum Programming
Neil MitchellMitchell, Neil Meta Forward build systems, formally
Stefan MitschMitsch, Stefan Carnegie Mellon University, USAUnited States Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned Systems
Joshua MoermanMoerman, Joshua Open University of the NetherlandsNetherlands Gradient-Descent for Randomized Controllers under Partial Observability
Torben MogensenMogensen, Torben DIKU, University of CopenhagenDenmark Committee Member in Steering Committee within the PEPM-track
Sidi Mohamed BeillahiMohamed Beillahi, Sidi University of TorontoCanada Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Anshuman MohanMohan, Anshuman Cornell UniversityUnited States Littleton: An Educational Environment for Property Law Legal Calculi
Alexandre MoineMoine, Alexandre InriaFrance Specification and Verification of a Transient Stack
David MonniauxMonniaux, David CNRS/VERIMAGFrance Formally Verified Superblock Scheduling
Stefan MonnierMonnier, Stefan Université de MontréalCanada Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself
Scott MooreMoore, Scott Galois, Inc.United States Synthesizing Evidence of Emergent Computation Committee Member in Program Committee within the PriSC-track
Michael MorakMorak, Michael University of KlagenfurtAustria Determining Action Reversibility in STRIPS Using Answer Set Programming with Quantifiers
Andreia MordidoMordido, Andreia Lasige / Faculty of Sciences, Universidade de Lisboa Deciding type equivalence with simple grammars
Mar Moreno-RebatoMoreno-Rebato, Mar Universidad Rey Juan Carlos Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
J. Garrett MorrisMorris, J. Garrett The University of IowaUnited States Session Chair of Distributed or Network Programs (part of POPL ) Committee Member in Program Committee within the POPL -track
Jason MorrisMorris, Jason Service Canada, Lexpedite Legal Technology Prevalence of Expression Types in Legislative Text
Mariano MoscatoMoscato, Mariano National Institute of Aerospace Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Reed MullanixMullanix, Reed University of Minnesota Setting the Record Straight with Singletons
Stefan K. MullerMuller, Stefan K. Illinois Institute of TechnologyUnited States Static Prediction of Parallel Computation Graphs
Dominic MulliganMulligan, Dominic Arm ResearchUnited Kingdom The Supervisionary proof-checking kernel, or: a work-in-progress toward proof-generating code
Cesar MunozMunoz, Cesar AWSUnited States Structural Embeddings Revisited
Adithya MuraliMurali, Adithya University of Illinois at Urbana-Champaign Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Koko MuroyaMuroya, Koko RIMS, Kyoto UniversityJapan Committee Member in Program Committee within the POPL -track
Lawrence MurrayMurray, Lawrence Uber Committee Member in Program Committee within the LAFI-track
Toby MurrayMurray, Toby University of MelbourneAustralia Committee Member in Program Committee within the PriSC-track Committee Member in Program Committee within the CPP-track
Noble MushtakMushtak, Noble Northeastern University A Realizability Model for Interoperability Between Languages with Garbage-Collected and Manually Managed Memory
Andrew MyersMyers, Andrew Cornell University Session Chair of Concurrency and Parallelism (part of POPL ) Session Chair of TOPLAS Session (part of POPL ) Session Chair of Graduating PhDs / Postdocs Mentoring Breakfast (part of POPL Diversity, Equity and Inclusion) POPL 2023 Report Committee Member in Program Committee within the PriSC-track
Chris MyersMyers, Chris University of Colorado, BoulderUnited States STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model Checking
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology Committee Member in Steering Committee within the CPP-track
Anders MörtbergMörtberg, Anders Department of Mathematics, Stockholm UniversitySweden Implementing a category-theoretic framework for typed abstract syntax Committee Member in Program Committee within the CPP-track
Markus Müller-OlmMüller-Olm, Markus University of MünsterGermany PC Member in Program Committee within the VMCAI-track
N Santosh NagarakatteNagarakatte, Santosh Rutgers UniversityUnited States One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes Committee Member in Steering Committee within the PriSC-track
Keiko NakataNakata, Keiko SAP Innovation Center PotsdamGermany Session Chair of Keynote 3 (part of PEPM) Committee Member in Program Committee within the PEPM-track
Aleksandar NanevskiNanevski, Aleksandar IMDEA Software InstituteSpain Visibility Reasoning for Concurrent Snapshot Algorithms
Monal NarasimhamurthyNarasimhamurthy, Monal University of Colorado, BoulderUnited States Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Nicolas NardinoNardino, Nicolas École normale supérieure de Lyon Formally Verified Superblock Scheduling
Oliver NashNash, Oliver Imperial College, London Formalising Lie algebras
Jorge A. NavasNavas, Jorge A. Certora, inc.United States Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE PC Member in Program Committee within the VMCAI-track
Luke NelsonNelson, Luke University of WashingtonUnited States A Formal Foundation for Symbolic Evaluation with Merging
Antonina NepeivodaNepeivoda, Antonina Program Systems Institute of RAS, RussiaRussia Session Chair of Contributed Talks 1 (part of PEPM) Committee Member in Program Committee within the PEPM-track
Thakur NeupaneNeupane, Thakur The MathWorks, Inc.United States STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model Checking
Minh NguyenNguyen, Minh University of BristolUnited Kingdom Linked Visualisations via Galois Dependencies
Kim NguyễnNguyễn, Kim Université Paris-SaclayFrance On Type-Cases, Union Elimination, and Occurrence Typing
Olivier NicoleNicole, Olivier CEA LIST, FranceFrance Lightweight Shape Analysis based on Physical Types
Victor NicoletNicolet, Victor University of TorontoCanada Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Aina NiemetzNiemetz, Aina Stanford UniversityUnited States Bit-Precise Reasoning via Int-Blasting
Mark Niklas MüllerNiklas Müller, Mark ETH ZurichSwitzerland PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
Tobias NipkowNipkow, Tobias Technische Universität München Committee Member in Steering Committee within the CPP-track
Yue NiuNiu, Yue Carnegie Mellon UniversityUnited States A Cost-Aware Logical Framework
Andres NötzliNötzli, Andres Stanford University, USAUnited States Bit-Precise Reasoning via Int-Blasting
O Liam O'ConnorO'Connor, Liam University of EdinburghUnited Kingdom Writing Valuable Papers Overcoming Restraint: Composing Verification of Foreign Functions with Cogent Invited Speaker in Invited speakers within the PLMW-track
Peter W. O'HearnO'Hearn, Peter W. Meta; University College LondonUnited Kingdom Applying Formal Verification to Microkernel IPC at Meta Concurrent Incorrectness Separation Logic
Martin OderskyOdersky, Martin EPFLSwitzerland Type-Level Programming with Match Types
Hakjoo OhOh, Hakjoo Korea UniversitySouth Korea Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented Programs Tutorial 1: Data-driven program analysis: combining machine learning and program analysis
Arthur Oliveira ValeOliveira Vale, Arthur Yale UniversityUnited States Layered and Object-Based Game Semantics
Martina OlliaroOlliaro, Martina Ca' Foscari University of Venice - Department of Environmental Sciences, Informatics and StatisticsItaly Relational String Abstract Domains
Jan OnderkaOnderka, Jan Czech Technical University in Prague Fast Three-Valued Abstract Bit-Vector Arithmetic
C.-H. Luke OngOng, C.-H. Luke University of OxfordUnited Kingdom A Language and Smoothed Semantics for Convergent Stochastic Gradient Descent Rigorous Approximation of Posterior Inference for Probabilistic Programs Nonparametric Involutive Markov Chain Monte Carlo Committee Member in Program Committee within the POPL -track
Sascha OssowskiOssowski, Sascha Universidad Rey Juan Carlos Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
Joël OuaknineOuaknine, Joël MPI-SWSGermany What’s Decidable about Linear Loops?
P Oded PadonPadon, Oded VMware Research; Stanford UniversityUnited States Induction Duality: Primal-Dual Search for Invariants PC Member in Program Committee within the VMCAI-track
Luca PadovaniPadovani, Luca University of TurinItaly Fair Termination of Binary Sessions
Brooks PaigePaige, Brooks University College London Committee Member in Program Committee within the LAFI-track
Jens PalsbergPalsberg, Jens University of California at Los AngelesUnited States PC Member in Program Committee within the VMCAI-track
Pavel PanchekhaPanchekha, Pavel University of UtahUnited States Artifact Evaluation Co-Chair in Organizing Committee for POPL 2022 Committee Member in Program Committee within the POPL -track Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Hugo PaquetPaquet, Hugo University of Cambridge Stateful processes in probabilistic programming
Zoe ParaskevopoulouParaskevopoulou, Zoe Northeastern UniversityUnited States Committee Member in Program Committee within the PEPM-track Committee Member in Program Committee within the CPP-track
Matthew J. ParkinsonParkinson, Matthew J. Microsoft Research, UKUnited Kingdom Committee Member in Program Committee within the POPL -track
Lionel ParreauxParreaux, Lionel Hong Kong University of Science and Technology Committee Member in Programme Committee within the PADL-track
Matteo PascucciPascucci, Matteo Slovak Academy of Science DPCL: a Language Template for Normative Specifications
Adam PaszkePaszke, Adam Google ResearchPoland Parallel Algebraic Effect Handlers
Volkan PatoğluPatoğlu, Volkan Sabanci UniversityTurkey Multi-Agent Pick and Delivery with Capacities: Action Planning vs Path Finding
Marco PatrignaniPatrignani, Marco CISPA Helmholtz Center for Information Security / Stanford University Composing Secure Compilers
Andreas PavlogiannisPavlogiannis, Andreas Aarhus UniversityDenmark The Decidability and Complexity of Interleaved Bidirected Dyck Reachability
Jennifer PaykinPaykin, Jennifer Galois, Inc.United States Accessibility, Diversity and Inclusion Chair in Organizing Committee for POPL 2022 Synthesizing Evidence of Emergent Computation
Roly PereraPerera, Roly Alan Turing InstituteUnited Kingdom Linked Visualisations via Galois Dependencies Committee Member in Programme Committee within the PADL-track
Simona PerriPerri, Simona University of Calabria, Italy Session Chair of Invited talk (part of PADL) Program Co-Chair in Programme Chairs within the PADL-track
Tomas PetricekPetricek, Tomas University of KentUnited Kingdom Linked Visualisations via Galois Dependencies Committee Member in Programme Committee within the PADL-track
Simon Peyton JonesPeyton Jones, Simon Microsoft ResearchUnited Kingdom Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Frank PfenningPfenning, Frank Carnegie Mellon University, USA Modal Logics and Types: Looking Back and Looking Forward
David PichardiePichardie, David Facebook ParisFrance A Flow-Insensitive-Complete Program Representation Committee Member in Program Committee within the PriSC-track
Jean Pichon-PharabodPichon-Pharabod, Jean Aarhus University CN: A Refinement Type System for C
Matthew PickeringPickering, Matthew Well-Typed LLPUnited Kingdom Staging with Class: A Specification for Typed Template Haskell
Brigitte PientkaPientka, Brigitte McGill UniversityCanada Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself Committee Member in Program Committee within the CPP-track
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States Session Chair of Contributed Talks (Morning) (part of CoqPL) Session Chair of Invited Talk I (part of CoqPL) Co-chair in Organizing Committee within the CoqPL-track
Frank PiessensPiessens, Frank KU Leuven Providing evidence for the security properties of hardware/software codesigns
Keshav PingaliPingali, Keshav The University of Texas at Austin Panel 2: the future of concurrency and parallelism
Ruzica PiskacPiskac, Ruzica Yale UniversityUnited States Workshops Co-Chair in Organizing Committee for POPL 2022 Committee Member in Program Committee within the ProLaLa-track Publicity Chair in Organizing Committee within the VMCAI-track Co-chair in Tutorial Evaluation Committee within the POPL TutorialFest-track
Clément Pit-ClaudelPit-Claudel, Clément MIT / AWSUnited States Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofs Invited Speaker in Invited speaker within the CoqPL-track
Andreas PodelskiPodelski, Andreas University of Freiburg, GermanyGermany PC Member in Program Committee within the VMCAI-track
Anton PodkopaevPodkopaev, Anton HSE UniversityRussia The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency Committee Member in Selection Committee within the POPL Student Research Competition-track
Elizabeth PolgreenPolgreen, Elizabeth University of EdinburghUnited Kingdom Session Chair of Program Verification (part of VMCAI) Satisfiability and Synthesis Modulo Oracles
Hernán Ponce de LeónPonce de León, Hernán Bundeswehr University MunichGermany Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Enrico PontelliPontelli, Enrico Parallel Declarative Solutions of Sequencing Problems using Multi-valued Decision Diagrams and GPUs
Andrei PopescuPopescu, Andrei University of SheffieldUnited Kingdom Session Chair of Chairs' Report and Business Meeting (part of CPP) Session Chair of Invited Talk (part of CPP) Session Chair of Formalization of Logic, Algebra and Geometry (part of CPP) Session Chair of Welcome from the chairs (part of CPP) PC Chair in Program Committee within the CPP-track PC Chair in Organization Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
Sorawee PorncharoenwasePorncharoenwase, Sorawee University of WashingtonUnited States A Formal Foundation for Symbolic Evaluation with Merging
François PottierPottier, François InriaFrance Panel (live only, no recording) Specification and Verification of a Transient Stack A Separation Logic for Heap Space under Garbage Collection Panelist in Panelists within the PLMW-track Committee Member in Program Committee within the POPL -track
Pavithra PrabhakarPrabhakar, Pavithra Kansas State UniversityUnited States Session Chair of Probabilistic Systems (part of VMCAI) Bisimulations for Neural Network Reduction PC Member in Program Committee within the VMCAI-track
Gautam PrakriyaPrakriya, Gautam Chinese University of Hong KongChina Interval Universal Approximation for Neural Networks
Mathias PreinerPreiner, Mathias Stanford UniversityUnited States Bit-Precise Reasoning via Int-Blasting
Thomas PressburgerPressburger, Thomas NASA ARC A Compositional Proof Framework for FRETish Requirements
Jonathan Prieto-CubidesPrieto-Cubides, Jonathan University of BergenNorway On homotopy of walks and spherical maps in homotopy type theory
Jonathan ProtzenkoProtzenko, Jonathan Microsoft Research, RedmondUnited States Session Chair of Verification 2 (part of POPL ) Session Chair of Keynote I (part of PriSC) Session Chair of Attacks and defenses (part of PriSC) Session Chair of Long talks #4 (part of ProLaLa) Session Chair of Long talks #5 (part of ProLaLa) Session Chair of Long talks #1 (part of ProLaLa) Session Chair of Industry keynote (part of ProLaLa) Session Chair of Long talks #2 (part of ProLaLa) Session Chair of Research keynote (part of ProLaLa) Session Chair of Long talks #3 (part of ProLaLa) Session Chair of Short talks (part of ProLaLa) Program Co-Chair in Program Committee within the ProLaLa-track Co-chair in Program Committee within the PriSC-track Committee Member in Steering Committee within the PriSC-track
Loïc PujetPujet, Loïc InriaFrance Observational Equality: Now for Good
Christopher PultePulte, Christopher University of Cambridge, UK CN: A Refinement Type System for C
Sergey PupyrevPupyrev, Sergey United States Profile Inference Revisited
David PurserPurser, David MPI-SWSGermany What’s Decidable about Linear Loops?
Pierre-Marie PédrotPédrot, Pierre-Marie INRIA Committee Member in Program Committee within the WITS-track
Markus PüschelPüschel, Markus ETH ZurichSwitzerland PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
Corina S. PăsăreanuPăsăreanu, Corina S. Carnegie Mellon UniversityUnited States PC Member in Program Committee within the VMCAI-track
R Azalea RaadRaad, Azalea Imperial College LondonUnited Kingdom Student Research Competition Co-Chair in Organizing Committee for POPL 2022 Student Research Competition Winners Concurrent Incorrectness Separation Logic Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores Co-chair in Selection Committee within the POPL Student Research Competition-track
Jonathan Ragan-KelleyRagan-Kelley, Jonathan Massachusetts Institute of TechnologyUnited States Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
Mukund RaghothamanRaghothaman, Mukund University of Southern California Artifact Evaluation Co-Chair in Organizing Committee for POPL 2022
Mukund RaghothamanRaghothaman, Mukund University of Southern CaliforniaUnited States Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Gautier RaimondiRaimondi, Gautier Inria Type-directed Program Transformation for Constant-Time Enforcement
Divya RameshRamesh, Divya University of Michigan Cod(e)ifying The Law
Aseem RastogiRastogi, Aseem Microsoft ResearchIndia Committee Member in Program Committee within the CPP-track
Stefan RatschanRatschan, Stefan The Czech Academy of Sciences Fast Three-Valued Abstract Bit-Vector Arithmetic
Shravan Ravi NarayanRavi Narayan, Shravan University of California at San DiegoUnited States Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Rodrigo RayaRaya, Rodrigo EPFLSwitzerland NP Satisfiability for Arrays as Powers
Kristian RealeReale, Kristian Department of Mathematics and Computer Science University of Calabria - DLVSystem S.r.l.Italy Smart Devices and Large Scale Reasoning via ASP: Tools and Applications
Sven ReimerReimer, Sven OneSpin Solutions, MunichGermany Making PROGRESS in Property Directed Reachability
Alex ReinkingReinking, Alex UC BerkeleyUnited States Artifact Evalation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Xinyue RenRen, Xinyue Nanjing UniversityChina Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata
Alex RendaRenda, Alex Massachusetts Institute of TechnologyUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Thomas RepsReps, Thomas University of Wisconsin--Madison Program Analysis via Graph Reachability: Past, Present, and Future [Part A]
Andrew ReynoldsReynolds, Andrew University of IowaUnited States Bit-Precise Reasoning via Int-Blasting Satisfiability and Synthesis Modulo Oracles
Tamara RezkRezk, Tamara Inria, France Committee Member in Steering Committee within the PriSC-track
Fracesco RiccaRicca, Fracesco University of CalabriaItaly Modelling the Outlier Detection Problem in QASP
Francesco RiccaRicca, Francesco University of Calabria, ItalyItaly Smart Devices and Large Scale Reasoning via ASP: Tools and Applications
Tania RichmondRichmond, Tania INRIA, Rennes, France then DGA - Maîtrise de l’Information Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
James RielyRiely, James DePaul UniversityUnited States Session Chair of Separation Logic (part of POPL ) The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Talia RingerRinger, Talia University of Illinois at Urbana-ChampaignUnited States You and Your Environment Invited Speaker in Invited speakers within the PLMW-track
Nick RiouxRioux, Nick University of Pennsylvania The Expression Problem and Theorem Proving (discussion)
Xavier RivalRival, Xavier INRIA/CNRS/ENS ParisFrance Lightweight Shape Analysis based on Physical Types PC Member in Program Committee within the VMCAI-track
Christine RizkallahRizkallah, Christine University of MelbourneAustralia Overcoming Restraint: Composing Verification of Foreign Functions with Cogent Committee Member in Organizing Committee within the PLMW-track Committee Member in Program Committee within the PriSC-track
Riley RobertsRoberts, Riley Utah State UniversityUnited States STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model Checking
Niall RocheRoche, Niall Mishcon de Reya,University College London,Accord Project Ergo - a programming language for Smart Legal Contracts
José Antonio Rodríguez-GarcíaRodríguez-García, José Antonio Universidad Rey Juan Carlos Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
Tiark RompfRompf, Tiark Purdue UniversityUnited States Partially Evaluating Symbolic Interpreters for All Committee Member in Program Committee within the PEPM-track
Andreas RossbergRossberg, Andreas Dfinity StiftungGermany Keynote 2: on WebAssembly
Carlos RozasRozas, Carlos Intel Corporation Towards Understanding Spectre-PHT in Memory-Safe Languages
Philipp RuemmerRuemmer, Philipp Uppsala UniversitySweden CertiStr: A Certified String Solver Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Committee Member in Program Committee within the POPL -track
Sukyoung RyuRyu, Sukyoung KAISTSouth Korea PLMW Panel (on Zoom)
Yann Régis-GianasRégis-Gianas, Yann Nomadic Labs ParisFrance Committee Member in Program Committee within the PEPM-track
S Fabrício S. ParanhosS. Paranhos, Fabrício Universidade Federal de Goiás Towards a Formalization of Nominal Sets in Coq
Feras SaadSaad, Feras Massachusetts Institute of TechnologyUnited States Scalable structure learning and inference for domain-specific probabilistic programs
Amr SabrySabry, Amr Indiana UniversityUnited States Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
Orkunt SabuncuSabuncu, Orkunt TED UniversityTurkey Multi-Agent Pick and Delivery with Capacities: Action Planning vs Path Finding
Mooly SagivSagiv, Mooly Tel Aviv UniversityIsrael Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Chiaki SakamaSakama, Chiaki Wakayama UniversityJapan Committee Member in Programme Committee within the PADL-track
Elmer SalazarSalazar, Elmer The University of Texas at DallasUnited States Modeling and Verification of Real-Time Systems with the Event Calculus and s(CASP) Graph-based Interpretation of Normal Logic Programs
Michael SammlerSammler, Michael MPI-SWSGermany VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
David SananSanan, David Nanyang Technological UniversitySingapore A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
Yuyang SangSang, Yuyang Yale University Session Chair of Tutorials 3 (part of POPL TutorialFest) Session Chair of Tutorials 4 (part of POPL TutorialFest)
Davide SangiorgiSangiorgi, Davide University of Bologna; InriaItaly From Enhanced Coinduction towards Enhanced Induction
Sriram SankaranarayananSankaranarayanan, Sriram University of Colorado, BoulderUnited States PC Member in Program Committee within the VMCAI-track
Mark SantolucitoSantolucito, Mark Barnard College, Columbia University, USAUnited States Artifact Evaluation Chair in Organizing Committee within the VMCAI-track
Giovanni SartorSartor, Giovanni University of BolognaItaly Stipula: a domain specific language for legal contracts Committee Member in Program Committee within the ProLaLa-track
Ken SatohSatoh, Ken National Institute of InformaticsJapan Introduction of PROLEG (PROlog-based LEGal reasoning support system) Committee Member in Program Committee within the ProLaLa-track
Kris SatyaSatya, Kris Georgia Institute of TechnologyUnited States Efficient Algorithms for Dynamic Bidirected Dyck-Reachability
Olivier Savary BélangerSavary Bélanger, Olivier Galois, Inc.United States Synthesizing Evidence of Emergent Computation
Philip SavilleSaville, Philip University of OxfordUnited Kingdom Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations
Konstantin SchekotihinSchekotihin, Konstantin Alpen-Adria Universit�t KlagenfurtAustria Decomposition-based job-shop scheduling with constrained clustering Committee Member in Programme Committee within the PADL-track
Philipp SchepperSchepper, Philipp CISPAGermany Subcubic Certificates for CFL Reachability
Sven ScheweSchewe, Sven University of LiverpoolUnited Kingdom EPMC Gets Knowledge in Multi-Agent Systems PC Member in Program Committee within the VMCAI-track
Tanja SchindlerSchindler, Tanja University of Freiburg Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Benedict SchlüterSchlüter, Benedict Ruhr University Bochum BPF and Spectre: Mitigating transient execution attacks
Georg Stefan SchmidSchmid, Georg Stefan EPFL, SwitzerlandSwitzerland Generalized Arrays for Stainless Frames
Alan SchmittSchmitt, Alan InriaFrance Certified Abstract Machines for Skeletal Semantics
Christoph SchollScholl, Christoph University of FreiburgGermany Making PROGRESS in Property Directed Reachability
Micha SchraderSchrader, Micha Technische Universität KaiserslauternGermany CertiStr: A Certified String Solver
Philipp SchröerSchröer, Philipp RWTH Aachen University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
William SchultzSchultz, William Northeastern University Formal Verification of a Distributed Dynamic Reconfiguration Protocol
Yoav SeginerSeginer, Yoav cdl-lang.org, Netherlands A verified algebraic representation of Cairo program execution
Martina SeidlSeidl, Martina Johannes Kepler University LinzAustria PC Member in Program Committee within the VMCAI-track
Dan SelmanSelman, Dan Docusign,Accord Project Ergo - a programming language for Smart Legal Contracts
Ilya SergeySergey, Ilya National University of SingaporeSingapore Workshops Co-Chair in Organizing Committee for POPL 2022 Automatically Synthesising Programs that We Can Trust Panel 2: the future of concurrency and parallelism Invited Speaker in Invited speakers within the PLMW-track Co-chair in Tutorial Evaluation Committee within the POPL TutorialFest-track
Sanjit SeshiaSeshia, Sanjit UC BerkeleyUnited States Satisfiability and Synthesis Modulo Oracles
Peter SestoftSestoft, Peter IT University of CopenhagenDenmark A partial history of partial evaluation
Tobias SeufertSeufert, Tobias University of FreiburgGermany Making PROGRESS in Property Directed Reachability
Peter SewellSewell, Peter University of CambridgeUnited Kingdom CN: A Refinement Type System for C VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
Chung-chieh ShanShan, Chung-chieh Indiana University, USA Committee Member in Steering Committee within the LAFI-track Committee Member in Program Committee within the POPL -track
Natarajan ShankarShankar, Natarajan SRI International, USA Session Chair of Satisfiability Modulo Theories (part of VMCAI)
Zhong ShaoShao, Zhong Yale UniversityUnited States Layered and Object-Based Game Semantics Verified Compilation of C Programs with a Nominal Memory Model Panel 1: proof assistants for PL and math Committee Member in Program Committee within the PriSC-track Committee Member in Steering Committee within the CPP-track
Qingkai ShiShi, Qingkai Ant GroupChina Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Sharon ShohamShoham, Sharon Tel Aviv UniversityIsrael Property-Directed Reachability as Abstract Interpretation in the Monotone Theory Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions
Filip SieczkowskiSieczkowski, Filip University of WrocławPoland Committee Member in Program Committee within the POPL -track
Mihaela SighireanuSighireanu, Mihaela IRIF, Université Paris Diderot, FranceFrance PC Member in Program Committee within the VMCAI-track
Giovanni SilenoSileno, Giovanni University of Amsterdam DPCL: a Language Template for Normative Specifications
Alexandra SilvaSilva, Alexandra Cornell UniversityUnited States Finding a research topic (or being found by a research topic?) Coalgebra for the working programming languages researcher Invited Speaker in Invited speakers within the PLMW-track
Jerome SimeonSimeon, Jerome ClauseUnited States Ergo - a programming language for Smart Legal Contracts
Gagandeep SinghSingh, Gagandeep University of Illinois at Urbana-Champaign; VMwareUnited States Session Chair of Program Analysis (part of POPL ) Formal Methods and Deep Learning [Part B] A Dual Number Abstraction for Static Analysis of Clarke Jacobians PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations PC Member in Program Committee within the VMCAI-track
Jeffrey Mark SiskindSiskind, Jeffrey Mark Elmore Family School of Electrical and Computer Engineering, Purdue UniversityUnited States Committee Member in Steering Committee within the LAFI-track
KC SivaramakrishnanSivaramakrishnan, KC IIT MadrasIndia Committee Member in Program Committee within the PEPM-track
Cyril SixSix, Cyril Kalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG Formally Verified Superblock Scheduling
Armando Solar-LezamaSolar-Lezama, Armando Massachusetts Institute of Technology Session Chair of Dynamic Analysis (part of POPL ) Session Chair of Reasoning about Probabilistic Programs and Algorithms (part of POPL ) Better Learning through Programming Languages
Tran Cao SonSon, Tran Cao New Mexico State University Committee Member in Programme Committee within the PADL-track
Yahui SongSong, Yahui National University of SingaporeSingapore Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tyler SorensenSorensen, Tyler University of California at Santa Cruz Committee Member in Selection Committee within the POPL Student Research Competition-track
Matthieu SozeauSozeau, Matthieu InriaFrance Session with the Coq Development Team The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoq
Sarah SpallSpall, Sarah Indiana University Forward build systems, formally
Jip SpelSpel, Jip RWTH Aachen UniversityGermany Gradient-Descent for Randomized Controllers under Partial Observability
Simon SpiesSpies, Simon MPI-SWSGermany Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Nick SpinaleSpinale, Nick Arm Research The Supervisionary proof-checking kernel, or: a work-in-progress toward proof-generating code
Bas SpittersSpitters, Bas Aarhus UniversityDenmark A Verified Pipeline from a Specification Language to Optimized, Safe Rust Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the CPP-track
Jiri SrbaSrba, Jiri Aalborg UniversityDenmark Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking
Kathrin StarkStark, Kathrin Princeton University, USAUnited States Committee Member in Program Committee within the CPP-track
Philipp StassenStassen, Philipp Aarhus University mitten: A Flexible Multimodal Proof Assistant
Sam StatonStaton, Sam University of Oxford Abstract types in probabilistic programming Committee Member in Program Committee within the POPL -track
Deian StefanStefan, Deian University of California at San DiegoUnited States Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI Committee Member in Steering Committee within the PriSC-track
Leo StefanescoStefanesco, Leo IRIF, University Paris Diderot & CNRSFrance Layered and Object-Based Game Semantics
Jonathan SterlingSterling, Jonathan Aarhus UniversityDenmark Make Three To Throw Away: Frontiers in Homotopical Proof Assistants A Cost-Aware Logical Framework
Martin StreckerStrecker, Martin Singapore Management University Overview of the CCLAW L4 project
Pierre-Yves StrubStrub, Pierre-Yves Ecole PolytechniqueFrance A Drag-and-Drop Proof Tactic
Aaron StumpStump, Aaron The University of Iowa, USAUnited States Committee Member in Program Committee within the WITS-track
Kohei SuenagaSuenaga, Kohei Graduate School of Informatics, Kyoto UniversityJapan Committee Member in Program Committee within the POPL -track
Jun SunSun, Jun Singapore Management UniversitySingapore A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
Meng SunSun, Meng Peking UniversityChina EPMC Gets Knowledge in Multi-Agent Systems
Julian SutherlandSutherland, Julian Imperial College London TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
David SwaseySwasey, David BedRock Systems A Case for Lightweight Interfaces in Coq
Hira Taqdees SyedaSyeda, Hira Taqdees Amazon Web ServicesGermany Committee Member in Program Committee within the CPP-track
Don SymeSyme, Don MicrosoftUnited Kingdom Industry keynote -- What does a toolchain for legislation eventually become?
Dmitrij SzamozvancevSzamozvancev, Dmitrij University of CambridgeUnited Kingdom Formal Metatheory of Second-Order Abstract Syntax
César SánchezSánchez, César IMDEA Software InstituteSpain PC Member in Program Committee within the VMCAI-track
T Quang-Trung TaTa, Quang-Trung National University of Singapore Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Nicolas TabareauTabareau, Nicolas Inria Gradualizing the Calculus of Inductive Constructions
Nicolas TabareauTabareau, Nicolas InriaFrance Observational Equality: Now for Good Panel 1: proof assistants for PL and math
Nima TajelipirbazariTajelipirbazari, Nima TED UniversityTurkey Multi-Agent Pick and Delivery with Capacities: Action Planning vs Path Finding
Bryan TanTan, Bryan University of California at Santa BarbaraUnited States SolType: Refinement Types for Arithmetic Overflow in Solidity
Shangyin TanTan, Shangyin Purdue UniversityUnited States Partially Evaluating Symbolic Interpreters for All
Val TannenTannen, Val University of Pennsylvania, USA Tealeaves: Categorical structures for syntax
Éric TanterTanter, Éric University of Chile Gradualizing the Calculus of Inductive Constructions Committee Member in Program Committee within the PriSC-track
Paul TarauTarau, Paul University of North TexasUnited States Committee Member in Programme Committee within the PADL-track
Fabio TardivoTardivo, Fabio New Mexico State UniversityUnited States Parallel Declarative Solutions of Sequencing Problems using Multi-valued Decision Diagrams and GPUs
Serdar TasiranTasiran, Serdar Amazon, n.n. PC Member in Program Committee within the VMCAI-track
Joseph TassarottiTassarotti, Joseph Boston CollegeUnited States Verifying Concurrent, Crash-Safe Systems with Perennial A Separation Logic for Negative Dependence Committee Member in Program Committee within the LAFI-track Invited Speaker in Invited speaker within the CoqPL-track Committee Member in Program Committee within the CPP-track
Enrico TassiTassi, Enrico INRIAFrance Committee Member in Program Committee within the CoqPL-track
Christine TassonTasson, Christine Sorbonne Université — LIP6France Session Chair of Contributed talks (part of LAFI) Session Chair of Keynote (part of LAFI) Committee Member in Organizing Committee within the LAFI-track
Carlo TaticchiTaticchi, Carlo University of PerugiaItaly Timed Concurrent Language for Argumentation: an Interleaving Approach
Zachary TatlockTatlock, Zachary University of WashingtonUnited States Relational E-matching
Zenna TavaresTavares, Zenna Massachusetts Institute of Technology Committee Member in Program Committee within the LAFI-track
Landon TaylorTaylor, Landon Utah State UniversityUnited States Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms
Tachio TerauchiTerauchi, Tachio Waseda UniversityJapan Committee Member in Program Committee within the POPL -track
Aalok ThakkarThakkar, Aalok University of PennsylvaniaUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Aditya V. ThakurThakur, Aditya V. University of California at DavisUnited States Committee Member in Program Committee within the POPL -track
Jérémy ThibaultThibault, Jérémy MPI-SP SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation
Ramanathan S. ThinniyamThinniyam, Ramanathan S. MPI-SWSGermany Context-Bounded Verification of Thread Pools
Amin TimanyTimany, Amin Aarhus UniversityDenmark Web Co-Chair in Organizing Committee for POPL 2022 Session Chair of Session with the Coq Development Team (part of CoqPL) Session Chair of Invited Talk II (part of CoqPL) Session Chair of Contributed Talk (Afternoon) (part of CoqPL) Co-chair in Organizing Committee within the CoqPL-track
Cesare TinelliTinelli, Cesare University of IowaUnited States Bit-Precise Reasoning via Int-Blasting PC Member in Program Committee within the VMCAI-track
Alon TitelmanTitelman, Alon Starkware Industries Ltd. A verified algebraic representation of Cairo program execution
Laura TitoloTitolo, Laura NIA/NASA LaRCUnited States Session Chair of Invited Talk (part of CPP) A Compositional Proof Framework for FRETish Requirements PC Member in Program Committee within the VMCAI-track Committee Member in Program Committee within the CPP-track
Sam Tobin-HochstadtTobin-Hochstadt, Sam Indiana University Forward build systems, formally
Emina TorlakTorlak, Emina University of WashingtonUnited States A Formal Foundation for Symbolic Evaluation with Merging
Paolo TorriniTorrini, Paolo INRIA A CompCert backend with symbolic encryption
Sophie TourretTourret, Sophie Max Planck Institute for Informatics Committee Member in Program Committee within the CPP-track
Dmitriy TraytelTraytel, Dmitriy University of CopenhagenDenmark Committee Member in Program Committee within the CPP-track
Richard TreflerTrefler, Richard University of Waterloo, CanadaCanada Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
Adrian Trejo NuñezTrejo Nuñez, Adrian University of Texas at AustinUnited States Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Rahmadi TrimanandaTrimananda, Rahmadi University of California at Irvine, USAUnited States Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not Terminate
Stavros TripakisTripakis, Stavros Northeastern University Formal Verification of a Distributed Dynamic Reconfiguration Protocol
Jean-Baptiste TristanTristan, Jean-Baptiste Boston CollegeUnited States Committee Member in Organizing Committee within the LAFI-track
Stelios TsampasTsampas, Stelios FAU Erlangen-Nuremberg, INF 8 The Fox and the Hound (Episode 2): Fully Abstract, Robust Compilation and How to Reconcile the Two, Abstractly
Takeshi TsukadaTsukada, Takeshi Chiba UniversityJapan Software Model-Checking as Cyclic-Proof Search
Kanae TsushimaTsushima, Kanae National Institute of Informatics, JapanJapan Introduction of PROLEG (PROlog-based LEGal reasoning support system) Committee Member in Program Committee within the ProLaLa-track
Syouki TsuyamaTsuyama, Syouki Tokyo Institute of Technology Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)
Andrea TurriniTurrini, Andrea State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of SciencesChina EPMC Gets Knowledge in Multi-Agent Systems
U Sebastian UllrichUllrich, Sebastian Karlsruhe Institute of TechnologyGermany Gotta prove fast: building an ecosystem for effortless native compilation of tactics
Çağrı Uluç YıldırımoğluUluç Yıldırımoğlu, Çağrı Sabanci UniversityTurkey Multi-Agent Pick and Delivery with Capacities: Action Planning vs Path Finding
Hiroshi UnnoUnno, Hiroshi University of Tsukuba; RIKEN AIPJapan Software Model-Checking as Cyclic-Proof Search
Dominique UnruhUnruh, Dominique University of Tartu Reflection, Rewinding, and Coin-Toss in EasyCrypt
Caterina UrbanUrban, Caterina Inria & École Normale Supérieure \| Université PSLFrance Committee Member in Program Committee within the POPL -track
V Viktor VafeiadisVafeiadis, Viktor MPI-SWSGermany Truly Stateless, Optimal Dynamic Partial Order Reduction Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores
L. Thomas van Binsbergenvan Binsbergen, L. Thomas CWINetherlands Reflections on the design and application of eFLINT
Thomas van Binsbergenvan Binsbergen, Thomas University of Amsterdam DPCL: a Language Template for Normative Specifications
Floris van Doornvan Doorn, Floris University of PittsburghUnited States Committee Member in Program Committee within the CPP-track
Tom van Engersvan Engers, Tom Leibniz Institute / University of Amsterdam / TNO DPCL: a Language Template for Normative Specifications
Sarat Chandra VaranasiVaranasi, Sarat Chandra The University of Texas at DallasUnited States Modeling and Verification of Real-Time Systems with the Event Calculus and s(CASP)
Anton VaronkaVaronka, Anton MPI-SWSGermany What’s Decidable about Linear Loops?
Vasco T. VasconcelosVasconcelos, Vasco T. LASIGE, Faculty of Sciences, University of LisbonPortugal Deciding type equivalence with simple grammars
Niki VazouVazou, Niki IMDEA Software Institute Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the WITS-track
Martin VechevVechev, Martin ETH ZurichSwitzerland PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
Daniel VenturaVentura, Daniel Universidade Federal de Goiás Towards a Formalization of Nominal Sets in Coq
Freek VerbeekVerbeek, Freek Open University of the Netherlands, The Netherlands Committee Member in Program Committee within the CPP-track
Simon Friis VindumVindum, Simon Friis Aarhus UniversityDenmark Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
Dimitrios VytiniotisVytiniotis, Dimitrios DeepMindUnited Kingdom Committee Member in Program Committee within the PEPM-track Committee Member in Program Committee within the POPL -track
Matthijs VákárVákár, Matthijs University of Oxford Committee Member in Program Committee within the LAFI-track
W Dominik WagnerWagner, Dominik University of Oxford A Language and Smoothed Semantics for Convergent Stochastic Gradient Descent
David WalkerWalker, David Princeton UniversityUnited States Safe, Modular Packet Pipeline Programming
Bow-Yaw WangWang, Bow-Yaw Academia SinicaTaiwan Verifying Pufferfish Privacy in Hidden Markov Models
Jiawan WangWang, Jiawan Nanjing UniversityChina Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata
Lei WangWang, Lei FacebookUnited States Profile Inference Revisited
Meng WangWang, Meng University of BristolUnited Kingdom CircuitFlow: : A Domain Specific Language for Dataflow Programming Staging with Class: A Specification for Typed Template Haskell Linked Visualisations via Galois Dependencies
Xi WangWang, Xi University of WashingtonUnited States A Formal Foundation for Symbolic Evaluation with Merging
Yisu Remy WangWang, Yisu Remy University of WashingtonUnited States Relational E-matching
Yuepeng WangWang, Yuepeng Simon Fraser University Web Co-Chair in Organizing Committee for POPL 2022
Yuting WangWang, Yuting Shanghai Jiao Tong UniversityChina Verified Compilation of C Programs with a Nominal Memory Model
Zhuyang WangWang, Zhuyang University of MinnesotaUnited States Logarithm and Program Testing
Zi WangWang, Zi University of Wisconsin-MadisonUnited States Interval Universal Approximation for Neural Networks
Conrad WattWatt, Conrad University of CambridgeUnited Kingdom Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Guannan WeiWei, Guannan Purdue UniversityUnited States Partially Evaluating Symbolic Interpreters for All
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States Session Chair of Types (part of POPL ) Session Chair of SIGPLAN CARES (part of POPL ) Session Chair of Metaprogramming (part of POPL ) Session Chair of SIGPLAN CARES (part of POPL ) Session Chair of SIGPLAN CARES (part of POPL Diversity, Equity and Inclusion) Session Chair of SIGPLAN CARES (part of POPL Diversity, Equity and Inclusion) Panel (live only, no recording) Effect-Oblivious Equivalence Benchmarking Binding (discussion) The Expression Problem and Theorem Proving (discussion) Panelist in Panelists within the PLMW-track
Aaron WeissWeiss, Aaron Northeastern UniversityUnited States Student Volunteer Co-Chair in Organizing Committee for POPL 2022
Tobias WelpWelp, Tobias OneSpin Solutions, MunichGermany Making PROGRESS in Property Directed Reachability
Benjamin WernerWerner, Benjamin Ecole polytechniqueFrance A Drag-and-Drop Proof Tactic
Scott WesleyWesley, Scott University of Waterloo, CanadaCanada Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
Markus A. WhitelandWhiteland, Markus A. MPI-SWSGermany What’s Decidable about Linear Loops?
John WickersonWickerson, John Imperial College LondonUnited Kingdom Committee Member in Program Committee within the POPL -track
Freek WiedijkWiedijk, Freek Radboud University NijmegenNetherlands Committee Member in Program Committee within the CPP-track
Thomas WiesWies, Thomas New York UniversityUnited States Session Chair of Static Analysis and Abstract Interpretation (part of VMCAI) Session Chair of Invited Talk (part of VMCAI) Program Co-Chair in Organizing Committee within the VMCAI-track
James R. WilcoxWilcox, James R. CertoraUnited States Property-Directed Reachability as Abstract Interpretation in the Monotone Theory Induction Duality: Primal-Dual Search for Invariants Committee Member in Program Committee within the POPL -track
Max WillseyWillsey, Max University of WashingtonUnited States Relational E-matching
Tobias WinklerWinkler, Tobias RWTH Aachen UniversityGermany Out of Control: Reducing Probabilistic Models by Control-State Elimination
Dominik WintererWinterer, Dominik ETH ZurichSwitzerland Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Sebastian WolffWolff, Sebastian New York UniversityUnited States Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Meng Weng WongWong, Meng Weng Singapore Management UniversitySingapore Overview of the CCLAW L4 project Committee Member in Program Committee within the ProLaLa-track
James WorrellWorrell, James University of OxfordUnited Kingdom What’s Decidable about Linear Loops?
Nicolas WuWu, Nicolas Imperial College LondonUnited Kingdom Staging with Class: A Specification for Typed Template Haskell Committee Member in Program Committee within the POPL -track
Yuming WuWu, Yuming Nanjing UniversityChina Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata
Zhilin WuWu, Zhilin Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of SciencesChina Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Valentin WüstholzWüstholz, Valentin ConsenSysGermany Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
X Ningning XieXie, Ningning University of TorontoCanada Parallel Algebraic Effect Handlers Staging with Class: A Specification for Typed Template Haskell
Wen XiongXiong, Wen Nanjing UniversityChina Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata
Harry XuXu, Harry University of California, Los Angeles (UCLA)United States Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not Terminate
Anton XueXue, Anton University of Pennsylvania Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Y Jeremy YallopYallop, Jeremy University of CambridgeUnited Kingdom let (rec) insertion without Effects, Lights or Magic Staging with Class: A Specification for Typed Template Haskell
Hongseok YangYang, Hongseok KAISTSouth Korea PC Chair in Organizing Committee for POPL 2022 Session Chair of Welcome (part of POPL ) Welcome by POPL 2022 Program Chair POPL'22 Distinguished Papers Program Chair Report Program Chair in Program Committee within the POPL -track Committee Member in Selection Committee within the POPL Virtual Workshop-track
Rem YangYang, Rem University of Illinois at Urbana-ChampaignUnited States A Dual Number Abstraction for Static Analysis of Clarke Jacobians
Qianchuan YeYe, Qianchuan Purdue UniversityUnited States Scrap your boilerplate definitions in 10 lines of Ltac! Oblivious Algebraic Data Types
Neringa YoungYoung, Neringa Lithuania Committee Member in Selection Committee within the POPL Virtual Workshop-track
Hongtao YuYu, Hongtao FacebookUnited States Profile Inference Revisited
Charles YuanYuan, Charles Massachusetts Institute of TechnologyUnited States Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
Z Fabian ZaiserZaiser, Fabian University of Oxford Rigorous Approximation of Posterior Inference for Probabilistic Programs Nonparametric Involutive Markov Chain Monte Carlo
Vladimir ZamdzhievZamdzhiev, Vladimir InriaFrance Semantics for Variational Quantum Programming
Francesco Zappa NardelliZappa Nardelli, Francesco MetaFrance Applying Formal Verification to Microkernel IPC at Meta
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Session Chair of Chairs' Report and Business Meeting (part of CPP) Session Chair of Proof Infrastructure, Rewriting and Automated Reasoning (part of CPP) Session Chair of Invited Talk (part of CPP) Session Chair of Welcome from the chairs (part of CPP) Tealeaves: Categorical structures for syntax PC Chair in Program Committee within the CPP-track PC Chair in Organization Committee within the CPP-track
Olivier ZendraZendra, Olivier INRIA, Rennes, France Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Georg ZetzscheZetzsche, Georg MPI-SWSGermany Context-Bounded Verification of Thread Pools
Cheng ZhangZhang, Cheng Boston UniversityUnited States On Incorrectness Logic and Kleene Algebra with Top and Tests
Danfeng ZhangZhang, Danfeng Pennsylvania State UniversityUnited States Committee Member in Program Committee within the PriSC-track
Jialu ZhangZhang, Jialu Artifact Evaluation Committee Member in Artifact Evaluation Committee within the VMCAI-track
Lijun ZhangZhang, Lijun Institute of Software, Chinese Academy of SciencesChina Verifying Pufferfish Privacy in Hidden Markov Models EPMC Gets Knowledge in Multi-Agent Systems
Ling ZhangZhang, Ling Shanghai Jiao Tong UniversityChina Verified Compilation of C Programs with a Nominal Memory Model
Qirun ZhangZhang, Qirun Georgia Institute of TechnologyUnited States Session Chair of Algorithmic Verification 1 (part of POPL ) Session Chair of Algorithmic Verification 2 (part of POPL ) Program Analysis via Graph Reachability: Past, Present, and Future [Part B] Efficient Algorithms for Dynamic Bidirected Dyck-Reachability Committee Member in Program Committee within the POPL -track
Tesla ZhangZhang, Tesla The Pennsylvania State University Multi case trees: confluence and coverage (discussion) First-class pattern synonyms
Yihong ZhangZhang, Yihong University of WashingtonUnited States Relational E-matching
Yizhou ZhangZhang, Yizhou University of WaterlooCanada Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion
Zhen ZhangZhang, Zhen Utah State UniversityUnited States Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model Checking
Zirui Neil ZhaoZhao, Zirui Neil University of Illinois at Urbana-ChampaignUnited States Towards Understanding Spectre-PHT in Memory-Safe Languages
Tan Zhi-XuanZhi-Xuan, Tan Massachusetts Institute of Technology Committee Member in Program Committee within the LAFI-track
Yaoda ZhouZhou, Yaoda University of Hong Kong Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yuan ZhouZhou, Yuan University of OxfordUnited Kingdom Committee Member in Program Committee within the LAFI-track
Amy ZhuZhu, Amy University of WashingtonUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Lukasz ZiarekZiarek, Lukasz University at BuffaloUnited States Committee Member in Programme Committee within the PADL-track
Noam ZilbersteinZilberstein, Noam Cornell UniversityUnited States Applying Formal Verification to Microkernel IPC at Meta
Beta ZilianiZiliani, Beta FAMAF, UNC and CONICETArgentina Committee Member in Program Committee within the PEPM-track
Yoni ZoharZohar, Yoni Bar Ilan UniversityUnited States Session Chair of Static Analysis and Hybrid Systems (part of VMCAI) Bit-Precise Reasoning via Int-Blasting
Daming ZouZou, Daming ETH ZurichSwitzerland Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Lenore ZuckZuck, Lenore UICUnited States PC Member in Program Committee within the VMCAI-track PC Member in Program Committee within the VMCAI-track
Ö Joakim ÖhmanÖhman, Joakim IMDEA Software Institute; Universidad Politécnica de MadridSpain Visibility Reasoning for Concurrent Snapshot Algorithms

POPL 2022 Contributors

Results (848)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia