POPL 2025 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (1097)

A Parosh Aziz AbdullaAbdulla, Parosh Aziz Uppsala University, Sweden An Automata-based Framework for Quantum Circuit Verification Verifying Quantum Circuits with Level-Synchronized Tree Automata PC Member in Program Committee within the VMCAI-track
Muhammad AbdullahAbdullah, Muhammad MIT Collapsing Towers for Side-Channel Security (Short Paper)
Umut A. AcarAcar, Umut A. Carnegie Mellon UniversityUnited States Invited Talk: Bridging Safety and Performance
Beniamino AccattoliAccattoli, Beniamino Inria & Ecole PolytechniqueFrance Interaction Equivalence
Michael D. AdamsAdams, Michael D. National University of SingaporeUnited States Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
Alejandro AguirreAguirre, Alejandro Aarhus UniversityDenmark Modelling Recursion and Probabilistic Choice in Guarded Type Theory Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Amal AhmedAhmed, Amal Northeastern University, USAUnited States Committee Member in Program Committee within the WAW-track Author in Steering Committee within the PriSC-track
Seth AhrenbachAhrenbach, Seth Beneficial AI FoundationUnited States DafnyBench: A Benchmark for Formal Software Verification PC Member in Program Committee within the Dafny-track
Ozgur AkgunAkgun, Ozgur University of St Andrews, St Andrews, UKUnited Kingdom Committee Member in Program Committee within the PADL-track
Nikhil AkitiAkiti, Nikhil UCSD Generic Refinement Types
Hinano AkiyamaAkiyama, Hinano Ochanomizu University Algebraic Stepper for Simple Modules
Ryan AlameddineAlameddine, Ryan University of California, Berkeley Optimizing Asynchronous Rust with Hydroflow Optimizing Asynchronous Rust with Hydroflow
Jonathan AldrichAldrich, Jonathan Carnegie Mellon UniversityUnited States Gradual C0: Symbolic Execution for Gradual Verification
Cass AlexandruAlexandru, Cass RPTU Kaiserslautern-LandauGermany Intrinsically Correct Sorting in Cubical Agda
Damir AlfiatonovAlfiatonov, Damir Innopolis University Towards Generic Higher-Order Unification Implementations in Haskell
Clément AllainAllain, Clément INRIAFrance Tail Modulo Cons, OCaml, and Relational Separation Logic
Guillaume AllaisAllais, Guillaume University of StrathclydeUnited Kingdom Co-chair in Chairs within the PEPM-track
Ricardo AlmeidaAlmeida, Ricardo University of Edinburgh A CHERI C Memory Model for Verified Temporal Safety
José Bacelar AlmeiraAlmeira, José Bacelar University of Minho & INESC TEC Leakage-Free Probabilistic Jasmin Programs
Carmen AlmudéverAlmudéver, Carmen Universitat Politècnica de València Committee Member in Program Committee within the PLanQC-track
Nada AminAmin, Nada Harvard UniversityUnited States Collapsing Towers for Side-Channel Security (Short Paper) Semantics of the memo Probabilistic Programming Language DafnyBench: A Benchmark for Formal Software Verification dafny-annotator: AI-Assisted Verification of Dafny Programs VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search Committee Member in Program Committee within the PADL-track Committee Member in Program Committee Members within the PEPM-track
Matthew AmyAmy, Matthew Simon Fraser UniversityCanada Lightweight functional verification of quantum programs Linear and non-linear relational analyses for Quantum Program Optimization Organizing Committee in Organizing Committee within the PLanQC-track
Elli AnastasiadiAnastasiadi, Elli Uppsala UniversitySweden Committee Member in Program Committee within the VMCAI-track
Emmanuel Anaya GonzalezAnaya Gonzalez, Emmanuel UCSD Laurel: Unblocking Automated Verification with Large Language Models
Bruno AndreottiAndreotti, Bruno Universidade Federal de Minas Gerais Committee Member in Artifact Evaluation Committee within the VMCAI-track
Andrew W. AppelAppel, Andrew W. Princeton University A Verified Foreign Function Interface Between Coq and C
Vincenzo ArceriArceri, Vincenzo University of Parma, ItalyItaly Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Miguel AreiasAreias, Miguel University of Porto, Portugal On Bridging Prolog and Python to Enhance an Inductive Logic Programming System
Jaime AriasArias, Jaime CNRS; LIPN; Université Sorbonne Paris NordFrance Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Joaquín AriasArias, Joaquín Universidad Rey Juan CarlosSpain C3G: Causally Constrained Counterfactual Generation
Zena M. AriolaAriola, Zena M. University of OregonUnited States Committee Member in Program Committee Members within the PEPM-track
Michael ArntzeniusArntzenius, Michael None Finite-Choice Logic Programming
Jai AroraArora, Jai University of Illinois at Urbana-ChampaignUnited States TensorRight: Automated Verification of Tensor Graph Rewrites
Kazuyuki AsadaAsada, Kazuyuki Tohoku University Characterizations of Partial Well-Behaved Lenses
Kenichi AsaiAsai, Kenichi Ochanomizu UniversityJapan Session Chair of Types and meta theory (part of PEPM) Algebraic Stepper for Simple Modules
Flavio AscariAscari, Flavio University of Pisa U-turn: Forward-driven backward analysis for incorrectness
Nicola AssoliniAssolini, Nicola University of VeronaItaly Committee Member in AV Committee for POPL 2025 A Static Analysis of Entanglement
Mohamed Faouzi AtigAtig, Mohamed Faouzi Uppsala University, SwedenSweden Committee Member in Program Committee within the POPL -track
Robert AtkeyAtkey, Robert University of Strathclyde Type-Sensitive Algebraic Macros (Short Paper) Committee Member in Program Committee within the POPL -track Author in Selection Committee within the POPL Student Research Competition-track
Eric AtkinsonAtkinson, Eric Inference Plans for Hybrid Particle Filtering
Eric AtkinsonAtkinson, Eric Binghamton University Committee Member in Program Committee within the LAFI-track
Martin AvanziniAvanzini, Martin Inria A quantitative probabilistic relational Hoare logic
Sacha-Élie AyounAyoun, Sacha-Élie Imperial College LondonUnited Kingdom Student Volunteer Co-Chair in Organizing Committee for POPL 2025 Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation Committee Member in Program Committee within the TPSA-track
Jon AytacAytac, Jon Sandia National Laboratories Reasoning About Sampling Without Sampling: Atomic Machines for Contextual Equivalence in Probabilistic Programs
Muqsit AzeemAzeem, Muqsit Technical University of MunichGermany Committee Member in Student Volunteers for POPL 2025 1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Rochester Institute of Technology, USAUnited States Domain Reasoning In TopKAT: Reduction and Completeness Committee Member in Program Committee within the POPL -track
B Anne BaanenBaanen, Anne Vrije Universiteit Amsterdam Certifying rings of integers in number fields
Michael BackesBackes, Michael Cispa Helmholtz Center for Information Security Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
Alexander BaiBai, Alexander MPI-SWSUnited States A Big-Step Compositional Continuation-Passing Semantics for WebAssembly
Marcello BalducciniBalduccini, Marcello Saint Joseph's University, USA Committee Member in Program Committee within the PADL-track
Thomas BallBall, Thomas Microsoft ResearchUnited States Session Chair of Automata and Temporal Properties (part of POPL ) Symbolic Automata: omega-Regularity Modulo Theories
Ignacio BallesterosBallesteros, Ignacio IMDEA Software Institute and Universidad Politécnica de MadridSpain Haskell Based Spreadsheets
Stephanie BalzerBalzer, Stephanie Carnegie Mellon UniversityUnited States A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types Semantic Logical Relations for Timed Message-Passing Protocols
Mutsunori BanbaraBanbara, Mutsunori Nagoya UniversityJapan Committee Member in Program Committee within the PADL-track
Rini BanerjeeBanerjee, Rini University of CambridgeUnited Kingdom Fulminate: Testing CN Separation-Logic Specifications in C
Sorav BansalBansal, Sorav IIT Delhi and CompilerAI LabsIndia Committee Member in Program Committee within the POPL -track
Jialu BaoBao, Jialu Cornell University Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
Yuyan BaoBao, Yuyan Augusta UniversityUnited States Author in Selection Committee within the POPL Student Research Competition-track
Anita BaralBaral, Anita Miami University ASP for Language Documentation and Reclamation: A Derivational Stemming Tool for Myaamia
Haniel BarbosaBarbosa, Haniel Universidade Federal de Minas Gerais, BrazilBrazil PC Member in Program Committee within the VMCAI-track
Aurèle BarrièreBarrière, Aurèle EPFLSwitzerland Committee Member in Program Committee within the PriSC-track
Gilles BartheBarthe, Gilles MPI-SP; IMDEA Software InstituteGermany Preservation of Speculative Constant-time by Compilation Preservation of speculative constant-time by compilation Automating equational proofs in Dirac notation A quantitative probabilistic relational Hoare logic
Ezio BartocciBartocci, Ezio TU WienAustria Exact Inference for Nested Discrete Probabilistic Programs (Remote)
David BasinBasin, David ETH ZurichSwitzerland Reachability Analysis of the Domain Name System
Guillaume BaudartBaudart, Guillaume InriaFrance Inference Plans for Hybrid Particle Filtering
Andrej BauerBauer, Andrej University of LjubljanaSlovenia Committee Member in Program Committee within the WITS-track
Atılım Güneş BaydinBaydin, Atılım Güneş University of Oxford Session Chair of Fourth session (part of LAFI) Session Chair of Second session (part of LAFI) Welcome Closing remarks Co-chair in Program Committee within the LAFI-track
Olga BecciBecci, Olga University of Bologna Size Analysis of Imperative Quantum Circuit Building Programs Through Floyd-Hoare Logics
Calvin BeckBeck, Calvin University of Pennsylvania, USACanada Vellvm: Formalizing the Informal
Ryan BeckettBeckett, Ryan Microsoft Research, USA Committee Member in Program Committee within the POPL -track
Julia BelyakovaBelyakova, Julia Purdue UniversityUnited States Session Chair of Verification 1 (part of POPL ) From Traces to Program Incorrectness: A Type-Theoretic Approach Derivative-Guided Symbolic Execution
Clara Benac EarleBenac Earle, Clara Universidad Politécnica de MadridSpain Committee Member in Program Committee within the PADL-track
Benjamin BennetzenBennetzen, Benjamin Department of Computer Science, Aalborg University A Type Safe Calculus for Generating Syntax-Directed Editors
Manuel BenteleBentele, Manuel University of FreiburgGermany Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
Aaron BerdyBerdy, Aaron AWS Quantum Technologies AutoQASM: Imperative quantum programming in Python
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States PC Member in Program Committee within the CPP-track
Yves BertotBertot, Yves INRIAFrance Session with the Coq Development Team
Frédéric BessonBesson, Frédéric Inria, Rennes BeePL: Correct-by-compilation kernel extensions
Siddharth BhatBhat, Siddharth University of Cambridge Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Malgorzata BiernackaBiernacka, Malgorzata University of Wrocław Committee Member in Program Committee within the PADL-track
Lars BirkedalBirkedal, Lars Aarhus UniversityDenmark Session Chair of Session 8 (part of CPP) The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic Modelling Recursion and Probabilistic Choice in Guarded Type Theory Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Henry BlanchetteBlanchette, Henry Pantograph: A Fluid and Typed Structure Editor
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands PC Member in Program Committee within the CPP-track
Lionel BlatterBlatter, Lionel Max Planck Institute for Security and Privacy Preservation of Speculative Constant-time by Compilation Preservation of speculative constant-time by compilation
Clément BlaudeauBlaudeau, Clément InriaFrance Avoiding signature avoidance in ML modules with zippers
Sandrine BlazyBlazy, Sandrine University of RennesFrance Session Chair of Session 5 (part of CPP) From operational semantics to verified compilation (and more) Business Meeting PC Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track PC Chair in Program Committee within the CPP-track Committee Member in Program Committee within the PriSC-track
Roderick BloemBloem, Roderick Institute of Software Technology, Graz University of Technology Austria Synthesis of Controllers for Continuous Blackbox Systems
Rastislav BodíkBodík, Rastislav Google Research, Brain TeamUnited States TensorRight: Automated Verification of Tensor Graph Rewrites
Sylvie BoldoBoldo, Sylvie Inria and Université Paris-SaclayFrance PC Member in Program Committee within the CPP-track
Filippo BonchiBonchi, Filippo University of PisaItaly Committee Member in Program Committee within the POPL -track
Karnbongkot BoonriongBoonriong, Karnbongkot Imperial College LondonUnited States Randomised Testing of the Dafny Compiler: Into the CI
Utpal BoraBora, Utpal University of CambridgeUnited Kingdom LLOR: Automated Repair of OpenMP Programs
Agustin BorgnaBorgna, Agustin Quantinuum HUGR: A Quantum-Classical Intermediate Representation Imperative Quantum Programming with Ownership and Borrowing in Guppy
Ahmed BouajjaniBouajjani, Ahmed IRIF, Université Paris DiderotFrance PC Member in Program Committee within the VMCAI-track
Olivier BouissouBouissou, Olivier Amazon Helping users to reduce Brittleness in their Dafny programs - a success story
Sylvain BoulméBoulmé, Sylvain Université Grenoble Alpes - CNRS - Grenoble INP - VerimagFrance Formally verified hardening of C programs against hardware fault injection
Frédéric BourBour, Frédéric TaridesFrance Tail Modulo Cons, OCaml, and Relational Separation Logic
Maddy BowersBowers, Maddy Massachusetts Institute of TechnologyUnited States Lazy Knowledge Compilation for Discrete PPLs
William J. BowmanBowman, William J. University of British ColumbiaCanada The Ethical Compiler: Addressing the Is-Ought Gap in Compilation (Invited Talk) Semantics-based program manipulation in the age of LLMs
David BrandfonbrenerBrandfonbrener, David Harvard VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Oliver BračevacBračevac, Oliver EPFL, LAMPSwitzerland Committee Member in Program Committee within the POPL -track
Andrew BrownBrown, Andrew Portland State University Meta-tracing Interpreters in WebAssembly
Greg BrownBrown, Greg University of Edinburgh A Fuelled Self-Reducer for System T (Short Paper)
Roberto BruniBruni, Roberto University of PisaItaly U-turn: Forward-driven backward analysis for incorrectness
Florian BruseBruse, Florian University of KasselGermany Space-Efficient Model-Checking of Higher-Order Recursion Schemes
Dakota BryanBryan, Dakota Committee Member in Student Volunteers for POPL 2025
Mario BucevBucev, Mario EPFLSwitzerland Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
William E. ByrdByrd, William E. University of Alabama at Birmingham, USAUnited States VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
C Yufan CaiCai, Yufan National University of Singapore Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
Julie CaillerCailler, Julie LIRMM Committee Member in Artifact Evaluation Committee within the VMCAI-track
Brian CampbellCampbell, Brian University of Edinburgh A CHERI C Memory Model for Verified Temporal Safety
Ronaldo CanizalesCanizales, Ronaldo Committee Member in Student Volunteers for POPL 2025
Lauren CapellutoCapelluto, Lauren AWS Quantum Technologies AutoQASM: Imperative quantum programming in Python
Michael CarbinCarbin, Michael Massachusetts Institute of TechnologyUnited States Inference Plans for Hybrid Particle Filtering
Jacques CaretteCarette, Jacques McMaster UniversityCanada Author in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the WITS-track
Mario CarneiroCarneiro, Mario CMUUnited States Session Chair of Session 7 (part of CPP) PC Member in Program Committee within the CPP-track
Manuel CarroCarro, Manuel IMDEA Software Institute and Universidad Politécnica de MadridSpain Committee Member in Program Committee within the PADL-track
Pedro CarrottCarrott, Pedro Imperial College LondonUnited Kingdom Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation
William CashmanCashman, William University of Oxford Fusion and flow: formal protocols to reliably build photonic graph states
Chris CasinghinoCasinghino, Chris Jane Street Session Chair of Jane Street Social Event (part of POPL ) Jane Street Game Night Data Race Freedom à la Mode
Federico CassanoCassano, Federico Northeastern University DafnyBench: A Benchmark for Formal Software Verification VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Laura M. CastroCastro, Laura M. University of A CoruñaSpain Committee Member in Program Committee within the PADL-track
Ethan CecchettiCecchetti, Ethan University of Wisconsin-MadisonUnited States Leveraging Duality for Programming with zkSNARKs Universal Composability is Robust Compilation
Martin CeresaCeresa, Martin IMDEA Software InstituteSpain MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs
Jahrim Gabriele CesarioCesario, Jahrim Gabriele University of St. GallenItaly Dis/Equality Graphs
Joris CeulemansCeulemans, Joris KU LeuvenBelgium BiSikkel: A Multimode Logical Framework in Agda
Devora Chait-RothChait-Roth, Devora New York UniversityUnited States Committee Member in Student Volunteers for POPL 2025 Constructing Trustworthy Smart Contracts
Tej ChajedChajed, Tej UW-MadisonUnited States PC Member in Program Committee within the Dafny-track
Debraj ChakrabortyChakraborty, Debraj Masaryk UniversityIndia 1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Saikat ChakrabortyChakraborty, Saikat Microsoft ResearchUnited States Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Soham ChakrabortyChakraborty, Soham TU DelftNetherlands Relaxed Memory Concurrency Re-executed PC Member in Program Committee within the VMCAI-track
Jonathan ChanChan, Jonathan University of PennsylvaniaCanada Committee Member in Student Volunteers for POPL 2025 Consistency of a Dependent Calculus of Indistinguishability
Kartik ChandraChandra, Kartik MITUnited States A Domain-Specific PPL for Reasoning about Reasoning (or: a memo on memo) Semantics of the memo Probabilistic Programming Language
Satish ChandraChandra, Satish Google, IncUnited States Committee Member in Program Committee within the POPL -track
Bor-Yuh Evan ChangChang, Bor-Yuh Evan University of Colorado Boulder & AmazonUnited States Session Chair of Second Session (part of PLMW @ POPL) Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms Organizer in Organizing Committee within the PLMW @ POPL-track
Le ChangChang, Le University of Maryland, College Park The Quantum Abstract Machine
Nicolas ChappeChappe, Nicolas Inria Lyon, LIP Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IR
Christopĥe CharetonChareton, Christopĥe CEA, LIST, France Committee Member in Program Committee within the PLanQC-track
Sarah E. ChasinsChasins, Sarah E. University of California at BerkeleyUnited States Committee Member in Program Committee within the POPL -track
Samuel ChassotChassot, Samuel EPFL, LARASwitzerland Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
Agnishom ChattopadhyayChattopadhyay, Agnishom ImironJapan Verified and Efficient Matching of Regular Expressions with Lookaround
Alain Chavarri VillarelloChavarri Villarello, Alain Vrije Universiteit Amsterdam Certifying rings of integers in number fields
Dong ChenChen, Dong Huawei Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Hanxi ChenChen, Hanxi University of Pennsylvania Committee Member in Student Volunteers for POPL 2025 Vellvm: Formalizing the Informal
Liang-Ting ChenChen, Liang-Ting Academia SinicaTaiwan Committee Member in Program Committee Members within the PEPM-track
Liqian ChenChen, Liqian National University of Defense TechnologyChina Affine Disjunctive Invariant Generation with Farkas’ Lemma
Sheng ChenChen, Sheng University of Louisiana at Lafayette Committee Member in Program Committee within the POPL -track
Tony ChenChen, Tony MIT A Domain-Specific PPL for Reasoning about Reasoning (or: a memo on memo)
Xin ChenChen, Xin University of New Mexico, USAUnited States Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training PC Member in Program Committee within the VMCAI-track
Yi-Ting ChenChen, Yi-Ting AWS Quantum Technologies AutoQASM: Imperative quantum programming in Python
Yo-Ga ChenChen, Yo-Ga Academia Sinica Committee Member in Student Volunteers for POPL 2025 An Automata-based Framework for Quantum Circuit Verification Verifying Quantum Circuits with Level-Synchronized Tree Automata
Yu-Fang ChenChen, Yu-Fang Academia SinicaTaiwan An Automata-based Framework for Quantum Circuit Verification Verifying Quantum Circuits with Level-Synchronized Tree Automata
James CheneyCheney, James University of EdinburghUnited Kingdom Nominal Matching Logic With Fixpoints Committee Member in Program Committee within the POPL -track
Ellie Y. ChengCheng, Ellie Y. MITUnited States Inference Plans for Hybrid Particle Filtering
Alvin CheungCheung, Alvin University of California at BerkeleyUnited States Flo: a Semantic Foundation for Progressive Stream Processing
Louis CheungCheung, Louis University of Melbourne Formalized Burrows-Wheeler Transform
Kshitij ChhabraChhabra, Kshitij AWS Quantum Technologies AutoQASM: Imperative quantum programming in Python
Michele ChiariChiari, Michele TU WienAustria Exact Inference for Nested Discrete Probabilistic Programs (Remote)
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Session Chair of Separation Logic (part of POPL ) Collapsing Towers for Side-Channel Security (Short Paper) Committee Member in Program Committee within the POPL -track Committee Member in Steering Committee within the CPP-track
Minki ChoCho, Minki Seoul National UniversitySouth Korea Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
David ChocholatýChocholatý, David Brno University of TechnologyCzechia Committee Member in Artifact Evaluation Committee within the VMCAI-track
Vikraman ChoudhuryChoudhury, Vikraman Università di Bologna & Inria OLASItaly Session Chair of Semantic models (part of POPL ) Semantic Analysis of Normalisation for Directional Logic Programming Intrinsically Correct Sorting in Cubical Agda Towards Quantum Multiparty Session Types The Duality of λ-Abstraction
Eloise ChristianChristian, Eloise Rochester Institute of TechnologyUnited States Committee Member in Student Volunteers for POPL 2025
Cheng-En ChuangChuang, Cheng-En University at BuffaloUnited States Semantic Logical Relations for Timed Message-Passing Protocols
Kai-Min ChungChung, Kai-Min Academia Sinica An Automata-based Framework for Quantum Circuit Verification
Jonathan CitrinCitrin, Jonathan Google Deepmind Invited talk: TORAX - A Fast and Differentiable Tokamak Transport Simulator in JAX (Remote)
Pierre ClairambaultClairambault, Pierre CNRS & LIS, Aix-Marseille UniversitéFrance Committee Member in Program Committee within the POPL -track
Rance CleavelandCleaveland, Rance University of Maryland The Quantum Abstract Machine
Basile ClémentClément, Basile OCamlProFrance Tail Modulo Cons, OCaml, and Relational Separation Logic
Albert CohenCohen, Albert Google DeepMindFrance Committee Member in Program Committee within the POPL -track
Joshua M. CohenCohen, Joshua M. Princeton University Implementing OCaml APIs in Coq Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Andrea ColledanColledan, Andrea University of Bologna & INRIA Sophia Antipolis Size Analysis of Imperative Quantum Circuit Building Programs Through Floyd-Hoare Logics Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
Nicholas ColtharpColtharp, Nicholas Portland State UniversityUnited States Committee Member in Student Volunteers for POPL 2025
Johan CommelinCommelin, Johan University of Utrecht PC Member in Program Committee within the CPP-track
Youyou CongCong, Youyou Institute of Science TokyoJapan Committee Member in Program Committee Members within the PEPM-track
Giovanna Kobus ConradoConrado, Giovanna Kobus Hong Kong University of Science and TechnologyHong Kong Program Analysis via Multiple Context Free Language Reachability
Breandan ConsidineConsidine, Breandan McGill UniversityCanada Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Arthur CorrensonCorrenson, Arthur CISPA Helmholtz Center for Information Security Coinductive Proofs for Temporal Hyperliveness
Carlos Tome CortinasCortinas, Carlos Tome None Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Patrick CousotCousot, Patrick Calculational Design of Hyperlogics by Abstract Interpretation PC Member in Program Committee within the VMCAI-track
Maria-Nicoleta CraciunCraciun, Maria-Nicoleta University of Oxford NP-NUTS: A Nonparametric No-U-Turn Sampler Data-oriented Design for Differentiable, Probabilistic Programming (Remote)
Chen CuiCui, Chen University of Hong KongChina Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
Joseph W. CutlerCutler, Joseph W. University of Pennsylvania Getting the Most Out of POPL
Jack CzenszakCzenszak, Jack Northeastern University Towards Symbolic Execution for Probability and Non-determinism
D Loris D'AntoniD'Antoni, Loris University of California, San DiegoUnited States Finding Good Programs by Avoiding Bad Ones PC Member in Program Committee within the VMCAI-track
Anthony D'ArienzoD'Arienzo, Anthony University of Illinois and Sandia National LaboratoriesUnited States Reasoning About Sampling Without Sampling: Atomic Machines for Contextual Equivalence in Probabilistic Programs
Emanuele D'OsualdoD'Osualdo, Emanuele University of KonstanzGermany Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
Vijay D'SilvaD'Silva, Vijay Google Inc. PC Member in Program Committee within the VMCAI-track
Deepak D'SouzaD'Souza, Deepak IISc BangaloreIndia PC Member in Program Committee within the VMCAI-track
Sander R. DahmenDahmen, Sander R. Vrije Universiteit Amsterdam Certifying rings of integers in number fields
Ugo Dal LagoDal Lago, Ugo University of Bologna & INRIA Sophia AntipolisItaly Size Analysis of Imperative Quantum Circuit Building Programs Through Floyd-Hoare Logics Towards Quantum Multiparty Session Types Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
Stefania DamatoDamato, Stefania University of NottinghamUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Lesly-Ann DanielDaniel, Lesly-Ann CEA ListFrance Committee Member in Program Committee within the PriSC-track
David DaraisDarais, David GaloisUnited States Committee Member in Program Committee within the POPL -track
Thibault DardinierDardinier, Thibault ETH ZurichSwitzerland Session Chair of Program Logics 2 (part of POPL ) Formal Foundations for Translational Separation Logic Verifiers Viper: An Infrastructure for Automated Verification in Separation Logic
Kanak DasDas, Kanak University of California, RiversideUnited States Committee Member in Student Volunteers for POPL 2025
Sopam DasguptaDasgupta, Sopam C3G: Causally Constrained Counterfactual Generation
Davide DavoliDavoli, Davide Université Côte d’Azur, InriaFrance A quantitative probabilistic relational Hoare logic
Ana de Almeida Borgesde Almeida Borges, Ana Portugal PC Member in Program Committee within the CPP-track
Luis Eduardo Bueso de Barriode Barrio, Luis Eduardo Bueso Universidad Politécnica de MadridSpain Haskell Based Spreadsheets
Giovanni de Felicede Felice, Giovanni Quantinuum Fusion and flow: formal protocols to reliably build photonic graph states
Arianne Meijer-van de Griendde Griend, Arianne Meijer-van University of Helsinki Committee Member in Program Committee within the PLanQC-track
Tom de Jongde Jong, Tom University of NottinghamUnited Kingdom PC Member in Program Committee within the CPP-track
Robin De VogelaereDe Vogelaere, Robin KU Leuven A practical approach to handling tabular data in logic
Benjamin DelawareDelaware, Benjamin Purdue UniversityUnited States Session Chair of Quantum Computing 1 (part of POPL ) Session Chair of Session 2 (part of CoqPL) Session Chair of Session 3 (part of CoqPL) Towards Automated Verification of LLM-Synthesized C Programs From Traces to Program Incorrectness: A Type-Theoretic Approach Co-chair in Program Committee within the CoqPL-track
Ramiro DemasiDemasi, Ramiro Universidad Nacional de Córdoba Committee Member in Artifact Evaluation Committee within the VMCAI-track
Farzaneh DerakhshanDerakhshan, Farzaneh Illinois Institute of TechnologyUnited States Committee Member in Program Committee within the PriSC-track
Vladislav DeryabkinDeryabkin, Vladislav Innopolis University Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
Harsh DesaiDesai, Harsh Carnegie Mellon University An MLIR Dialect for WebAssembly
Jyotirmoy DeshmukhDeshmukh, Jyotirmoy University of Southern California Session Chair of Applications (part of VMCAI) Keynote Talk: Formal methods in a model-free, data-driven world PC Member in Program Committee within the VMCAI-track
Dominique DevrieseDevriese, Dominique KU LeuvenBelgium BiSikkel: A Multimode Logical Framework in Agda
Alessandra Di PierroDi Pierro, Alessandra University of VeronaItaly A Static Analysis of Entanglement
Antonio Di StasioDi Stasio, Antonio City St George’s, University of London Committee Member in Artifact Evaluation Committee within the VMCAI-track
Rayna DimitrovaDimitrova, Rayna CISPA Helmholtz Center for Information Security Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
Christos DimoulasDimoulas, Christos Northwestern UniversityUnited States Committee Member in Program Committee within the POPL -track
Tingting DingDing, Tingting University of Michigan Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
Jenna DiVincenzo (Wise)DiVincenzo (Wise), Jenna Purdue University PLMW Panel Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification Gradual C0: Symbolic Execution for Gradual Verification
Mike DoddsDodds, Mike Galois, IncUnited States PLMW Panel
Marko DokoDoko, Marko Heriot-Watt University, UK CoqNFU: Towards Formalizing NFU in Coq
Stephen DolanDolan, Stephen Jane StreetUnited Kingdom Data Race Freedom à la Mode
Alastair F. DonaldsonDonaldson, Alastair F. Imperial College LondonUnited Kingdom Randomised Testing of the Dafny Compiler: Into the CI PC Member in Program Committee within the Dafny-track
Jin Song DongDong, Jin Song National University of SingaporeSingapore Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
Rui DongDong, Rui University of MichiganUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Myra DotzelDotzel, Myra Carnegie Mellon UniversityUnited States Intermittent Concurrency
Derek DreyerDreyer, Derek MPI-SWSGermany Session Chair of Program Logics 1 (part of POPL ) How to Write Papers So People Can Read Them A Semantic Approach to Robust Property Preservation Data Race Freedom à la Mode
Claire DrossDross, Claire AdaCoreFrance Two-way collaboration between flow and proof in SPARK
Ross DuncanDuncan, Ross Quantinuum Session Chair of Session 3 (part of PLanQC) HUGR: A Quantum-Classical Intermediate Representation Imperative Quantum Programming with Ownership and Borrowing in Guppy
Ross DuncanDuncan, Ross Quantinuum Organizing Committee in Organizing Committee within the PLanQC-track
Alejandro Díaz-CaroDíaz-Caro, Alejandro INRIA / LORIA & UNQFrance Committee Member in Program Committee within the PLanQC-track
E Gabriel EbnerEbner, Gabriel Microsoft Research Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming Symbolic Automata: omega-Regularity Modulo Theories
Amirali EbrahimzadehEbrahimzadeh, Amirali Committee Member in Student Volunteers for POPL 2025
Alec EdgingtonEdgington, Alec Quantinuum HUGR: A Quantum-Classical Intermediate Representation
Paul EichlerEichler, Paul CISPA - Helmholtz Center for Information SecurityGermany Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
Richard A. EisenbergEisenberg, Richard A. Jane StreetUnited States Session Chair of Jane Street Social Event (part of POPL ) Invited Talk: Type inference in OCaml and GHC using Levels Jane Street Game Night Data Race Freedom à la Mode
Neta EladElad, Neta Tel Aviv UniversityIsrael Axe 'Em: Eliminating Spurious States with Induction Axioms
Laila ElbeheiryElbeheiry, Laila MPI-SWS Data Race Freedom à la Mode
Mohamed ElwakilElwakil, Mohamed U.S. Coast Guard AcademyUnited States Automatic Inference of Enclave Placement in LLVM Compiler
Michael EmmiEmmi, Michael Amazon Web ServicesUnited States Committee Member in Program Committee within the POPL -track
Frank EmrichEmrich, Frank University of Edinburgh, UK Continuing Stack Switching in Wasmtime
Sune Skaanning EngtorpEngtorp, Sune Skaanning Department of Computer Science, University of Copenhagen A Type Safe Calculus for Generating Syntax-Directed Editors
Esra ErdemErdem, Esra Sabanci UniversityTurkey Session Chair of Session 5 (part of PADL) Co-chair in Programme Chairs within the PADL-track
Sebastian ErdwegErdweg, Sebastian JGU MainzGermany A Framework of Differential Operators
Julian ErhardErhard, Julian LMU Munich; TU MunichGermany Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
Ian Erik VarataluErik Varatalu, Ian Tallinn University of Technology, EstoniaEstonia Committee Member in Student Volunteers for POPL 2025 RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds
Juhan ErnitsErnits, Juhan Tallinn University of TechnologyEstonia RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds
Zafer EsenEsen, Zafer Uppsala UniversitySweden Committee Member in Artifact Evaluation Committee within the VMCAI-track
Guilherme EspadaEspada, Guilherme LASIGE, University of LisbonPortugal Committee Member in AV Committee for POPL 2025
F Xaver FabianFabian, Xaver CISPA Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks Committee Member in Program Committee within the PriSC-track
Claudia FaggianFaggian, Claudia Université de Paris & CNRS Committee Member in Program Committee within the LAFI-track
Sarah FakhouryFakhoury, Sarah Microsoft ResearchUnited States Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Chris FallinFallin, Chris F5United States Full-Stack Correctness in Wasm: Eliminating Bugs Inside and Outside the Sandbox Author in Steering Committee within the PriSC-track
Andong FanFan, Andong University of Toronto Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Dongliang FangFang, Dongliang Beijing Key Laboratory of IOT Information Security Technology, Institute of Information Engineering, CAS, China; School of Cyber Security, University of Chinese Academy of Sciences, ChinaChina Automated Flaw Detection for Industrial Robot RESTful Service
Yuzhou FangFang, Yuzhou University of Southern CaliforniaUnited States An Incremental Algorithm for Algebraic Program Analysis
Simone FaroFaro, Simone University of Catania Qutes: a Pathway to High-Level Quantum Programming
Marie FarrellFarrell, Marie The University of ManchesterUnited Kingdom PC Member in Program Committee within the Dafny-track
Azadeh FarzanFarzan, Azadeh University of TorontoCanada Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning Committee Member in Program Committee within the POPL -track
Sakina FatimaFatima, Sakina University of OttawaCanada Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Daniel FeldanFeldan, Daniel New York University Committee Member in Artifact Evaluation Committee within the VMCAI-track
Simon FelixFelix, Simon Ateleris GmbHSwitzerland Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
Qiuyi FengFeng, Qiuyi Formal Verification of Quantum Stabilizer Code
Maribel FernandezFernandez, Maribel King's College LondonUnited Kingdom Nominal Matching Logic With Fixpoints
Jack FeserFeser, Jack BasisUnited States Industry Talk: Basis - Programming Languages as Core Technology for AI
Nathaniel FilardoFilardo, Nathaniel University of Cambridge A CHERI C Memory Model for Verified Temporal Safety
Bernd FinkbeinerFinkbeiner, Bernd CISPA Helmholtz Center for Information SecurityGermany Coinductive Proofs for Temporal Hyperliveness
Denis FirsovFirsov, Denis Tallinn University of TechnologyEstonia Leakage-Free Probabilistic Jasmin Programs
Cormac FlanaganFlanagan, Cormac University of California at Santa Cruz Committee Member in Program Committee within the POPL -track
Eugene FlesselleFlesselle, Eugene EPFLSwitzerland System $F^\omega$ with Coherent Implicit Resolution System $F^\omega$ with Coherent Implicit Resolution
Christian FontenotFontenot, Christian University of Colorado Boulder Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms
Yannick ForsterForster, Yannick INRIAFrance Organizer in Organizing Committee within the PLMW @ POPL-track
Frédéric FortFort, Frédéric University of Lille Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jeffrey S. FosterFoster, Jeffrey S. Tufts UniversityUnited States Committee Member in Program Committee within the POPL -track
José Fragoso SantosFragoso Santos, José INESC-ID/Instituto Superior Técnico, Portugal Committee Member in Program Committee within the POPL -track
Franz FranchettiFranchetti, Franz Carnegie Mellon University, USA Towards Semantics Lifting for Scientific Computing: A Case Study on FFT
Mario FrankFrank, Mario University of PotsdamGermany Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Mike FranusichFranusich, Mike SpiralGen, Inc. Towards Semantics Lifting for Scientific Computing: A Case Study on FFT
Lars-Åke FredlundFredlund, Lars-Åke Universidad Politécnica de MadridSpain Checking Concurrency Coding Rules
Cameron FreerFreer, Cameron Massachusetts Institute of TechnologyUnited States Committee Member in Steering Committee within the LAFI-track
Asta Halkjær FromFrom, Asta Halkjær University of Copenhagen An Isabelle/HOL Framework for Synthetic Completeness Proofs
Daniel FruminFrumin, Daniel University of GroningenNetherlands PC Member in Program Committee within the CPP-track
Hongfei FuFu, Hongfei Shanghai Jiao Tong UniversityChina Affine Disjunctive Invariant Generation with Farkas’ Lemma
Peng FuFu, Peng University of South Carolina Session Chair of Session 2 (part of PLanQC) Proto-Quipper with Reversing and Control
Zhoulai FuFu, Zhoulai State University of New York, Korea On Extending Incorrectness Logic with Backwards Reasoning
G Marco GaboardiGaboardi, Marco Boston UniversityUnited States Domain Reasoning In TopKAT: Reduction and Completeness
Joshua GancherGancher, Joshua Northeastern UniversityUnited States ILA: Correctness via Type Checking for Fully Homomorphic Encryption Committee Member in Program Committee within the PriSC-track
Deepti GandluriGandluri, Deepti Google Beyond the Baseline: Experimental WebAssembly for High Performance
Luis Hernan Garcia PaucarGarcia Paucar, Luis Hernan Aston UniversityUnited Kingdom A Complete Translation from Planning Problems to linear logic
Ronald GarciaGarcia, Ronald University of British ColumbiaCanada PLMW Panel
Isabel Garcia-ContrerasGarcia-Contreras, Isabel University of WaterlooCanada Automatic Inference of Relational Object Invariants
Philippa GardnerGardner, Philippa Imperial College LondonUnited Kingdom Progressful Interpreters for Efficient WebAssembly Mechanisation Committee Member in Program Committee within the WAW-track
Deepak GargGarg, Deepak MPI-SWSGermany A Semantic Approach to Robust Property Preservation Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
Poorva GargGarg, Poorva University of California, Los AngelesIndia Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Antoine GaulinGaulin, Antoine McGill University McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
Simon J. GayGay, Simon J. University of Glasgow, UKUnited Kingdom The Duality of λ-Abstraction
Lorenzo GazzellaGazzella, Lorenzo Università di Pisa Calculational design of Incorrectness Separation Logic
Hong GeGe, Hong University of Cambridge State Space Model Programming in Turing.jl
Martin GebserGebser, Martin University of Klagenfurt, AustriaAustria Committee Member in Program Committee within the PADL-track
Timon GehrGehr, Timon ETH ZurichSwitzerland Committee Member in Program Committee within the POPL -track
Aina Linn GeorgesGeorges, Aina Linn Max Planck Institute for Software Systems (MPI-SWS) A Semantic Approach to Robust Property Preservation The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic Data Race Freedom à la Mode
Roberto GiacobazziGiacobazzi, Roberto University of ArizonaUnited States The Best of Abstract Interpretations Adversities in Abstract Interpretation - Accommodating Robustness by Abstract Interpretation PC Member in Program Committee within the VMCAI-track
Mirco GiacobbeGiacobbe, Mirco University of BirminghamUnited Kingdom Loop Invariants Using Neural Networks
Gaetan GilbertGilbert, Gaetan All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
Eric GiovanniniGiovannini, Eric University of MichiganUnited States Committee Member in Student Volunteers for POPL 2025 Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
Marco GIUNTIGIUNTI, Marco University of Oxford Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Simon J. GodsillGodsill, Simon J. Department of Engineering, University of Cambridge State Space Model Programming in Turing.jl
Stefano GogiosoGogioso, Stefano University of Oxford The Focked-up ZX Calculus: Picturing Continuous-Variable Quantum Computation
Amir Kafshdar GoharshadyGoharshady, Amir Kafshdar Hong Kong University of Science and TechnologyHong Kong PC Member in Program Committee within the VMCAI-track
Priyanka GoliaGolia, Priyanka Indian Institute of Technology, Kanpur, India and National University of Singapore, Singapore Committee Member in Program Committee within the VMCAI-track
Anitha GollamudiGollamudi, Anitha University of Massachusetts LowellUnited States Automatic Inference of Enclave Placement in LLVM Compiler ILA: Correctness via Type Checking for Fully Homomorphic Encryption
Tarakaram GollamudiGollamudi, Tarakaram None A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types ILA: Correctness via Type Checking for Fully Homomorphic Encryption
Pavel GolovinGolovin, Pavel MPI-SWSGermany RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
Hannah GommerstadtGommerstadt, Hannah Vassar College Diversity, Equity, and Inclusion Chair in Organizing Committee for POPL 2025
Sergey GoncharovGoncharov, Sergey University of Birmingham, School of Comp. Sci. Abstract Operational Methods for Call-by-Push-Value
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
April GonçalvesGonçalves, April University of Strathclyde Type-Sensitive Algebraic Macros (Short Paper)
Daniel GoodmanGoodman, Daniel Oracle LabsUnited Kingdom Sandwood: Runtime Adaptable Probabilistic Programming for Java (Remote)
Bhavik Kamlesh GoplaniGoplani, Bhavik Kamlesh University of Kansas APIdemic: Verifying Idempotency of REST API Clients
Andrew D. GordonGordon, Andrew D. Cogna and University of EdinburghUnited Kingdom Committee Member in Program Committee within the LAFI-track
Jacob GorenburgGorenburg, Jacob Gradual C0: Symbolic Execution for Gradual Verification
Roberta GoriGori, Roberta Diaprtimento di Informatica, Universita' di Pisa, Italy U-turn: Forward-driven backward analysis for incorrectness
Roberta GoriGori, Roberta University of PisaItaly Committee Member in Program Committee within the TPSA-track
Roberta GoriGori, Roberta Diaprtimento di Informatica, Universita' di Pisa, Italy Committee Member in Program Committee within the POPL -track
Felipe GorostiagaGorostiaga, Felipe IMDEA Software Institute MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs
Eric GoubaultGoubault, Eric Ecole Polytechnique PC Member in Program Committee within the VMCAI-track
Hemant GouniGouni, Hemant Carnegie Mellon University, Pittsburgh, Pennsylvania, United StatesUnited States Gradual C0: Symbolic Execution for Gradual Verification
Daniel GratzerGratzer, Daniel Aarhus UniversityDenmark A modal deconstruction of Löb induction
Neville GrechGrech, Neville Dedaub LimitedMalta Committee Member in Program Committee within the POPL -track
Michael GreenbergGreenberg, Michael Stevens Institute of TechnologyUnited States Industrial Relations Co-Chair in Organizing Committee for POPL 2025 How to give a good talk
Simon Oddershede GregersenGregersen, Simon Oddershede New York UniversityUnited States Session Chair of Probabilistic Programming 2 (part of POPL ) Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Benjamin GregoireGregoire, Benjamin INRIA Preservation of Speculative Constant-time by Compilation Preservation of speculative constant-time by compilation A quantitative probabilistic relational Hoare logic
Karuna GrewalGrewal, Karuna Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Eric GriffisGriffis, Eric University of MichiganUnited States Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
Radu GrigoreGrigore, Radu Meta Improving Static Analysis using Information Collected at Runtime
Jason GrossGross, Jason MIT CSAILUnited States PC Member in Program Committee within the CPP-track
Marco GuarnieriGuarnieri, Marco IMDEA Software InstituteSpain Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks Author in Steering Committee within the PriSC-track
Shibashis GuhaGuha, Shibashis Tata Institute of Fundamental Research, IndiaIndia PC Member in Program Committee within the VMCAI-track
Ashutosh GuptaGupta, Ashutosh Indian Institute of Technology BombayIndia PC Member in Program Committee within the VMCAI-track
Gopal GuptaGupta, Gopal Automated Playing of Survival Video Games with Commonsense Reasoning (short paper) C3G: Causally Constrained Counterfactual Generation Exploring Answer Set Programming for Provenance Graph-Based Cyber Threat Detection: A Novel Approach Committee Member in Program Committee within the PADL-track
Priyam GuptaGupta, Priyam Purdue University Committee Member in Student Volunteers for POPL 2025 Increasing the Expressiveness of a Gradual Verifier
Arie GurfinkelGurfinkel, Arie University of WaterlooCanada Session Chair of Model Checking (part of VMCAI) Automatic Inference of Relational Object Invariants
H Sebastian HackHack, Sebastian Saarland University, Saarland Informatics CampusGermany Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
Ernst Moritz HahnHahn, Ernst Moritz University of TwenteNetherlands Co-chair in Artifact Evaluation Committee within the VMCAI-track Artifact Evaluation Co-Chair in Organizing Committee within the VMCAI-track
Philipp HallerHaller, Philipp KTH Royal Institute of TechnologySweden Committee Member in Program Committee within the POPL -track
Zachary HansenHansen, Zachary University of Nebraska Omaha SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic
Michael HanusHanus, Michael Kiel UniversityGermany Session Chair of Language design, pedagogical tool, and staged interpreter (part of PEPM) Session Chair of Session 2 (part of PADL) Can Logic Programming Be Liberated from Predicates and Backtracking? (Lightning talk) Committee Member in Program Committee within the PADL-track
Bryant HargreavesHargreaves, Bryant University of Texas at Dallas, USA Automated Playing of Survival Video Games with Commonsense Reasoning (short paper)
Tim HargreavesHargreaves, Tim Department of Engineering, University of CambridgeUnited Kingdom State Space Model Programming in Turing.jl
Matthew P HarriganHarrigan, Matthew P Google Quantum AI Expressing and Analyzing Quantum Algorithms with Qualtran
Philipp G. HaselwarterHaselwarter, Philipp G. Aarhus UniversityDenmark Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Keishi HASHIBAHASHIBA, Keishi The University of OsakaJapan Characterizations of Partial Well-Behaved Lenses
Muhammad HassnainHassnain, Muhammad University of California, Davis Counterexamples in Safe Rust
Deyuan (Mike) HeHe, Deyuan (Mike) Princeton UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Rasmus HebsgaardHebsgaard, Rasmus Aalborg UniversityDenmark ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks
Lukas HeidemannHeidemann, Lukas Quantinuum HUGR: A Quantum-Classical Intermediate Representation
Katharina HeidlerHeidler, Katharina Technical University Munich Formalizing the One-way to Hiding Theorem
Philippe HeimHeim, Philippe CISPA Helmholtz Center for Information Security Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
Lukas HeinrichHeinrich, Lukas TU MunichGermany Committee Member in Program Committee within the LAFI-track
Matthias HeizmannHeizmann, Matthias University of Freiburg, GermanyGermany Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
Joseph M. HellersteinHellerstein, Joseph M. UC BerkeleyUnited States Flo: a Semantic Foundation for Progressive Stream Processing
Fritz HengleinHenglein, Fritz Department of Computer Science, University of Copenhagen (DIKU) and Deon DigitalDenmark Committee Member in Program Committee Members within the PEPM-track
Simon HennigerHenniger, Simon Technical University of Munich Committee Member in Student Volunteers for POPL 2025 VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Ludovic HenrioHenrio, Ludovic University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIPFrance Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IR
Manuel HermenegildoHermenegildo, Manuel Technical University of Madrid (UPM) and IMDEA Software InstituteSpain Committee Member in Program Committee Members within the PEPM-track
Ángel HerranzHerranz, Ángel Universidad Politécnica de MadridSpain Checking Concurrency Coding Rules Logic Programming with Extensible Types (Lightning talk)
Chris HeunenHeunen, Chris University of EdinburghUnited Kingdom Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
Michal HečkoHečko, Michal Brno University of Technology Committee Member in Artifact Evaluation Committee within the VMCAI-track
Daniel HillerströmHillerström, Daniel Category Labs and The University of EdinburghUnited Kingdom Continuing Stack Switching in Wasmtime
Kengo HirataHirata, Kengo University of Edinburgh Concurrent Quantum Separation Logic for Fine-Grained Parallelism Concurrent Quantum Separation Logic for Fine-Grained Parallelism Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
Andrew K. HirschHirsch, Andrew K. University at Buffalo, SUNYUnited States Session Chair of Third Session (part of PLMW @ POPL) Organizer in Organizing Committee within the PLMW @ POPL-track
Florent HivertHivert, Florent Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA Machine Checked Proofs and Programs in Algebraic Combinatorics
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the POPL -track
Steven HoltzenHoltzen, Steven Northeastern UniversityUnited States Towards Symbolic Execution for Probability and Non-determinism Committee Member in Program Committee within the POPL -track Committee Member in Steering Committee within the LAFI-track
Lukáš HolíkHolík, Lukáš Brno University of TechnologyCzechia An Automata-based Framework for Quantum Circuit Verification Verifying Quantum Circuits with Level-Synchronized Tree Automata
Kuen-Bang Hou (Favonia)Hou (Favonia), Kuen-Bang University of MinnesotaUnited States Committee Member in Program Committee within the WITS-track
Zhe HouHou, Zhe Griffith University Generically Automating Separation Logic by Functors, Homomorphisms, and Modules Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
Farzin HoushmandHoushmand, Farzin Google TensorRight: Automated Verification of Tensor Graph Rewrites
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany My Journey in Secure Compilation Steering Committee Chair in Steering Committee within the CPP-track Author in Steering Committee within the PriSC-track
Justin HsuHsu, Justin Cornell UniversityUnited States Committee Member in Program Committee within the POPL -track
Jason Z.S. HuHu, Jason Z.S. Amazon Web Services, USAUnited States McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory A Dependent Type Theory for Meta-programming with Intensional Analysis
Sabrina Ruixin HuHu, Sabrina Ruixin Harvard VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Zhenjiang HuHu, Zhenjiang Peking UniversityChina Biparsers: Exact Printing for Data Synchronisation Committee Member in Program Committee Members within the PEPM-track
Yipeng HuangHuang, Yipeng Rutgers UniversityUnited States Sdim: A Qudit Stabilizer Simulator
Joffrey HuguetHuguet, Joffrey AdaCoreFrance Two-way collaboration between flow and proof in SPARK
Chung-Kil HurHur, Chung-Kil Seoul National UniversitySouth Korea CRIS: The power of imagination in specification and verification Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
Adam Husted KjelstrømHusted Kjelstrøm, Adam Efficient Strong Simulation of High-level Quantum Gates Efficient Strong Simulation of High-level Quantum Gates
Hans HüttelHüttel, Hans Department of Computer Science, Aalborg UniversityDenmark A Type Safe Calculus for Generating Syntax-Directed Editors
I Daniela InclezanInclezan, Daniela Miami UniversityUnited States Session Chair of Session 7 (part of PADL)
Daniela InclezanInclezan, Daniela Miami University, USA ASP for Language Documentation and Reclamation: A Derivational Stemming Tool for Myaamia
Daniela InclezanInclezan, Daniela Miami UniversityUnited States Committee Member in Program Committee within the PADL-track
Apoorv IngleIngle, Apoorv University of IowaUnited States Committee Member in AV Committee for POPL 2025
Grant IraciIraci, Grant University at BuffaloUnited States Semantic Logical Relations for Timed Message-Passing Protocols
Daisuke IshiiIshii, Daisuke JAISTJapan A Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic
Laura IsraelIsrael, Laura Portland State UniversityUnited States Committee Member in Student Volunteers for POPL 2025
Franjo IvancicIvancic, Franjo GoogleUnited States PC Member in Program Committee within the VMCAI-track
Fedor IvanovIvanov, Fedor Innopolis University Towards Generic Higher-Order Unification Implementations in Haskell
Desi R. IvavonaIvavona, Desi R. University of Oxford Invited talk: Modern Bayesian Experimental Design
Ilan IwumbweIwumbwe, Ilan Imperial College LondonUganda QuteFuzz: Fuzzing quantum compilers using randomly generated circuits with control flow and subcircuits
Yusuf IzmirliogluIzmirlioglu, Yusuf United Kingdom Committee Member in Program Committee within the PADL-track
J Jules JacobsJacobs, Jules Cornell University A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
Swen JacobsJacobs, Swen CISPAGermany Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
Suresh JagannathanJagannathan, Suresh Purdue UniversityUnited States From Traces to Program Incorrectness: A Type-Theoretic Approach Derivative-Guided Symbolic Execution
Devansh JainJain, Devansh University of Illinois at Urbana-Champaign TensorRight: Automated Verification of Tensor Graph Rewrites
Marie-Christine JakobsJakobs, Marie-Christine LMU Munich, GermanyGermany PC Member in Program Committee within the VMCAI-track
Georges-Axel JaloyanJaloyan, Georges-Axel Amazon Web Services Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
JJ JamesJames, JJ Committee Member in Student Volunteers for POPL 2025
Junyoung JangJang, Junyoung McGill UniversityCanada McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
Tomi JanhunenJanhunen, Tomi Tampere UniversityFinland Committee Member in Program Committee within the PADL-track
Jean-Christophe JaskulaJaskula, Jean-Christophe AWS Quantum Technologies AutoQASM: Imperative quantum programming in Python
Barry JayJay, Barry Typed Program Analysis without Encodings
Martin JensenJensen, Martin Aarhus University CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
Sumit JhaJha, Sumit Florida International University, USAUnited States Committee Member in Program Committee within the VMCAI-track
Ranjit JhalaJhala, Ranjit UCSD Auditing Rust Crates Effectively
Ranjit JhalaJhala, Ranjit University of California at San DiegoUnited States Laurel: Unblocking Automated Verification with Large Language Models
Ranjit JhalaJhala, Ranjit UCSD Generic Refinement Types
Limin JiaJia, Limin Carnegie Mellon University An MLIR Dialect for WebAssembly Intermittent Concurrency Committee Member in Program Committee within the PriSC-track
Songlin JiaJia, Songlin Purdue University, USAUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Shengyi JiangJiang, Shengyi Committee Member in Student Volunteers for POPL 2025 Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
Saurabh JoshiJoshi, Saurabh Supra ResearchIndia LLOR: Automated Repair of OpenMP Programs
Ralf JungJung, Ralf ETH ZurichSwitzerland Student Research Competition Co-Chair in Organizing Committee for POPL 2025 Program logics à la carte Student Research Competition Chair in Selection Committee within the POPL Student Research Competition-track
K Robin KaarsgaardKaarsgaard, Robin University of Southern DenmarkDenmark Author in Selection Committee within the POPL Student Research Competition-track
M. Frans KaashoekKaashoek, M. Frans Massachusetts Institute of Technology, USA Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems
Ivan KabashnyiKabashnyi, Ivan JetBrains Research, Constructor University Bremen, Germany Relaxed Memory Concurrency Re-executed
Adeeb KabirKabir, Adeeb Rutgers University Sdim: A Qudit Stabilizer Simulator
Younesse KaddarKaddar, Younesse University of OxfordUnited Kingdom Data-oriented Design for Differentiable, Probabilistic Programming (Remote)
Gowtham KakiKaki, Gowtham University of Colorado at BoulderUnited States Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms Committee Member in Program Committee within the POPL -track
Cezary KaliszykKaliszyk, Cezary University of MelbourneAustralia Towards Mining Robust Coq Proof Patterns PC Member in Program Committee within the CPP-track
Benjamin Lucien KaminskiKaminski, Benjamin Lucien Saarland University; University College LondonGermany Partial Incorrectness Logic A Taxonomy of Hoare-Like Logics Committee Member in Program Committee within the TPSA-track Committee Member in Program Committee within the POPL -track
Sudeep KanavKanav, Sudeep LMU MunichGermany 1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Byeongjee KangKang, Byeongjee Carnegie Mellon UniversityUnited States An MLIR Dialect for WebAssembly
Jeehoon KangKang, Jeehoon KAISTSouth Korea PC Member in Program Committee within the CPP-track
Johannes KanigKanig, Johannes AdaCoreFrance Two-way collaboration between flow and proof in SPARK
Tobias KappéKappé, Tobias LIACS, Leiden University Algebras for Deterministic Computation are Inherently Incomplete CF-GKAT: Efficient Validation of Control-Flow Transformations
Nat KarmiosKarmios, Nat Imperial College LondonUnited Kingdom Committee Member in Student Volunteers for POPL 2025
Jingyu KeKe, Jingyu Shanghai Jiao Tong UniversityChina Affine Disjunctive Invariant Generation with Farkas’ Lemma
Chantal KellerKeller, Chantal Université Paris SaclayFrance Committee Member in Program Committee Members within the PEPM-track
Ariel E. KellisonKellison, Ariel E. Cornell UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
George KenisonKenison, George Liverpool John Moores University Simple Linear Loops: Algebraic Invariants and Applications
Eric KesslerKessler, Eric AWS Quantum Technologies AutoQASM: Imperative quantum programming in Python
Artem KhyzhaKhyzha, Artem Arm LtdUnited Kingdom Committee Member in Program Committee within the POPL -track
Donnacha Oisín KidneyKidney, Donnacha Oisín Imperial College LondonUnited Kingdom Formalising Graph Algorithms with Coinduction
Kentaro KikuchiKikuchi, Kentaro Tohoku University Characterizations of Partial Well-Behaved Lenses
Dohan KimKim, Dohan University of Innsbruck An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
Jinwoo KimKim, Jinwoo Seoul National University Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
Yonghyun KimKim, Yonghyun Seoul National University, South Korea Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
Yoonseung KimKim, Yoonseung Yale UniversityUnited States VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
Keegan KimbrellKimbrell, Keegan University of Texas at Dallas, USA Automated Playing of Survival Video Games with Commonsense Reasoning (short paper)
Zachary KincaidKincaid, Zachary Princeton UniversityUnited States Associate Chair in Program Committee within the POPL -track
Tijil KiranKiran, Tijil Rutgers University Sdim: A Qudit Stabilizer Simulator
Marisa KirisameKirisame, Marisa University of UtahUnited States Incremental Bidirectional Typing via Order Maintenance
Christina KirkKirk, Christina University of Innsbruck Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Kohei KishidaKishida, Kohei University of Illinois at Urbana-ChampaignUnited States Proto-Quipper with Reversing and Control
Thea KjeldsmarkKjeldsmark, Thea University of California, IrvineUnited States Committee Member in Student Volunteers for POPL 2025 Expanding the Scope of Grammar-Based Enumerative Testing
Adam Husted KjelstrømKjelstrøm, Adam Husted Aarhus UniversityDenmark Program Analysis via Multiple Context Free Language Reachability
Fredrik KjolstadKjolstad, Fredrik Stanford UniversityUnited States Committee Member in Program Committee within the POPL -track
Gerwin KleinKlein, Gerwin Proofcraft and UNSW SydneyAustralia Committee Member in Steering Committee within the CPP-track
Dominik KlumppKlumpp, Dominik University of FreiburgGermany Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
Charles KnippKnipp, Charles Federal Reserve Board of Governors, USA State Space Model Programming in Turing.jl
Hsiang-Shang ‘Josh’ KoKo, Hsiang-Shang ‘Josh’ Institute of Information Science, Academia SinicaTaiwan Committee Member in Program Committee within the POPL -track
Naoki KobayashiKobayashi, Naoki University of TokyoJapan Session Chair of Decision Procedures (part of POPL ) On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus Committee Member in Program Committee within the POPL -track
Mark KochKoch, Mark Quantinuum HUGR: A Quantum-Classical Intermediate Representation Imperative Quantum Programming with Ownership and Borrowing in Guppy
Jérémie KoenigKoenig, Jérémie Yale UniversityUnited States Unifying compositional verification and certified compilation with a three-dimensional refinement algebra
Jed Koh Jin KeatKoh Jin Keat, Jed National University of Singapore Property Testing Trace Languages Property Testing Trace Languages
Michalis KokologiannakisKokologiannakis, Michalis ETH ZurichSwitzerland Stateless Model Checking Concurrent and Distributed Programs RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency Model Checking C/C++ with Mixed-Size Accesses
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University and Southampton UniversityUnited Kingdom PC Member in Program Committee within the CPP-track Committee Member in Program Committee within the PADL-track
Joomy KorkutKorkut, Joomy Bloomberg LPUnited States Session Chair of Proof Assistants (part of POPL ) A Verified Foreign Function Interface Between Coq and C
Katherine KosaianKosaian, Katherine University of Iowa PC Member in Program Committee within the VMCAI-track
Natalia KosilovaKosilova, Natalia Oracle Labs Sandwood: Runtime Adaptable Probabilistic Programming for Java (Remote)
Eric KoskinenKoskinen, Eric Stevens Institute of TechnologyUnited States An Abstract Domain for Heap Commutativity Committee Member in Program Committee within the POPL -track
Daisuke KotaniKotani, Daisuke Kyoto University Wanco: WebAssembly AOT Compiler that supports Live Migration
András KovácsKovács, András University of Gothenburg and Chalmers University of Technology Eta conversion for the unit type (is still not that simple) Committee Member in Program Committee Members within the PEPM-track
Dexter KozenKozen, Dexter Cornell UniversityUnited States A Demonic Outcome Logic for Randomized Nondeterminism
Maite KramarzKramarz, Maite University of TorontoCanada M3: A Multi-Stage ML with Mutation
Nicolai KrausKraus, Nicolai University of NottinghamUnited Kingdom PC Member in Program Committee within the CPP-track
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands Affect: An Affine Type and Effect System Committee Member in Steering Committee within the CPP-track PC Member in Program Committee within the CPP-track
Jan KretinskyKretinsky, Jan Masaryk University, Czech RepublicGermany 1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization PC Member in Program Committee within the VMCAI-track
Shankaranarayanan KrishnaKrishna, Shankaranarayanan IIT Bombay, India PC Chair in Program Committee within the VMCAI-track Co-chair in Organizing Committee within the VMCAI-track
Niroop KrishnakumarKrishnakumar, Niroop UCSD Generic Refinement Types
Rahul KrishnanKrishnan, Rahul University of Wisconsin-MadisonUnited States Leveraging Duality for Programming with zkSNARKs
Neel KrishnaswamiKrishnaswami, Neel University of CambridgeUnited Kingdom Student Research Competition Co-Chair in Organizing Committee for POPL 2025 Session Chair of Theory (part of POPL ) Semantic Analysis of Normalisation for Directional Logic Programming Fulminate: Testing CN Separation-Logic Specifications in C Student Research Competition Chair in Selection Committee within the POPL Student Research Competition-track
Nikolai KudasovKudasov, Nikolai Innopolis UniversityRussia Towards Generic Higher-Order Unification Implementations in Haskell Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
Atticus KuhnKuhn, Atticus University of Cambridge Loop Invariants Using Neural Networks
Anika KumarKumar, Anika Rutgers University Sdim: A Qudit Stabilizer Simulator
Viktor KunčakKunčak, Viktor EPFL, SwitzerlandSwitzerland Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study PC Member in Program Committee within the VMCAI-track
Cole KurashigeKurashige, Cole UCSD Generic Refinement Types
Thi Ha KyawKyaw, Thi Ha LG Electronics Toronto AI Lab Restricted Evolution as a Strategy for Constant Runtime Error Mitigation
Robert KünnemannKünnemann, Robert CISPA Helmholtz Center for Information Security Universal Composability is Robust Compilation
L Shadaj LaddadLaddad, Shadaj University of California at BerkeleyUnited States Performant, Readable and Interoperable Rust from Dafny Flo: a Semantic Foundation for Progressive Stream Processing
Ambroise LafontLafont, Ambroise Ecole PolytechniqueFrance PC Member in Program Committee within the CPP-track
Ignacio LagunaLaguna, Ignacio Lawrence Livermore National LaboratoryUnited States Towards Verified Linear Algebra Programs Through Equivalence
Shuvendu K. LahiriLahiri, Shuvendu K. Microsoft ResearchUnited States Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Christopher LamLam, Christopher University of Illinois at Urbana-ChampaignUnited States Audio/Video Co-Chairs in Organizing Committee for POPL 2025 Committee Member in AV Committee for POPL 2025
Leonidas LampropoulosLampropoulos, Leonidas University of Maryland, College ParkGreece Session Chair of Fourth Session (part of PLMW @ POPL) Session Chair of First Session (part of PLMW @ POPL) Icebreaker Pantograph: A Fluid and Typed Structure Editor Formalizing Erlang’s Success Typings Committee Member in Program Committee within the POPL -track Organizer in Organizing Committee within the PLMW @ POPL-track
Adrienne LancelotLancelot, Adrienne Inria, LIX Ecole Polytechnique, IRIF Université Paris CitéFrance Interaction Equivalence
Ivan LaneseLanese, Ivan University of Bologna/INRIA Towards Quantum Multiparty Session Types Committee Member in Program Committee within the PADL-track
Vincent LaporteLaporte, Vincent Inria Preservation of Speculative Constant-time by Compilation Preservation of speculative constant-time by compilation PC Member in Program Committee within the CPP-track
Alberto LarrauriLarrauri, Alberto University of OxfordUnited Kingdom Synthesis of Controllers for Continuous Blackbox Systems
Per LarsenLarsen, Per University of California, Irvine Committee Member in Program Committee within the PriSC-track
Alan LawrenceLawrence, Alan Quantinuum HUGR: A Quantum-Classical Intermediate Representation Imperative Quantum Programming with Ownership and Borrowing in Guppy
Xuan-Bach D. LeLe, Xuan-Bach D. University of MelbourneAustralia Towards Mining Robust Coq Proof Patterns
Dongho LEELEE, Dongho Dalhousie UniversityCanada Committee Member in Program Committee within the PLanQC-track
Jaehyung LeeLee, Jaehyung Seoul National University Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
Sung-Hwan LeeLee, Sung-Hwan Seoul National UniversitySouth Korea VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
Woosuk LeeLee, Woosuk Hanyang UniversitySouth Korea Committee Member in Program Committee within the POPL -track
Nico LehmannLehmann, Nico UCSD Generic Refinement Types
K. Rustan M. LeinoLeino, K. Rustan M. AmazonUnited States Keynote Steering Committee Chair in Steering Committee Chairs within the Dafny-track
Roland LeißaLeißa, Roland University of Mannheim, School of Business Informatics and MathematicsGermany Session Chair of Program Analysis (part of POPL ) MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
Michael LeMayLeMay, Michael Committee Member in Program Committee within the PriSC-track
Ondřej LengálLengál, Ondřej Brno University of TechnologyCzechia An Automata-based Framework for Quantum Circuit Verification Verifying Quantum Circuits with Level-Synchronized Tree Automata
Tancrède LepointLepoint, Tancrède Amazon Web Services Verifying the Fisher-Yates Shuffle Algorithm in Dafny
Xavier LeroyLeroy, Xavier Collège de FranceFrance Associate Chair in Program Committee within the POPL -track
Mohsen LesaniLesani, Mohsen University of California at Santa Cruz TensorRight: Automated Verification of Tensor Graph Rewrites
Derek LeungLeung, Derek Massachusetts Institute of Technology, USA Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems
Michael LeuschelLeuschel, Michael HHUGermany Committee Member in Program Committee within the PADL-track
Alexander K. LewLew, Alexander K. Massachusetts Institute of TechnologyUnited States Session Chair of Synthesis and Compilation (part of POPL ) Lazy Knowledge Compilation for Discrete PPLs
Nicholas V. LewchenkoLewchenko, Nicholas V. University of Colorado BoulderUnited States Committee Member in Student Volunteers for POPL 2025
Robert Y. LewisLewis, Robert Y. Brown UniversityUnited States PC Member in Program Committee within the CPP-track
Cynthia LiLi, Cynthia Committee Member in Student Volunteers for POPL 2025
Fang LiLi, Fang Oklahoma Christian University Session Chair of Session 6 (part of PADL) Exploring Answer Set Programming for Provenance Graph-Based Cyber Threat Detection: A Novel Approach
Guoqiang LiLi, Guoqiang Shanghai Jiao Tong UniversityChina Affine Disjunctive Invariant Generation with Farkas’ Lemma
James LiLi, James Cornell University Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching
John LiLi, John Northeastern University Towards Symbolic Execution for Probability and Non-determinism
Junru LiLi, Junru Southeast University, NanjingChina A Weighted Bipolar Argumentation Framework and its ASP-based Implementation
Kwing Hei LiLi, Kwing Hei Aarhus UniversityDenmark Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Liyi LiLi, Liyi Iowa State UniversityUnited States The Quantum Abstract Machine Committee Member in Program Committee within the PLanQC-track
Qin LiLi, Qin Shanghai Key Laboratory of Trustworthy Computing, East China Normal UniversityChina Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training
Qing LiLi, Qing Department of Engineering, University of Cambridge State Space Model Programming in Turing.jl
Runming LiLi, Runming Carnegie Mellon University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Wu Angela LiLi, Wu Angela Rice University Verified and Efficient Matching of Regular Expressions with Lookaround
Yao LiLi, Yao Portland State UniversityUnited States Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the CoqPL-track
Yue Chen LiLi, Yue Chen Massachusetts Institute of Technology Dafny as Verification-Aware Intermediate Language for Code Generation
Yalun LiangLiang, Yalun Shanghai Jiao Tong University Experience Report: Stack Switching in Wasm SpecTec
Steven LibbyLibby, Steven The Scenic Route to Deforestation
Jack Liell-CockLiell-Cock, Jack University of Oxford Compositional imprecise probability: a solution from graded monads and Markov categories
Yuliya LierlerLierler, Yuliya University of Nebraska SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic
Jannis LimpergLimperg, Jannis University of Munich (LMU)Germany Tactic Script Optimisation for Aesop
Jyun-Ao LinLin, Jyun-Ao National Taipei University of TechnologyTaiwan An Automata-based Framework for Quantum Circuit Verification Verifying Quantum Circuits with Level-Synchronized Tree Automata
Yun LinLin, Yun Shanghai Jiao Tong UniversityChina Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
Sam LindleyLindley, Sam The University of EdinburghUnited Kingdom Session Chair of High-level abstraction and automation (part of PEPM) Experience Report: Stack Switching in Wasm SpecTec Semantics-based program manipulation in the age of LLMs Committee Member in Program Committee Members within the PEPM-track
Marian Lingsch-RosenfeldLingsch-Rosenfeld, Marian LMU Munich Committee Member in Artifact Evaluation Committee within the VMCAI-track
Kirby LinvillLinvill, Kirby University of Colorado BoulderUnited States Committee Member in Student Volunteers for POPL 2025
Benny Zong LiuLiu, Benny Zong Imperial College London QuteFuzz: Fuzzing quantum compilers using randomly generated circuits with control flow and subcircuits
Cyrus LiuLiu, Cyrus Samsung SemiconductorUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Fangzhou LiuLiu, Fangzhou Southeast University, NanjingChina A Weighted Bipolar Argumentation Framework and its ASP-based Implementation
Hongming LiuLiu, Hongming Shanghai Jiao Tong UniversityChina Affine Disjunctive Invariant Generation with Farkas’ Lemma
Jing LiuLiu, Jing UC Irvine; MPI-SP Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Puzhuo LiuLiu, Puzhuo Tsinghua UniversityChina Automated Flaw Detection for Industrial Robot RESTful Service
Si LiuLiu, Si ETH ZurichSwitzerland Reachability Analysis of the Domain Name System
Y. Annie LiuLiu, Y. Annie Stony Brook UniversityUnited States Session Chair of Macros, lenses, and LLMs (part of PEPM) Welcome Farewell Invited Talk: Solvers, unite! A simple unified semantics for reasoning with assurance and agreement Co-chair in Chairs within the PEPM-track
Yang LiuLiu, Yang Nanyang Technological UniversitySingapore Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
Yiyun LiuLiu, Yiyun University of Pennsylvania Consistency of a Dependent Calculus of Indistinguishability
Fang-Yi LoLo, Fang-Yi Academia Sinica Committee Member in Student Volunteers for POPL 2025 An Automata-based Framework for Quantum Circuit Verification Verifying Quantum Circuits with Level-Synchronized Tree Automata
Hunter LockwoodLockwood, Hunter Myaamia Center & Miami University ASP for Language Documentation and Reclamation: A Derivational Stemming Tool for Myaamia
Chloe LoughridgeLoughridge, Chloe Harvard University DafnyBench: A Benchmark for Formal Software Verification dafny-annotator: AI-Assisted Verification of Dafny Programs VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Sirui LuLu, Sirui University of WashingtonUnited States TensorRight: Automated Verification of Tensor Graph Rewrites
Xiaokun LuanLuan, Xiaokun Peking University Generically Automating Separation Logic by Functors, Homomorphisms, and Modules Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
Brandon LuciaLucia, Brandon Carnegie Mellon University, USA An MLIR Dialect for WebAssembly
Joseph LundervilleLunderville, Joseph Simon Fraser University Linear and non-linear relational analyses for Quantum Program Optimization
Zhengxiong LuoLuo, Zhengxiong National University of SingaporeChina Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Matthew LutzeLutze, Matthew Aarhus University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Owen LynchLynch, Owen University of Oxford Data-oriented Design for Differentiable, Probabilistic Programming (Remote)
Andreas LööwLööw, Andreas Imperial College London Data Structure Abstraction and Incorrectness Separation Logic
M Frederik M. W. HyldgaardM. W. Hyldgaard, Frederik Aalborg UniversityDenmark ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks
Dougal MaclaurinMaclaurin, Dougal Committee Member in Steering Committee within the LAFI-track
Benedikt MaderbacherMaderbacher, Benedikt Graz University of TechnologyAustria Synthesis of Controllers for Continuous Blackbox Systems
Fabio MadgeMadge, Fabio Automated Reasoning Group, Amazon Web Services Performant, Readable and Interoperable Rust from Dafny
P. MadhusudanMadhusudan, P. University of Illinois at Urbana-ChampaignUnited States Committee Member in Program Committee within the POPL -track
Kenji MaillardMaillard, Kenji InriaFrance All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
Rupak MajumdarMajumdar, Rupak MPI-SWSGermany Sound and Complete Proof Rules for Probabilistic Termination
Ekaterina MaksimovaMaksimova, Ekaterina Innopolis University Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
Dhruv MakwanaMakwana, Dhruv University of CambridgeUnited Kingdom Fulminate: Testing CN Separation-Logic Specifications in C
Gregory MalechaMalecha, Gregory BedRock SystemsUnited States Committee Member in Program Committee within the CoqPL-track
Kaushik MallikMallik, Kaushik IST Austria, AustriaAustria Committee Member in Program Committee within the VMCAI-track
Konstantinos MamourasMamouras, Konstantinos Rice UniversityUnited States Verified and Efficient Matching of Regular Expressions with Lookaround Author in Selection Committee within the POPL Student Research Competition-track
Louis MandelMandel, Louis IBM Research, USA Inference Plans for Hybrid Particle Filtering
Ravi MangalMangal, Ravi Colorado State UniversityUnited States Committee Member in Program Committee within the VMCAI-track
Vikash K. MansinghkaMansinghka, Vikash K. Massachusetts Institute of TechnologyUnited States Lazy Knowledge Compilation for Discrete PPLs
William ManskyMansky, William University of Illinois ChicagoUnited States PC Member in Program Committee within the CPP-track
Rida Ait El ManssourManssour, Rida Ait El CNRS & IRIF, Paris Simple Linear Loops: Algebraic Invariants and Applications
Giulio ManzonettoManzonetto, Giulio Université Paris Cité Interaction Equivalence
Francesco Pio MarinoMarino, Francesco Pio University of Catania, University of Rouen Qutes: a Pathway to High-Level Quantum Programming
Darko MarinovMarinov, Darko University of Illinois at Urbana-ChampaignUnited States Committee Member in Program Committee within the POPL -track
Julio MariñoMariño, Julio Universidad Politécnica de MadridSpain Checking Concurrency Coding Rules Haskell Based Spreadsheets Logic Programming with Extensible Types (Lightning talk)
Iason MarmanisMarmanis, Iason MPI-SWSGermany Model Checking C/C++ with Mixed-Size Accesses
Danielle MarshallMarshall, Danielle University of GlasgowUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Chris MartensMartens, Chris Northeastern UniversityUnited States A Complete Translation from Planning Problems to linear logic Finite-Choice Logic Programming
Patrick MassotMassot, Patrick Université Paris-SaclayFrance PC Member in Program Committee within the CPP-track
Isabella MastroeniMastroeni, Isabella University of VeronaItaly Session Chair of Verification (part of VMCAI) Abstract Local Completeness: A Local form of Abstract Non-Interference A Static Analysis of Entanglement Adversities in Abstract Interpretation - Accommodating Robustness by Abstract Interpretation
Christoph MathejaMatheja, Christoph DTUDenmark Workshops Co-Chair in Organizing Committee for POPL 2025
Umang MathurMathur, Umang National University of SingaporeSingapore Session Chair of Concurrency 2 (part of POPL ) The Decision Problem for Regular First Order Theories
Yusuke MatsushitaMatsushita, Yusuke Kyoto University Concurrent Quantum Separation Logic for Fine-Grained Parallelism Concurrent Quantum Separation Logic for Fine-Grained Parallelism
Mikael MayerMayer, Mikael Automated Reasoning Group, Amazon Web Services Performant, Readable and Interoperable Rust from Dafny Verifying the Fisher-Yates Shuffle Algorithm in Dafny
Micaela MayeroMayero, Micaela LIPN, Université Paris 13France PC Member in Program Committee within the CPP-track
Ian McCormackMcCormack, Ian Carnegie Mellon UniversityUnited States Gradual C0: Symbolic Execution for Gradual Verification
James McKinnaMcKinna, James Heriot-Watt UniversityUnited Kingdom Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
Sean McLaughlinMcLaughlin, Sean Amazon Web Services Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
Wolfgang MeierMeier, Wolfgang Aarhus University CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
Innokentii MeleshchenkoMeleshchenko, Innokentii JetBrains Research, Neapolis University Pafos, Cyprus Relaxed Memory Concurrency Re-executed
Orestis MelkonianMelkonian, Orestis Input Output Global (IOG/IOHK)United Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Stephen MellMell, Stephen Student Volunteer Co-Chair in Organizing Committee for POPL 2025
Matteo MeluzziMeluzzi, Matteo TU Delft, the Netherlands Relaxed Memory Concurrency Re-executed
Kayvan MemarianMemarian, Kayvan University of Cambridge A CHERI C Memory Model for Verified Temporal Safety Fulminate: Testing CN Separation-Logic Specifications in C
Charith MendisMendis, Charith University of Illinois at Urbana-ChampaignUnited States TensorRight: Automated Verification of Tensor Graph Rewrites
Lucy MenonMenon, Lucy Microsoft The WebAssembly Component Model
Eric MercerMercer, Eric Brigham Young UniversityUnited States Property-agnostic base case extension for scalable verification of distributed systems Committee Member in Program Committee within the VMCAI-track
Gabriele MessinaMessina, Gabriele University of Catania Qutes: a Pathway to High-Level Quantum Programming
David MestelMestel, David Maastricht University The Decision Problem for Regular First Order Theories
Joachim MeyerMeyer, Joachim Saarland University, Saarland Informatics CampusGermany MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
Roland MeyerMeyer, Roland TU BraunschweigGermany SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the VMCAI-track
Aart MiddeldorpMiddeldorp, Aart University of Innsbruck Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Mae MilanoMilano, Mae Princeton UniversityUnited States Session Chair of Types 2 (part of POPL ) Flo: a Semantic Foundation for Progressive Stream Processing
Dale MillerMiller, Dale INRIA Saclay and LIX/Institut Polytechnique de ParisFrance Committee Member in Steering Committee within the CPP-track
Yasuhiko MinamideMinamide, Yasuhiko Tokyo Institute of TechnologyJapan Session Chair of Session 3 (part of CPP) Formalization of Differential Privacy in Isabelle/HOL Further Tackling Post Correspondence Problem and Proof Generation PC Member in Program Committee within the CPP-track
Mikhail MintsMints, Mikhail California Institute of Technology Compiling Qunity: From High-Level Quantum Programs to Circuits
Antoine MinéMiné, Antoine Sorbonne UniversitéFrance PC Member in Program Committee within the VMCAI-track
Md Rakib Hossain MisuMisu, Md Rakib Hossain University of California IrvineUnited States DafnyBench: A Benchmark for Formal Software Verification
Alistair MoffatMoffat, Alistair The University of Melbourne Formalized Burrows-Wheeler Transform
Torben MogensenMogensen, Torben DIKU, University of CopenhagenDenmark Committee Member in Program Committee Members within the PEPM-track
Mohammadsadegh MohagheghiMohagheghi, Mohammadsadegh Masaryk UniversityCzechia 1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Stefanie MohrMohr, Stefanie Technical University of MunichGermany 1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Alexandre MoineMoine, Alexandre New York UniversityUnited States PLMW Panel
Evgenii MoiseenkoMoiseenko, Evgenii JetBrains Research Relaxed Memory Concurrency Re-executed
Alberto MomiglianoMomigliano, Alberto Università degli Studi di Milano Split Decisions: Explicit Contexts for Substructural Languages
Luca MondadaMondada, Luca University of OxfordUnited Kingdom HUGR: A Quantum-Classical Intermediate Representation
David MonniauxMonniaux, David CNRSFrance Formally verified hardening of C programs against hardware fault injection Committee Member in Program Committee within the POPL -track
J. Garrett MorrisMorris, J. Garrett University of IowaUnited States Committee Member in Program Committee within the POPL -track
Andreas Tor MortensenMortensen, Andreas Tor Department of Computer Science, Aalborg University A Type Safe Calculus for Generating Syntax-Directed Editors
Eliot MossMoss, Eliot University of Massachusetts at AmherstUnited States A Transactions Extension for Web Assembly
Sergio MoverMover, Sergio École PolytechniqueFrance PC Member in Program Committee within the VMCAI-track
Anish MudideMudide, Anish Massachusetts Institute of Technology DafnyBench: A Benchmark for Formal Software Verification
Gautam MudugantiMuduganti, Gautam Indian Institute of Technology Hyderabad, IndiaIndia LLOR: Automated Repair of OpenMP Programs
Eric MugnierMugnier, Eric University of California San Diego Laurel: Unblocking Automated Verification with Large Language Models
Prasita MukherjeeMukherjee, Prasita Committee Member in Student Volunteers for POPL 2025 Towards Automated Verification of LLM-Synthesized C Programs
Liam MulcahyMulcahy, Liam University of Michigan Incremental Bidirectional Typing via Order Maintenance
Cesar MunozMunoz, Cesar NASAUnited States PC Member in Program Committee within the CPP-track
Andrzej MurawskiMurawski, Andrzej University of OxfordUnited Kingdom Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
Koko MuroyaMuroya, Koko NIIJapan PC Member in Program Committee within the VMCAI-track
Karthik Srinivasa MurthyMurthy, Karthik Srinivasa Google TensorRight: Automated Verification of Tensor Graph Rewrites
Andrew MyersMyers, Andrew Cornell University A Research Career in Balance Author in Steering Committee within the PriSC-track
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology Baking for Dafny: A CakeML Backend for Dafny Committee Member in Program Committee within the POPL -track
Rasmus Ejlers MøgelbergMøgelberg, Rasmus Ejlers IT University of CopenhagenDenmark Modelling Recursion and Probabilistic Choice in Guarded Type Theory
Niklas MückMück, Niklas MPI-SWSGermany A Semantic Approach to Robust Property Preservation
Peter MüllerMüller, Peter ETH ZurichSwitzerland Formal Foundations for Translational Separation Logic Verifiers Viper: An Infrastructure for Automated Verification in Separation Logic
N Chandra Kanth NageshNagesh, Chandra Kanth University of Colorado BoulderUnited States Committee Member in Student Volunteers for POPL 2025
Keisuke NakanoNakano, Keisuke Tohoku UniversityJapan Characterizations of Partial Well-Behaved Lenses
Hitomi NakayamaNakayama, Hitomi Committee Member in Student Volunteers for POPL 2025
Kedar NamjoshiNamjoshi, Kedar Nokia Bell LabsUnited States Session Chair of Abstract Interpretation # 1 (part of VMCAI) Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications Constructing Trustworthy Smart Contracts
Chandrakana NandiNandi, Chandrakana CertoraUnited States Committee Member in Program Committee within the WITS-track
Praveen NarayananNarayanan, Praveen Google TensorRight: Automated Verification of Tensor Graph Rewrites
Louis NarmourNarmour, Louis Colorado State University, University of Rennes, Inria, CNRS, IRISAUnited States Session Chair of Probabilistic Programming 1 (part of POPL ) Maximal Simplification of Polyhedral Reductions
David E. NarváezNarváez, David E. Virginia Tech CF-GKAT: Efficient Validation of Control-Flow Transformations
Nico NausNaus, Nico Open University of The Netherlands & Virginia Tech CF-GKAT: Efficient Validation of Control-Flow Transformations
Jorge A. NavasNavas, Jorge A. CertoraUnited States Automatic Inference of Relational Object Invariants
Hamed NematiNemati, Hamed KTH Royal Institute of TechnologySweden Committee Member in Program Committee within the PriSC-track
Dhruv NevatiaNevatia, Dhruv ETH Zurich Reachability Analysis of the Domain Name System
Max S. NewNew, Max S. University of MichiganUnited States Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
Jim NewtonNewton, Jim EPITA / LRE https://www.lre.epita.frFrance Type-Checking Heterogeneous Sequences in a Simple Embeddable Type System
Daniel NezamabadiNezamabadi, Daniel Chalmers University of Technology and University of GothenburgSwitzerland Baking for Dafny: A CakeML Backend for Dafny
Dan NguyenNguyen, Dan University of Texas at Dallas, USA Automated Playing of Survival Video Games with Commonsense Reasoning (short paper)
Steven NguyenNguyen, Steven Rutgers University Sdim: A Qudit Stabilizer Simulator
Tobias NipkowNipkow, Tobias Technische Universität München Committee Member in Steering Committee within the CPP-track
Naoki NishidaNishida, Naoki Nagoya UniversityJapan Committee Member in Program Committee within the PADL-track
Andreas NuytsNuyts, Andreas KU Leuven, BelgiumBelgium BiSikkel: A Multimode Logical Framework in Agda
Wesley B NuzzoNuzzo, Wesley B University of Massachusetts, Lowell (UML) Automatic Inference of Enclave Placement in LLVM Compiler
O Peter O'HearnO'Hearn, Peter University College London, UK and Lacework, London, UK Committee Member in Program Committee within the TPSA-track
Hakjoo OhOh, Hakjoo Korea UniversitySouth Korea Committee Member in Program Committee within the POPL -track
Yasuo OkabeOkabe, Yasuo Kyoto University Wanco: WebAssembly AOT Compiler that supports Live Migration
Ana Oliveira Da CostaOliveira Da Costa, Ana IST Austria, AustriaAustria Committee Member in Program Committee within the VMCAI-track
Bruno C. d. S. OliveiraOliveira, Bruno C. d. S. University of Hong KongChina QuickSub: Efficient Iso-Recursive Subtyping Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
Tiago OliveiraOliveira, Tiago SandboxAQ Leakage-Free Probabilistic Jasmin Programs
Santiago Arranz OlmosOlmos, Santiago Arranz Max Planck Institute for Security and Privacy Preservation of Speculative Constant-time by Compilation Preservation of speculative constant-time by compilation
Cyrus OmarOmar, Cyrus University of MichiganUnited States Incremental Bidirectional Typing via Order Maintenance Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus Committee Member in Program Committee within the POPL -track
Akihiro OmoriOmori, Akihiro Department of Mathematical and Computing Science, Tokyo Institute of Technology Further Tackling Post Correspondence Problem and Proof Generation
C.-H. Luke OngOng, C.-H. Luke NTU NP-NUTS: A Nonparametric No-U-Turn Sampler Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
P Martin P. HansenP. Hansen, Martin Aalborg UniversityDenmark ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks
Oded PadonPadon, Oded Weizmann Institute of ScienceIsrael Verification of Distributed Protocols: Decidable Modeling and Invariant Inference A Primal-Dual Perspective on Program Verification Algorithms
Abhinandan PalPal, Abhinandan University of BirminghamUnited Kingdom Loop Invariants Using Neural Networks
Karl PalmskogPalmskog, Karl KTH Royal Institute of TechnologySweden PC Member in Program Committee within the CPP-track
Jens PalsbergPalsberg, Jens University of California, Los Angeles (UCLA)United States Session Chair of Quantum Computing 2 (part of POPL ) Welcome to Quantum 3.0! Committee Member in Program Committee within the POPL -track Committee Member in Program Committee Members within the PEPM-track
Zhiwen PanPan, Zhiwen Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, ChinaChina Automated Flaw Detection for Industrial Robot RESTful Service
Pavel PanchekhaPanchekha, Pavel University of UtahUnited States Incremental Bidirectional Typing via Order Maintenance Committee Member in Program Committee within the POPL -track
Hugo PaquetPaquet, Hugo École Normale Supérieure, PSL University & INRIAFrance Committee Member in Program Committee within the LAFI-track
Udaya ParampalliParampalli, Udaya Formal Verification of Quantum Stabilizer Code
Alberto PardoPardo, Alberto Universidad de la Republica, Uruguay Committee Member in Program Committee within the PADL-track
Manasvi ParikhParikh, Manasvi Committee Member in Student Volunteers for POPL 2025
Matthew J. ParkinsonParkinson, Matthew J. Microsoft Azure ResearchUnited Kingdom Committee Member in Program Committee within the POPL -track
Bryan ParnoParno, Bryan Carnegie Mellon UniversityUnited States Keynote: Bringing Verified Cryptographic Protocols to Practice Teaching Types and Non-Interference in Dafny Towards Proof Stability in SMT-based Program Verification PC Member in Program Committee within the Dafny-track
Gaurav ParthasarathyParthasarathy, Gaurav ETH ZurichSwitzerland Formal Foundations for Translational Separation Logic Verifiers
Adam PaszkePaszke, Adam Google DeepMindGermany Committee Member in Program Committee within the LAFI-track
Marco PatrignaniPatrignani, Marco University of TrentoItaly Opening Remarks Closing Remarks Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks Universal Composability is Robust Compilation Co-chair in Program Committee within the PriSC-track Author in Steering Committee within the PriSC-track
Andreas PavlogiannisPavlogiannis, Andreas Aarhus UniversityDenmark Session Chair of Concurrency (part of POPL ) Program Analysis via Multiple Context Free Language Reachability PC Member in Program Committee within the VMCAI-track
Angel Pavlov AngelovPavlov Angelov, Angel Sofia UniversityBulgaria Committee Member in AV Committee for POPL 2025
Jennifer PaykinPaykin, Jennifer IntelUnited States Session Chair of Session 2 (part of CPP) Session Chair of Session 1 (part of PLanQC) Programming with Projective Cliffords PC Member in Program Committee within the CPP-track Program Chair in Program Committee within the PLanQC-track Chair in Organizing Committee within the PLanQC-track
Barak A. PearlmutterPearlmutter, Barak A. Maynooth UniversityIreland Committee Member in Program Committee within the LAFI-track
Elia PerantoniPerantoni, Elia Adversities in Abstract Interpretation - Accommodating Robustness by Abstract Interpretation
Mário PereiraPereira, Mário NOVA LINCS & DI -- Nova School of Science and TechnologyPortugal Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ivan PerezPerez, Ivan NASA Ames Research Center Logic Programming with Extensible Types (Lightning talk)
Basile PesinPesin, Basile Ecole Nationale de l'Aviation Civile (ENAC) Formally verified hardening of C programs against hardware fault injection
Benjamin PetersPeters, Benjamin MPI-SWS Data Race Freedom à la Mode
Annabell PetriPetri, Annabell Universiteit Twente Committee Member in Artifact Evaluation Committee within the VMCAI-track
Loïc PeyrotPeyrot, Loïc IMDEA Software Institute Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Frank PfenningPfenning, Frank Carnegie Mellon University, USA Substructural Type Systems Committee Member in Program Committee within the POPL -track
Katherine PhilipPhilip, Katherine Portland State University Committee Member in Student Volunteers for POPL 2025 Formalizing Representation Transformations: A Case Study of Bit Vector Types
Phitchaya Mangpo PhothilimthanaPhothilimthana, Phitchaya Mangpo Google TensorRight: Automated Verification of Tensor Graph Rewrites
David PichardiePichardie, David MetaFrance Enhancing Infer Compositional Analysis with Summary Specialization
Jean Pichon-PharabodPichon-Pharabod, Jean Aarhus UniversityDenmark CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
Lauren PickPick, Lauren UC Berkeley and UW-Madison Committee Member in Program Committee within the POPL -track
Brigitte PientkaPientka, Brigitte McGill UniversityCanada Session Chair of Session 4 (part of CPP) McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract) Semantics-based program manipulation in the age of LLMs Split Decisions: Explicit Contexts for Substructural Languages A Dependent Type Theory for Meta-programming with Intensional Analysis Committee Member in Steering Committee within the CPP-track
Frank PiessensPiessens, Frank KU Leuven Author in Steering Committee within the PriSC-track
Jared PincusPincus, Jared Boston UniversityUnited States Committee Member in Student Volunteers for POPL 2025 An Abstract Domain for Heap Commutativity
Ruzica PiskacPiskac, Ruzica Yale UniversityUnited States Associate Chair in Program Committee within the POPL -track
Michael PiskozubPiskozub, Michael University at Buffalo, SUNY Committee Member in Student Volunteers for POPL 2025
Clément Pit-ClaudelPit-Claudel, Clément EPFLSwitzerland Committee Member in Program Committee within the POPL -track PC Member in Program Committee within the CPP-track PC Member in Program Committee within the Dafny-track
Ryan PitaskyPitasky, Ryan Committee Member in Student Volunteers for POPL 2025
Adam PocockPocock, Adam Oracle LabsUnited States Sandwood: Runtime Adaptable Probabilistic Programming for Java (Remote)
Andreas PodelskiPodelski, Andreas University of FreiburgGermany PC Member in Program Committee within the VMCAI-track
Anton PodkopaevPodkopaev, Anton JetBrains Research, Constructor UniversityNetherlands Relaxed Memory Concurrency Re-executed
Gabriel PoesiaPoesia, Gabriel Stanford University dafny-annotator: AI-Assisted Verification of Dafny Programs
Josselin PoiretPoiret, Josselin Nantes Université, Inria All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
Piotr PolesiukPolesiuk, Piotr University of Wrocław Committee Member in Program Committee within the CoqPL-track
Nadia PolikarpovaPolikarpova, Nadia University of California at San DiegoUnited States Laurel: Unblocking Automated Verification with Large Language Models Associate Chair in Program Committee within the POPL -track
Enrico PontelliPontelli, Enrico New Mexico State UniversityUnited States Committee Member in Program Committee within the PADL-track
Francesco PontiggiaPontiggia, Francesco TU Wien Exact Inference for Nested Discrete Probabilistic Programs (Remote)
Andrei PopescuPopescu, Andrei University of SheffieldUnited Kingdom Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
Caspar PopovaPopova, Caspar University of Maryland College ParkUnited States Committee Member in Student Volunteers for POPL 2025
Thomas J. PorterPorter, Thomas J. University of MichiganUnited States Incremental Bidirectional Typing via Order Maintenance Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
Marie-Laure PotetPotet, Marie-Laure Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG Formally verified hardening of C programs against hardware fault injection
François PottierPottier, François InriaFrance Tail Modulo Cons, OCaml, and Relational Separation Logic Data Race Freedom à la Mode
Damien PousPous, Damien CNRS PC Member in Program Committee within the CPP-track
Boldizsár PoórPoór, Boldizsár Quantinuum Fusion and flow: formal protocols to reliably build photonic graph states
Vinayak PrabhuPrabhu, Vinayak Colorado State UniversityUnited States PC Member in Program Committee within the VMCAI-track
Prasanth PrahladanPrahladan, Prasanth University of Colorado Boulder Distributed transactions over mergeable types: A meta-theory for 5G control-plane protocol verification
Tarun PrasadPrasad, Tarun Harvard VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Jacob PrinzPrinz, Jacob University of Maryland, College Park Pantograph: A Fluid and Typed Structure Editor
Swarn PriyaPriya, Swarn Virginia TechUnited States BeePL: Correct-by-compilation kernel extensions Committee Member in Program Committee within the PriSC-track
Jonathan ProtzenkoProtzenko, Jonathan Microsoft Azure ResearchUnited States PC Member in Program Committee within the CPP-track Author in Steering Committee within the PriSC-track
Christopher PultePulte, Christopher University of CambridgeUnited Kingdom Fulminate: Testing CN Separation-Logic Specifications in C
Edoardo PuttiPutti, Edoardo University of Twente Committee Member in Artifact Evaluation Committee within the VMCAI-track
Pierre-Marie PédrotPédrot, Pierre-Marie INRIAFrance All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
Thibaut PéramiPérami, Thibaut University of Cambridge Towards general white-box automation: a typeclass-guided context cleaner
Q Shaz QadeerQadeer, Shaz Meta, Inc.United States Committee Member in Program Committee within the POPL -track
Weihao QuQu, Weihao Monmouth UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
R Azalea RaadRaad, Azalea Imperial College LondonUnited Kingdom Introduction U-turn: Forward-driven backward analysis for incorrectness Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation Committee Member in Organizing Committee within the TPSA-track Committee Member in Program Committee within the TPSA-track
Gabriel RadanneRadanne, Gabriel InriaFrance Avoiding signature avoidance in ML modules with zippers
Stefan RadziukRadziuk, Stefan Imperial College LondonUnited Kingdom Progressful Interpreters for Efficient WebAssembly Mechanisation
Jonathan Ragan-KelleyRagan-Kelley, Jonathan Massachusetts Institute of TechnologyUnited States A Domain-Specific PPL for Reasoning about Reasoning (or: a memo on memo)
Mukund RaghothamanRaghothaman, Mukund University of Southern CaliforniaUnited States Committee Member in Program Committee within the POPL -track
Sibi RajaRaja, Sibi Harvard VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Vineet RajaniRajani, Vineet University of Kent Committee Member in Program Committee within the PriSC-track
Sanjay RajopadhyeRajopadhye, Sanjay Colorado State University Maximal Simplification of Polyhedral Reductions
Tahina RamananandroRamananandro, Tahina Microsoft ResearchUnited States Committee Member in Program Committee within the POPL -track
Jan-Paul Ramos-DavilaRamos-Davila, Jan-Paul Cornell UniversityUnited States Audio/Video Co-Chairs in Organizing Committee for POPL 2025 Committee Member in AV Committee for POPL 2025 Formal Verification of a Software Defined Delay-Tolerant Network Gradual C0: Symbolic Execution for Gradual Verification
Robert RandRand, Robert University of ChicagoUnited States Workshops Co-Chair in Organizing Committee for POPL 2025 Session Chair of Session 4 (part of PLanQC) Compiling Qunity: From High-Level Quantum Programs to Circuits Organizing Committee in Organizing Committee within the PLanQC-track
Francesco RanzatoRanzato, Francesco University of PadovaItaly The Best of Abstract Interpretations
Sanil RaoRao, Sanil Carnegie Mellon University Towards Semantics Lifting for Scientific Computing: A Case Study on FFT
Xiaojia RaoRao, Xiaojia Imperial College LondonUnited Kingdom Progressful Interpreters for Efficient WebAssembly Mechanisation
Shravan Ravi NarayanRavi Narayan, Shravan Adventures in Making Wasm Fast and More Secure
Binoy RavindranRavindran, Binoy Virginia TechUnited States On Extending Incorrectness Logic with Backwards Reasoning
Baber RehmanRehman, Baber University of Hong KongHong Kong SAR China Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Hamza RemmalRemmal, Hamza EPFL, LAMPSwitzerland Value semantics in reference-based languages
Mathys RennelaRennela, Mathys WelinqFrance Organizing Committee in Organizing Committee within the PLanQC-track
Tamara RezkRezk, Tamara INRIAFrance Committee Member in Program Committee within the PriSC-track
Emily RiehlRiehl, Emily Johns Hopkins University Prospects for Computer Formalization of Infinite-Dimensional Category Theory
Mitchell RileyRiley, Mitchell Committee Member in Program Committee within the PLanQC-track
Martin RinardRinard, Martin MIT Committee Member in Program Committee Members within the PEPM-track
Xavier RivalRival, Xavier Inria; ENS; CNRS; PSL UniversityFrance Committee Member in Program Committee within the POPL -track PC Member in Program Committee within the VMCAI-track
Christine RizkallahRizkallah, Christine University of MelbourneAustralia Formal Verification of Quantum Stabilizer Code Towards Mining Robust Coq Proof Patterns Formalized Burrows-Wheeler Transform
Vincent RobinsonRobinson, Vincent University of Portland The Scenic Route to Deforestation
Adam RogalewiczRogalewicz, Adam Brno University of Technology, CzechiaCzechia Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)
Tiark RompfRompf, Tiark Purdue UniversityUnited States Committee Member in Program Committee Members within the PEPM-track
Julian RosemannRosemann, Julian Saarland University, Saarland Informatics CampusGermany Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
Neil Julien RossRoss, Neil Julien Dalhousie UniversityCanada Verifying the Equivalence of Parameterized Quantum Circuits Proto-Quipper with Reversing and Control Committee Member in Program Committee within the PLanQC-track
Nikolaj Rossander KristensenRossander Kristensen, Nikolaj Department of Computer Science, Aalborg University A Type Safe Calculus for Generating Syntax-Directed Editors
Andreas RossbergRossberg, Andreas IndependentGermany Experience Report: Stack Switching in Wasm SpecTec Committee Member in Program Committee within the WAW-track
Jurriaan RotRot, Jurriaan Radboud University Nijmegen Intrinsically Correct Sorting in Cubical Agda
Craig RoyRoy, Craig Quantinuum HUGR: A Quantum-Classical Intermediate Representation Imperative Quantum Programming with Ownership and Borrowing in Guppy
Grigore RoşuRoşu, Grigore University of Illinois at Urbana-ChampaignUnited States Committee Member in Program Committee within the POPL -track
Fabian RuchRuch, Fabian UnaffiliatedSweden Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Matthew RuizRuiz, Matthew Committee Member in Student Volunteers for POPL 2025
Neea RuschRusch, Neea Augusta UniversityUnited States Committee Member in Student Volunteers for POPL 2025 Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Didier RémyRémy, Didier Inria Avoiding signature avoidance in ML modules with zippers
Wojciech RóżowskiRóżowski, Wojciech University College LondonUnited Kingdom Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
Philipp RümmerRümmer, Philipp University of Regensburg and Uppsala University PC Member in Program Committee within the VMCAI-track
S Gustav S. BruhnsS. Bruhns, Gustav Aalborg UniversityDenmark ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks
Feras SaadSaad, Feras Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the POPL -track
Simmo SaanSaan, Simmo University of Tartu, EstoniaEstonia Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
Amit SabneSabne, Amit Google TensorRight: Automated Verification of Tensor Graph Rewrites
Orkunt SabuncuSabuncu, Orkunt TED UniversityTurkey Committee Member in Program Committee within the PADL-track
Teppei SaitoSaito, Teppei Japan Advanced Institute of Science and Technology, Japan An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
Elmer SalazarSalazar, Elmer The University of Texas at DallasUnited States C3G: Causally Constrained Counterfactual Generation
Guido SalvaneschiSalvaneschi, Guido University of St. GallenSwitzerland Session Chair of Syntax and Editing (part of POPL ) Dis/Equality Graphs
Malavika SamakSamak, Malavika Apple IncUnited States Committee Member in Program Committee within the PriSC-track
Michael SammlerSammler, Michael Institute of Science and Technology AustriaAustria A Semantic Approach to Robust Property Preservation Program logics à la carte Formal Foundations for Translational Separation Logic Verifiers Committee Member in Program Committee within the PriSC-track
David SananSanan, David Singapore Institute of Technology Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
David SananSanan, David Nanyang Technological University, SingaporeSingapore Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
Sriram SankaranarayananSankaranarayanan, Sriram University of Colorado, BoulderUnited States Session Chair of Keynote Talk and Cyber-Physical Systems (part of VMCAI) Session Chair of Concurrency (part of VMCAI) PC Chair in Program Committee within the VMCAI-track Co-chair in Organizing Committee within the VMCAI-track
Chuta SanoSano, Chuta McGill UniversityCanada Split Decisions: Explicit Contexts for Substructural Languages
Vitor Santos CostaSantos Costa, Vitor University of Porto, Portugal Session Chair of Session 4 (part of PADL) On Bridging Prolog and Python to Enhance an Inductive Logic Programming System
João SaraivaSaraiva, João Committee Member in Program Committee Members within the PEPM-track
Zeynep G. SaribaturSaribatur, Zeynep G. TU WienAustria Committee Member in Program Committee within the PADL-track
John SarracinoSarracino, John Lawrence Livermore National Laboratory Towards Verified Linear Algebra Programs Through Equivalence
V.R. SathiyanarayanaSathiyanarayana, V.R. MPI-SWS Sound and Complete Proof Rules for Probabilistic Termination
Sundara Vishnu SatishSatish, Sundara Vishnu University of Michigan - Ann ArborUnited States Committee Member in Student Volunteers for POPL 2025 Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
Tetsuya SatoSato, Tetsuya Tokyo Institute of TechnologyJapan Formalization of Differential Privacy in Isabelle/HOL
Gaurav SaxenaSaxena, Gaurav LG Electronics Toronto AI Lab Restricted Evolution as a Strategy for Constant Runtime Error Mitigation
Gabriel SchererScherer, Gabriel Université Paris Cité - Inria - CNRSFrance Tail Modulo Cons, OCaml, and Relational Separation Logic Committee Member in Program Committee within the WITS-track
Sven ScheweSchewe, Sven University of Liverpool PC Member in Program Committee within the VMCAI-track
Matthias SchlaipferSchlaipfer, Matthias Amazon Helping users to reduce Brittleness in their Dafny programs - a success story
Filip SchramkaSchramka, Filip Ateleris GmbHSwitzerland Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
Tom SchrijversSchrijvers, Tom KU LeuvenBelgium Biparsers: Exact Printing for Data Synchronisation Committee Member in Program Committee within the PADL-track
Michael SchwarzSchwarz, Michael TU MunichGermany Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
Frank SchüsseleSchüssele, Frank University of FreiburgGermany Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
Mircea SebeSebe, Mircea UIUCUnited States Nominal Matching Logic With Fixpoints
Md Syadus SefatSefat, Md Syadus Virginia TechUnited States On Extending Incorrectness Logic with Backwards Reasoning
Helmut SeidlSeidl, Helmut TU MunichGermany Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
Taro SekiyamaSekiyama, Taro National Institute of Informatics; SOKENDAIJapan Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs
Peter SelingerSelinger, Peter Dalhousie UniversityCanada Proto-Quipper with Reversing and Control
Elan SemenovaSemenova, Elan University of Maryland, College Park Formalizing Erlang’s Success Typings
Ilya SergeySergey, Ilya National University of SingaporeSingapore Industrial Relations Co-Chair in Organizing Committee for POPL 2025
Peter SewellSewell, Peter University of CambridgeUnited Kingdom A CHERI C Memory Model for Verified Temporal Safety Fulminate: Testing CN Separation-Logic Specifications in C
Florian SextlSextl, Florian TU Wien, AustriaAustria Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)
Ryan ShafferShaffer, Ryan AWS Quantum Technologies AutoQASM: Imperative quantum programming in Python
Bhakti ShahShah, Bhakti University of St. Andrews Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Razin A. ShaikhShaikh, Razin A. University of Oxford The Focked-up ZX Calculus: Picturing Continuous-Variable Quantum Computation
Amir ShaikhhaShaikhha, Amir University of EdinburghUnited Kingdom Committee Member in Program Committee within the LAFI-track
Farhad ShakerinShakerin, Farhad Microsoft C3G: Causally Constrained Counterfactual Generation
Chung-chieh ShanShan, Chung-chieh Indiana UniversityUnited States Committee Member in Program Committee within the POPL -track Committee Member in Steering Committee within the LAFI-track
Zhong ShaoShao, Zhong Yale UniversityUnited States Session Chair of Verification 2 (part of POPL ) Unifying compositional verification and certified compilation with a three-dimensional refinement algebra Committee Member in Program Committee within the POPL -track Committee Member in Steering Committee within the CPP-track
Jitendra SharmaSharma, Jitendra Miami University ASP for Language Documentation and Reclamation: A Derivational Stemming Tool for Myaamia
Subodh SharmaSharma, Subodh IIT DelhiIndia PC Member in Program Committee within the VMCAI-track
Ying ShengSheng, Ying Stanford University DafnyBench: A Benchmark for Formal Software Verification
Yunong ShiShi, Yunong AWS Quantum TechnologiesUnited States AutoQASM: Imperative quantum programming in Python
Shweta ShindeShinde, Shweta ETH ZurichSwitzerland Author in Steering Committee within the PriSC-track
Mahsa ShirmohammadiShirmohammadi, Mahsa CNRS & IRIF, Paris Simple Linear Loops: Algebraic Invariants and Applications
Sharon ShohamShoham, Sharon Tel Aviv UniversityIsrael Axe 'Em: Eliminating Spurious States with Induction Axioms A Primal-Dual Perspective on Program Verification Algorithms Associate Chair in Program Committee within the POPL -track
John ShorttShortt, John University of Ottawa A Coq Formalization of WebAssembly Execution Costs
Pratiksha ShresthaShrestha, Pratiksha Miami University ASP for Language Documentation and Reclamation: A Derivational Stemming Tool for Myaamia
Shuaizong Si Shuaizong Si Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, ChinaChina Automated Flaw Detection for Industrial Robot RESTful Service
Alexandra SilvaSilva, Alexandra Cornell UniversityUnited States Session Chair of Abstract Interpretation # 2 (part of VMCAI) Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching Keynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic program analysis A Demonic Outcome Logic for Randomized Nondeterminism
Violetta SimSim, Violetta Innopolis UniversityUzbekistan Committee Member in Student Volunteers for POPL 2025
Robert SimmonsSimmons, Robert IndependentUnited States Finite-Choice Logic Programming
Abhishek Kr SinghSingh, Abhishek Kr National University of SingaporeSingapore Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Satnam SinghSingh, Satnam GroqUnited States The Missing Diagonal: High Level Languages for Low Level Systems (Invited Talk Abstract) Semantics-based program manipulation in the age of LLMs
Kartik SinghalSinghal, Kartik QuantinuumUnited States Imperative Quantum Programming with Ownership and Borrowing in Guppy
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
Meghana Aparna SistlaSistla, Meghana Aparna The University of Texas at AustinUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Seyon SivarajahSivarajah, Seyon Quantinuum HUGR: A Quantum-Classical Intermediate Representation Imperative Quantum Programming with Ownership and Borrowing in Guppy
Anastasia SmirnovaSmirnova, Anastasia Innopolis University Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
Kaitlin SmithSmith, Kaitlin Northwestern University Unlocking quantum potential with software and compilers
Armando Solar-LezamaSolar-Lezama, Armando Massachusetts Institute of TechnologyUnited States Program Chair in Organizing Committee for POPL 2025 Lazy Knowledge Compilation for Discrete PPLs PC Chair in Program Committee within the POPL -track
Mallku SoldevilaSoldevila, Mallku FAMAF, UNC (Argentina) / CONICET (Argentina)Argentina Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Siva SomayyajulaSomayyajula, Siva Amazon Web Services Performant, Readable and Interoperable Rust from Dafny Dafny as Verification-Aware Intermediate Language for Code Generation
Fabio SomenziSomenzi, Fabio University of Colorado Boulder, USA PC Member in Program Committee within the VMCAI-track
Youngju SongSong, Youngju MPI-SWSGermany Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
Matthew SottileSottile, Matthew Lawrence Livermore National Laboratory Towards Verified Linear Algebra Programs Through Equivalence
Matthieu SozeauSozeau, Matthieu InriaFrance Session with the Coq Development Team All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
Bas SpittersSpitters, Bas Aarhus University CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
Bas SpittersSpitters, Bas Aarhus UniversityDenmark Committee Member in Program Committee within the CoqPL-track
Jiri SrbaSrba, Jiri Aalborg UniversityDenmark ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks
Meera SridharSridhar, Meera University of North Carolina Charlotte, USA PC Member in Program Committee within the VMCAI-track
B SrivathsanSrivathsan, B Chennai Mathematical InstituteIndia Committee Member in Program Committee within the VMCAI-track
Caleb StanfordStanford, Caleb University of California, DavisUnited States Artifact Evaluation Co-Chair in Organizing Committee for POPL 2025 Counterexamples in Safe Rust Auditing Rust Crates Effectively Co-chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Artem StarikovStarikov, Artem Innopolis University Towards Generic Higher-Order Unification Implementations in Haskell
Ian StarkStark, Ian The University of EdinburghUnited Kingdom A CHERI C Memory Model for Verified Temporal Safety
Kathrin StarkStark, Kathrin Heriot-Watt UniversityUnited Kingdom Session Chair of Session 1 (part of CoqPL) Session Chair of Session 6 (part of CPP) A Verified Foreign Function Interface Between Coq and C Conference Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track Author in Selection Committee within the POPL Student Research Competition-track Co-chair in Program Committee within the CoqPL-track
Philipp StassenStassen, Philipp Aarhus University Modelling Recursion and Probabilistic Choice in Guarded Type Theory
Sam StatonStaton, Sam University of OxfordUnited Kingdom NP-NUTS: A Nonparametric No-U-Turn Sampler Data-oriented Design for Differentiable, Probabilistic Programming (Remote) Algebraic and denotational semantics for Classically Controlled Quantum Communication Compositional imprecise probability: a solution from graded monads and Markov categories Committee Member in Program Committee within the LAFI-track
Tim SteenvoordenSteenvoorden, Tim Open UniversiteitNetherlands BeePL: Correct-by-compilation kernel extensions
Deian StefanStefan, Deian University of California at San DiegoUnited States Removing the runtime from the TCB and other adventures in making Wasm fast and more secure Auditing Rust Crates Effectively Author in Steering Committee within the PriSC-track
Peter Buus SteffensenSteffensen, Peter Buus Department of Computer Science, Aalborg University A Type Safe Calculus for Generating Syntax-Directed Editors
Dario SteinStein, Dario University of Oxford Committee Member in Program Committee within the LAFI-track
Kyle StoreyStorey, Kyle Brigham Young UniversityUnited States Property-agnostic base case extension for scalable verification of distributed systems
Yusen SuSu, Yusen University of WaterlooCanada Automatic Inference of Relational Object Invariants
Connor SughrueSughrue, Connor Virginia Tech BeePL: Correct-by-compilation kernel extensions
Alexander J. SummersSummers, Alexander J. University of British ColumbiaCanada Formal Foundations for Translational Separation Logic Verifiers
Chuyue SunSun, Chuyue Stanford University DafnyBench: A Benchmark for Formal Software Verification
Jun SunSun, Jun Singapore Management UniversitySingapore Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
Limin SunSun, Limin Institute of Information Engineering at Chinese Academy of Sciences; University of Chinese Academy of SciencesChina Automated Flaw Detection for Industrial Robot RESTful Service
Qinyi SunSun, Qinyi Massachusetts Institute of Technology DafnyBench: A Benchmark for Formal Software Verification
Zhouyue SunSun, Zhouyue Shanghai Jiao Tong UniversityChina Affine Disjunctive Invariant Generation with Farkas’ Lemma
Joshua SunshineSunshine, Joshua Carnegie Mellon University Gradual C0: Symbolic Execution for Gradual Verification
Ariadne Si SuoSuo, Ariadne Si University of Cambridge Semantic Analysis of Normalisation for Directional Logic Programming
Milijana SurbatovichSurbatovich, Milijana University of Maryland Intermittent Concurrency
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming Committee Member in Program Committee within the WITS-track
César SánchezSánchez, César IMDEA Software InstituteSpain MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs
T Nicolas TabareauTabareau, Nicolas InriaFrance Session Chair of Session 1 (part of CPP)
Nicolas TabareauTabareau, Nicolas Inria Session with the Coq Development Team
Nicolas TabareauTabareau, Nicolas InriaFrance Business Meeting All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants PC Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track PC Chair in Program Committee within the CPP-track
Kento TakyuTakyu, Kento Waseda UniversityJapan Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination
Raiki TamuraTamura, Raiki Kyoto UniversityJapan Wanco: WebAssembly AOT Compiler that supports Live Migration Wanco: WebAssembly AOT Compiler that supports Live Migration
Grace TanTan, Grace National University of Singapore The Store-Order Consistency Testing Problem for C-like Memory Models The Store-Order Consistency Testing Problem for C-like Memory Models
Yudai TanabeTanabe, Yudai Institute of Science TokyoJapan Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Qiyi TangTang, Qiyi University of LiverpoolUnited Kingdom Committee Member in Artifact Evaluation Committee within the VMCAI-track
Éric TanterTanter, Éric University of ChileChile All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants Gradual C0: Symbolic Execution for Gradual Verification
Zhe TaoTao, Zhe University of California, Davis Committee Member in Artifact Evaluation Committee within the VMCAI-track
Paul TarauTarau, Paul University of North TexasUnited States Leveraging LLM Reasoning with Dual Horn Programs Committee Member in Program Committee within the PADL-track
Joseph TassarottiTassarotti, Joseph New York UniversityUnited States A Demonic Outcome Logic for Randomized Nondeterminism Approximate Relational Reasoning for Higher-Order Probabilistic Programs PC Member in Program Committee within the CPP-track Author in Selection Committee within the POPL Student Research Competition-track Steering Committee Chair in Steering Committee Chairs within the Dafny-track
Enrico TassiTassi, Enrico INRIAFrance Elpi: rule-based meta-languge for Rocq Session with the Coq Development Team
Christine TassonTasson, Christine Sorbonne Université — LIP6France Committee Member in Steering Committee within the LAFI-track
Max TegmarkTegmark, Max Massachusetts Institute of Technology DafnyBench: A Benchmark for Formal Software Verification
Mohit TekriwalTekriwal, Mohit Lawrence Livermore National LaboratoryUnited States Towards Verified Linear Algebra Programs Through Equivalence Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Balder ten Cateten Cate, Balder ILLC, University of Amsterdam Algebras for Deterministic Computation are Inherently Incomplete
Joshua B. TenenbaumTenenbaum, Joshua B. Massachusetts Institute of TechnologyUnited States A Domain-Specific PPL for Reasoning about Reasoning (or: a memo on memo) Lazy Knowledge Compilation for Discrete PPLs
Tachio TerauchiTerauchi, Tachio Waseda UniversityJapan Committee Member in Program Committee within the POPL -track
Romain TetleyTetley, Romain Committee Member in Program Committee within the CoqPL-track
Aditya V. ThakurThakur, Aditya V. University of California at DavisUnited States Committee Member in Program Committee within the POPL -track PC Member in Program Committee within the VMCAI-track
Shriya ThakurThakur, Shriya Committee Member in Student Volunteers for POPL 2025
Jérémy ThibaultThibault, Jérémy MPI-SP Committee Member in Program Committee within the PriSC-track
René ThiemannThiemann, René University of Innsbruck An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
David ThienThien, David University of California, San Diego Auditing Rust Crates Effectively
Sarah TilscherTilscher, Sarah Technical University of Munich, Garching, GermanyGermany Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
Amin TimanyTimany, Amin Aarhus UniversityDenmark Conference Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
Laura TitoloTitolo, Laura AMA/NASA LaRCUnited States PC Member in Program Committee within the CPP-track Committee Member in Program Committee within the PADL-track
Ben L. TitzerTitzer, Ben L. Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the WAW-track
Saeid Tizpaz-NiariTizpaz-Niari, Saeid University of Texas at El PasoUnited States PC Member in Program Committee within the VMCAI-track
Andrew TolmachTolmach, Andrew Portland State University Meta-tracing Interpreters in WebAssembly
Diana TomilovskaiaTomilovskaia, Diana Innopolis University Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
James TownsendTownsend, James University of Amsterdam Committee Member in Program Committee within the LAFI-track
Dmitriy TraytelTraytel, Dmitriy University of CopenhagenDenmark Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings Committee Member in Steering Committee within the CPP-track
Richard TreflerTrefler, Richard University of Waterloo, Canada Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications
Jean-Baptiste TristanTristan, Jean-Baptiste Amazon Web ServicesUnited States Performant, Readable and Interoperable Rust from Dafny Verifying the Fisher-Yates Shuffle Algorithm in Dafny
Jean-Baptiste TristanTristan, Jean-Baptiste Committee Member in Steering Committee within the LAFI-track
Jean-Baptiste TristanTristan, Jean-Baptiste Amazon Web ServicesUnited States Steering Committee Chair in Steering Committee Chairs within the Dafny-track
Ashutosh TrivediTrivedi, Ashutosh University of Colorado BoulderUnited States Session Chair of Keynote Talk (Tuesday) and Learning (part of VMCAI) PC Chair in Program Committee within the VMCAI-track Co-chair in Organizing Committee within the VMCAI-track
Wei-Lun TsaiTsai, Wei-Lun Academia Sinica Committee Member in Student Volunteers for POPL 2025 An Automata-based Framework for Quantum Circuit Verification Verifying Quantum Circuits with Level-Synchronized Tree Automata
Stelios TsampasTsampas, Stelios FAU Erlangen-Nuremberg, INF 8 Abstract Operational Methods for Call-by-Push-Value
Takeshi TsukadaTsukada, Takeshi Chiba UniversityJapan A Primal-Dual Perspective on Program Verification Algorithms
Andrea TurriniTurrini, Andrea Institute of Software, Chinese Academy of SciencesChina Co-chair in Artifact Evaluation Committee within the VMCAI-track Artifact Evaluation Co-Chair in Organizing Committee within the VMCAI-track
Melinda TóthTóth, Melinda Eötvös Loránd University, Faculty of Informatics, Department of Programming Languages and Compilers & ELTE-Soft Nonprofit Ltd.Hungary Committee Member in Program Committee within the PADL-track
U Thien UdomsrirungruangUdomsrirungruang, Thien University of Oxford Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
Kazunori UedaUeda, Kazunori Waseda UniversityJapan Session Chair of Session 3 (part of PADL) Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination
Marcel UllrichUllrich, Marcel Saarland University, Saarland Informatics CampusGermany MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
Sebastian UllrichUllrich, Sebastian Lean FROGermany Chair in Program Committee within the WITS-track
Hiroshi UnnoUnno, Hiroshi Tohoku UniversityJapan Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs A Primal-Dual Perspective on Program Verification Algorithms
Dominique UnruhUnruh, Dominique RWTH Aachen Formalizing the One-way to Hiding Theorem Leakage-Free Probabilistic Jasmin Programs
Ramakrishna UpadrastaUpadrasta, Ramakrishna LLOR: Automated Repair of OpenMP Programs
Caterina UrbanUrban, Caterina Inria - École Normale SupérieureFrance Committee Member in Program Committee within the POPL -track
Henning UrbatUrbat, Henning FAU Erlangen-Nuremberg, INF 8 Abstract Operational Methods for Call-by-Push-Value
Elif UskupluUskuplu, Elif Indiana University, Bloomington Formalizing locally nameless syntax with cofinite quantification
V Viktor VafeiadisVafeiadis, Viktor MPI-SWSGermany Session Chair of Speculative Execution (part of POPL ) Stateless Model Checking Concurrent and Distributed Programs RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency Model Checking C/C++ with Mixed-Size Accesses Committee Member in Program Committee within the POPL -track
Deivid ValeVale, Deivid Radboud UniversityNetherlands Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Benoit ValironValiron, Benoit LRI, CentraleSupelec, Univ. Paris SaclayFrance Committee Member in Program Committee within the PLanQC-track
Milla ValnetValnet, Milla Sorbonne UniversitéFrance Committee Member in Artifact Evaluation Committee within the VMCAI-track
Jan van Brüggevan Brügge, Jan Heriot-Watt UniversityUnited Kingdom Committee Member in Student Volunteers for POPL 2025 Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
Jaco van de Polvan de Pol, Jaco Aarhus UniversityDenmark Program Analysis via Multiple Context Free Language Reachability
Mark van den Brandvan den Brand, Mark Eindhoven University of TechnologyNetherlands Committee Member in Program Committee Members within the PEPM-track
Sören van der Wallvan der Wall, Sören TU BraunschweigGermany SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
Niels van der Weidevan der Weide, Niels Radboud University Intrinsically Correct Sorting in Cubical Agda
Kylian Van DesselVan Dessel, Kylian Leuven.AI, Belgium A practical approach to handling tabular data in logic
Orpheas van Rooijvan Rooij, Orpheas University of EdinburghUnited Kingdom Affect: An Affine Type and Effect System
Julien VanegueVanegue, Julien Imperial College London; BloombergUnited States Committee Member in Program Committee within the TPSA-track
Alexa VanHattumVanHattum, Alexa Wellesley CollegeUnited States Committee Member in Program Committee within the PriSC-track
Gabriele VanoniVanoni, Gabriele IRIF, Université Paris Cité Interaction Equivalence Committee Member in Program Committee within the POPL -track
Anton VaronkaVaronka, Anton TU Wien Simple Linear Loops: Algebraic Invariants and Applications
Vasco T. VasconcelosVasconcelos, Vasco T. LASIGE, University of LisbonPortugal Committee Member in Program Committee within the POPL -track
Juan VasquezVasquez, Juan Committee Member in Student Volunteers for POPL 2025
Marco VassenaVassena, Marco Utrecht UniversityNetherlands Web Co-Chair in Organizing Committee for POPL 2025 Opening Remarks Closing Remarks Co-chair in Program Committee within the PriSC-track Committee Member in Steering Committee within the PriSC-track
Margus VeanesVeanes, Margus Microsoft Research RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds Symbolic Automata: omega-Regularity Modulo Theories Committee Member in Program Committee within the POPL -track
Joost VennekensVennekens, Joost KU Leuven A practical approach to handling tabular data in logic Committee Member in Program Committee within the PADL-track
Leonardo VenturiVenturi, Leonardo University of Bologna Size Analysis of Imperative Quantum Circuit Building Programs Through Floyd-Hoare Logics
Freek VerbeekVerbeek, Freek Open Universiteit & Virginia Tech BeePL: Correct-by-compilation kernel extensions On Extending Incorrectness Logic with Backwards Reasoning
Lena VerschtVerscht, Lena RWTH Aachen University; Saarland UniversityGermany Partial Incorrectness Logic A Taxonomy of Hoare-Like Logics
German VidalVidal, German Universitat Politecnica de ValenciaSpain Session Chair of Session 1 (part of PADL) Co-chair in Programme Chairs within the PADL-track
Jules VillardVillard, Jules MetaUnited Kingdom Introduction Committee Member in Organizing Committee within the TPSA-track Committee Member in Program Committee within the TPSA-track
Simon Friis VindumVindum, Simon Friis Aarhus UniversityDenmark The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
Max VistrupVistrup, Max ETH Zurich Program logics à la carte
Mahesh ViswanathanViswanathan, Mahesh University of Illinois at Urbana-ChampaignUnited States The Decision Problem for Regular First Order Theories
Finn VoichickVoichick, Finn University of MarylandUnited States Compiling Qunity: From High-Level Quantum Programs to Circuits
Vesal VojdaniVojdani, Vesal University of TartuEstonia Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
Tomáš VojnarVojnar, Tomáš Brno University of TechnologyCzechia Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)
Klaus von Gleissenthallvon Gleissenthall, Klaus Vrije Universiteit AmsterdamNetherlands Committee Member in Program Committee within the PriSC-track
Dimitrios VytiniotisVytiniotis, Dimitrios Google DeepMindUnited Kingdom Committee Member in Program Committee within the POPL -track
Matthijs VákárVákár, Matthijs Utrecht University Session Chair of Third session (part of LAFI) Session Chair of First session (part of LAFI) Welcome NP-NUTS: A Nonparametric No-U-Turn Sampler Committee Member in Program Committee within the POPL -track Co-chair in Program Committee within the LAFI-track
W Philip WadlerWadler, Philip University of Edinburgh Committee Member in Program Committee within the POPL -track
Luke WagnerWagner, Luke Fastly The WebAssembly Component Model
Riad S. WahbyWahby, Riad S. Stanford University, USA Universal Composability is Robust Compilation
Rameez WajidWajid, Rameez University of Colorado BoulderUnited States Committee Member in Student Volunteers for POPL 2025
Ryo WakizakaWakizaka, Ryo Kyoto UniversityJapan Concurrent Quantum Separation Logic for Fine-Grained Parallelism Concurrent Quantum Separation Logic for Fine-Grained Parallelism
Michael WalterWalter, Michael Ruhr-Universität Bochum Committee Member in Program Committee within the PLanQC-track
Anduo WangWang, Anduo Temple University, USA Enhancing network diagnosis with reflection in Prolog (extended abstract)
Chao WangWang, Chao University of Southern CaliforniaUnited States An Incremental Algorithm for Algebraic Program Analysis PC Member in Program Committee within the VMCAI-track
Claire WangWang, Claire Committee Member in Student Volunteers for POPL 2025
Jeffery WangWang, Jeffery CIMS, New York University Calculational Design of Hyperlogics by Abstract Interpretation
Jingbo WangWang, Jingbo Purdue University Session Chair of TOPLAS (part of POPL ) An Incremental Algorithm for Algebraic Program Analysis
Peixin WangWang, Peixin University of Oxford Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Theo WangWang, Theo University of Cambridge, University of OxfordUnited Kingdom Algebraic and denotational semantics for Classically Controlled Quantum Communication
Xinyu WangWang, Xinyu University of MichiganUnited States Committee Member in Program Committee within the POPL -track
Yuncheng WangWang, Yuncheng Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, ChinaChina Automated Flaw Detection for Industrial Robot RESTful Service
Yuting WangWang, Yuting Shanghai Jiao Tong UniversityChina Unifying compositional verification and certified compilation with a three-dimensional refinement algebra Committee Member in Program Committee within the PriSC-track
Zerong WangWang, Zerong Southeast University, NanjingChina A Weighted Bipolar Argumentation Framework and its ASP-based Implementation
Zhonghan WangWang, Zhonghan State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Committee Member in Artifact Evaluation Committee within the VMCAI-track
Frederic WantiezWantiez, Frederic State Space Model Programming in Turing.jl
Conrad WattWatt, Conrad Nanyang Technological UniversitySingapore Virtualization Chair in Organizing Committee for POPL 2025 Lighting talks and closing discussion Progressful Interpreters for Efficient WebAssembly Mechanisation Generically Automating Separation Logic by Functors, Homomorphisms, and Modules PC Member in Program Committee within the CPP-track Organizing Chair in Organizers within the WAW-track Committee Member in Program Committee within the PriSC-track
Anjiang WeiWei, Anjiang Stanford UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Guannan WeiWei, Guannan Inria/ENS; Tufts UniversityFrance A Big-Step Compositional Continuation-Passing Semantics for WebAssembly
Chana Weil-KennedyWeil-Kennedy, Chana IMDEA Software InstituteSpain Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
Christian WeilbachWeilbach, Christian University of British Columbia Partially Evaluating Higher-Order Probabilistic Programs without Stochastic Recursion to Graphical Models (Remote)
Maximilian WeiningerWeininger, Maximilian Institute of Science and Technology AustriaAustria 1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States Session Chair of Types 1 (part of POPL ) Consistency of a Dependent Calculus of Indistinguishability PC Member in Program Committee within the CPP-track
Pascal WeisenburgerWeisenburger, Pascal University of St. GallenSwitzerland Dis/Equality Graphs
Scott WesleyWesley, Scott Dalhousie University Verifying the Equivalence of Parameterized Quantum Circuits
Sam WestrickWestrick, Sam New York UniversityUnited States MPL: Provably Efficient Parallel Programming Author in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the PADL-track
Leo WhiteWhite, Leo Jane StreetUnited Kingdom Data Race Freedom à la Mode
John WickersonWickerson, John Imperial College LondonUnited Kingdom QuteFuzz: Fuzzing quantum compilers using randomly generated circuits with control flow and subcircuits
Remy WillemsWillems, Remy Amazon Helping users to reduce Brittleness in their Dafny programs - a success story
Douglas WilsonWilson, Douglas Quantinuum HUGR: A Quantum-Classical Intermediate Representation
Paul WilsonWilson, Paul University of Southampton Data-Parallel Differentiation by Optic Composition
Felix WindischWindisch, Felix Graz University of TechnologyAustria Synthesis of Controllers for Continuous Blackbox Systems
Sam WinnickWinnick, Sam University of Waterloo Programming with Projective Cliffords
Piotr WojciechowskiWojciechowski, Piotr West Virginia University, USAUnited States PC Member in Program Committee within the VMCAI-track
Dominik WojtczakWojtczak, Dominik Committee Member in Program Committee within the VMCAI-track
Cameron WongWong, Cameron Harvard SEAS Collapsing Towers for Side-Channel Security (Short Paper)
Frank WoodWood, Frank University of Oxford Partially Evaluating Higher-Order Probabilistic Programs without Stochastic Recursion to Graphical Models (Remote)
Nicolas WuWu, Nicolas Imperial College LondonUnited Kingdom Formalising Graph Algorithms with Coinduction
Shushu WuWu, Shushu Shanghai Jiao Tong University Relational Hoare Logic for Sequential Program Verification
Xiaodi WuWu, Xiaodi University of MarylandUnited States The Quantum Abstract Machine
Ānrán WángWáng, Ānrán Saarland University Partial Incorrectness Logic
X Anxhelo XhebrajXhebraj, Anxhelo NVIDIAUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ningning XieXie, Ningning University of TorontoCanada Publicity Chair in Organizing Committee for POPL 2025
Ruifeng XieXie, Ruifeng Peking University Committee Member in Student Volunteers for POPL 2025 Biparsers: Exact Printing for Data Synchronisation
Qiyuan XuXu, Qiyuan Nanyang Technological University Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
Runqing XuXu, Runqing A Framework of Differential Operators
Tianfan XuXu, Tianfan University of Illinois at Urbana-Champaign TensorRight: Automated Verification of Tensor Graph Rewrites
Yingte XuXu, Yingte MPI-SP and Institute of Software, Chinese Academy of Sciences Automating equational proofs in Dirac notation
Y Jeremy YallopYallop, Jeremy University of CambridgeUnited Kingdom Committee Member in Program Committee Members within the PEPM-track
Jonathon YallopYallop, Jonathon Committee Member in Student Volunteers for POPL 2025
Akihisa YamadaYamada, Akihisa National Institute of InformaticsJapan An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
Mengjia YanYan, Mengjia MIT Collapsing Towers for Side-Channel Security (Short Paper)
Yan YanYan, Yan Southeast University, NanjingChina A Weighted Bipolar Argumentation Framework and its ASP-based Implementation
Jianang YangYang, Jianang Million.js VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Junfeng YangYang, Junfeng Shanghai Key Laboratory of Trustworthy Computing, East China Normal UniversityChina Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training
Yihan YangYang, Yihan Harvey Mudd College Towards Verified Linear Algebra Programs Through Equivalence
Yuheng YangYang, Yuheng MIT Collapsing Towers for Side-Channel Security (Short Paper)
Peisen YaoYao, Peisen Zhejiang UniversityChina Committee Member in Program Committee within the POPL -track
Yue YaoYao, Yue Carnegie Mellon University A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types Semantic Logical Relations for Timed Message-Passing Protocols
Kevin YeYe, Kevin Simon Fraser University Committee Member in Student Volunteers for POPL 2025 Lightweight functional verification of quantum programs
Qianchuan YeYe, Qianchuan University at Buffalo, SUNYUnited States Session Chair of Session 4 (16:00 - 17:30) (part of CoqPL) Committee Member in Program Committee within the CoqPL-track
Lia YehYeh, Lia University of Oxford The Focked-up ZX Calculus: Picturing Continuous-Variable Quantum Computation Fusion and flow: formal protocols to reliably build photonic graph states Committee Member in Program Committee within the PLanQC-track
Di-De YenYen, Di-De Academia Sinica An Automata-based Framework for Quantum Circuit Verification
Mingsheng YingYing, Mingsheng Institute of Software at Chinese Academy of Sciences; Tsinghua UniversityChina Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs (Extended Abstract) Committee Member in Program Committee within the POPL -track
Irene YoonYoon, Irene France PC Member in Program Committee within the CPP-track Committee Member in Program Committee within the CoqPL-track
Taeyoung YoonYoon, Taeyoung Seoul National University Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
Nobuko YoshidaYoshida, Nobuko University of OxfordUnited Kingdom Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
Emily YuYu, Emily Institute of Science and Technology Austria Committee Member in Artifact Evaluation Committee within the VMCAI-track
Nengkun YuYu, Nengkun Stony Brook University, USAUnited States Committee Member in Program Committee within the PLanQC-track
Yongwei YuanYuan, Yongwei Purdue UniversityUnited States From Traces to Program Incorrectness: A Type-Theoretic Approach Derivative-Guided Symbolic Execution
Zhou YuanyuanYuanyuan, Zhou UCSD Laurel: Unblocking Automated Verification with Large Language Models
Tomofumi YukiYuki, Tomofumi Maximal Simplification of Polyhedral Reductions
Z Daniel ZackonZackon, Daniel McGill UniversityCanada Split Decisions: Explicit Contexts for Substructural Languages
Fabian ZaiserZaiser, Fabian University of Oxford Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
George ZakhourZakhour, George University of St. GallenSwitzerland Dis/Equality Graphs
Yannick ZakowskiZakowski, Yannick InriaFrance Web Co-Chair in Organizing Committee for POPL 2025 Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IR Committee Member in Program Committee within the PriSC-track
Vadim ZalivaZaliva, Vadim University of Cambridge, UKUnited States Artifact Evaluation Co-Chair in Organizing Committee for POPL 2025 A CHERI C Memory Model for Verified Temporal Safety Co-chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Vladimir ZamdzhievZamdzhiev, Vladimir InriaFrance Committee Member in Program Committee within the POPL -track
Fabio ZanasiZanasi, Fabio University College London Data-Parallel Differentiation by Optic Composition
Jessica ZangariZangari, Jessica Università della CalabriaItaly Committee Member in Program Committee within the PADL-track
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States General Chair in Organizing Committee for POPL 2025 Vellvm: Formalizing the Informal Committee Member in Steering Committee within the CPP-track
Nickolai ZeldovichZeldovich, Nickolai Massachusetts Institute of Technology, USA Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems
Stefan ZetzscheZetzsche, Stefan Amazon Web ServicesUnited Kingdom Session Chair of Keynote (part of Dafny) Session Chair of Proof Stability and Applications (part of Dafny) Session Chair of Verified Code Synthesis (part of Dafny) Session Chair of Backends and Teaching (part of Dafny) Day closing Verifying the Fisher-Yates Shuffle Algorithm in Dafny Day opening Dafny as Verification-Aware Intermediate Language for Code Generation Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny Randomised Testing of the Dafny Compiler: Into the CI Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track PC Chair in Program Committee Chairs within the Dafny-track
Cheng ZhangZhang, Cheng University College London (UCL)United Kingdom Domain Reasoning In TopKAT: Reduction and Completeness CF-GKAT: Efficient Validation of Control-Flow Transformations Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Danfeng ZhangZhang, Danfeng Duke UniversityUnited States Committee Member in Program Committee within the POPL -track
Jiatai ZhangZhang, Jiatai Tufts University A Big-Step Compositional Continuation-Passing Semantics for WebAssembly
Mona ZhangZhang, Mona Columbia University Gradual C0: Symbolic Execution for Gradual Verification
Naifeng ZhangZhang, Naifeng Carnegie Mellon University Towards Semantics Lifting for Scientific Computing: A Case Study on FFT
Ruoxi ZhangZhang, Ruoxi University of WaterlooCanada Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications
Weidong ZhangZhang, Weidong Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, UCAS Beijing, ChinaChina Automated Flaw Detection for Industrial Robot RESTful Service
Yizhou ZhangZhang, Yizhou University of WaterlooCanada Semantics of the memo Probabilistic Programming Language
Yu ZhangZhang, Yu Unifying compositional verification and certified compilation with a three-dimensional refinement algebra
Zhen ZhangZhang, Zhen Utah State UniversityUnited States Committee Member in Program Committee within the VMCAI-track
Zhicheng ZhangZhang, Zhicheng University of Technology Sydney Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs (Extended Abstract)
Zhizheng ZhangZhang, Zhizheng Southeast University, NanjingChina A Weighted Bipolar Argumentation Framework and its ASP-based Implementation
Eric ZhaoZhao, Eric Brown UniversityUnited States Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
Pinhan ZhaoZhao, Pinhan University of MichiganUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yaowen ZhengZheng, Yaowen Institute of Information Engineering at Chinese Academy of SciencesChina Automated Flaw Detection for Industrial Robot RESTful Service
Tan Zhi-XuanZhi-Xuan, Tan Massachusetts Institute of Technology Committee Member in Program Committee within the LAFI-track
Dinghong ZhongZhong, Dinghong Xi'an Jiaotong University A Big-Step Compositional Continuation-Passing Semantics for WebAssembly
Chenyu ZhouZhou, Chenyu University of Southern CaliforniaUnited States Session Chair of Kleene Algebra with Tests (part of POPL ) An Incremental Algorithm for Algebraic Program Analysis
Li ZhouZhou, Li Institute of Software, Chinese Academy of SciencesChina Automating equational proofs in Dirac notation
Litao ZhouZhou, Litao University of Hong KongChina Committee Member in Student Volunteers for POPL 2025 QuickSub: Efficient Iso-Recursive Subtyping Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Neng-Fa ZhouZhou, Neng-Fa CUNY Brooklyn College and Graduate Center Committee Member in Program Committee within the PADL-track
Xiangyu ZhouZhou, Xiangyu University of Michigan Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yi ZhouZhou, Yi Carnegie Mellon UniversityUnited States Towards Proof Stability in SMT-based Program Verification
Zhe ZhouZhou, Zhe Purdue University From Traces to Program Incorrectness: A Type-Theoretic Approach Derivative-Guided Symbolic Execution
Mingwei ZhuZhu, Mingwei University of Maryland, College Park The Quantum Abstract Machine
Shaopeng ZhuZhu, Shaopeng Currently in industry Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ekaterina ZhuchkoZhuchko, Ekaterina Tallinn University of Technology Committee Member in Student Volunteers for POPL 2025 Symbolic Automata: omega-Regularity Modulo Theories
Lukasz ZiarekZiarek, Lukasz University at BuffaloUnited States Semantic Logical Relations for Timed Message-Passing Protocols
Noam ZilbersteinZilberstein, Noam Cornell UniversityUnited States Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching Introduction A Demonic Outcome Logic for Randomized Nondeterminism Committee Member in Organizing Committee within the TPSA-track Committee Member in Program Committee within the TPSA-track
Conrad ZimmermanZimmerman, Conrad Northeastern UniversityUnited States Committee Member in Student Volunteers for POPL 2025 Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification Gradual C0: Symbolic Execution for Gradual Verification
Robert ZinkovZinkov, Robert University of Oxford VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
Lydia ZoghbiZoghbi, Lydia University of California, San Diego Auditing Rust Crates Effectively
Damien ZuffereyZufferey, Damien SonarSourceSwitzerland Committee Member in Program Committee within the POPL -track
Florian ZulegerZuleger, Florian TU ViennaAustria Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)
Fei ZuoZuo, Fei University of Central Oklahoma Exploring Answer Set Programming for Provenance Graph-Based Cyber Threat Detection: A Novel Approach
Maaike Annebet ZwartZwart, Maaike Annebet IT University of Copenhagen Modelling Recursion and Probabilistic Choice in Guarded Type Theory
Č Vedran ČačićČačić, Vedran CoqNFU: Towards Formalizing NFU in Coq
Ž Đorđe ŽikelićŽikelić, Đorđe Singapore Management University, SingaporeSingapore PC Member in Program Committee within the VMCAI-track

POPL 2025 Contributors

Results (1097)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia