POPL 2025 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (962)

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 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
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 Session Chair of High-level abstraction and automation (part of PEPM) Semantics of the memo Probabilistic Programming Language Collapsing Towers for Side-Channel Security (Short Paper) DafnyBench: A Benchmark for Formal Software Verification dafny-annotator: AI-Assisted Verification of Dafny Programs Keynote 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 Programme Committee 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 Programme Committee 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
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 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
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 Tufts UniversityUnited 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 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 Automating equational proofs in Dirac notation Preservation of speculative constant-time by compilation A quantitative probabilistic relational Hoare logic
Ezio BartocciBartocci, Ezio TU WienAustria Exact Inference for Nested Discrete Probabilistic Programs
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 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 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
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 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) 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
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
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
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
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 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 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
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. Gallen Dis/Equality Graphs
Joris CeulemansCeulemans, Joris KU LeuvenBelgium BiSikkel: A Multimode Logical Framework in Agda
Tej ChajedChajed, Tej UW-MadisonUnited States PC Member in Program Committee within the Dafny-track
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 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 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
Agnishom ChattopadhyayChattopadhyay, Agnishom Rice University 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 Vellvm: Formalizing the Informal
Liang-Ting ChenChen, Liang-Ting Academia SinicaTaiwan Committee Member in Programme Committee within the PEPM-track
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 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 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
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States 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 Semantic Analysis of Normalisation for Directional Logic Programming Towards Quantum Multiparty Session Types Intrinsically Correct Sorting in Cubical Agda The Duality of λ-Abstraction
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: A Fast and Differentiable Tokamak Transport Simulator in JAX
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
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 Programme Committee 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
Chen CuiCui, Chen University of Hong KongChina Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
Jack CzenszakCzenszak, Jack Northeastern University Towards Symbolic Execution for Probability and Non-determinism
D Loris D'AntoniD'Antoni, Loris UCSDUnited States 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 Formal Foundations for Translational Separation Logic Verifiers
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 From Traces to Program Incorrectness: A Type-Theoretic Approach Towards Automated Verification of LLM-Synthesized C Programs 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 PC Member in Program Committee within the VMCAI-track
Dominique DevrieseDevriese, Dominique KU LeuvenBelgium BiSikkel: A Multimode Logical Framework in Agda
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 Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
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
Derek DreyerDreyer, Derek MPI-SWSGermany A Semantic Approach to Robust Property Preservation Data Race Freedom à la Mode
Ross DuncanDuncan, Ross Quantinuum 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
Alec EdgingtonEdgington, Alec Quantinuum HUGR: A Quantum-Classical Intermediate Representation
Richard A. EisenbergEisenberg, Richard A. Jane StreetUnited States 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 Skaaning EngtorpEngtorp, Sune Skaaning Department of Computer Science, University of Copenhagen A type safe calculus for generating syntax-directed editors
Esra ErdemErdem, Esra Sabanci UniversityTurkey Co-chair in Programme Chairs within the PADL-track
Sebastian ErdwegErdweg, Sebastian JGU MainzGermany A Framework of Differential Operators
Ian Erik VarataluErik Varatalu, Ian Tallinn University of Technology, EstoniaEstonia RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds
Juhan ErnitsErnits, Juhan Tallinn University of Technology 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 FastlyUnited States 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
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
Qiuyi FengFeng, Qiuyi Formal Verification of Quantum Stabilizer Code
Maribel FernandezFernandez, Maribel King's College LondonUnited Kingdom Nominal Matching Logic With Fixpoints
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
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
Peng FuFu, Peng University of South Carolina 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
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 PC Member in Program Committee within the VMCAI-track
Gaetan GilbertGilbert, Gaetan All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
Eric GiovanniniGiovannini, Eric University of MichiganUnited States 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 Labs Sandwood: Runtime Adaptable Probabilistic Programming for Java
Andrew D. GordonGordon, Andrew D. Cogna and University of EdinburghUnited Kingdom Committee Member in Program Committee within the LAFI-track
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
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
Simon Oddershede GregersenGregersen, Simon Oddershede New York UniversityUnited States 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
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
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 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
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
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 Programme Committee within the PEPM-track
Simon HennigerHenniger, Simon Technical University of Munich 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 Programme Committee within the PEPM-track
Ángel HerranzHerranz, Ángel Universidad Politécnica de MadridSpain Checking Concurrency Coding Rules
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 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 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 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. McGill UniversityCanada 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 Programme Committee within the PEPM-track
Yipeng HuangHuang, Yipeng Rutgers UniversityUnited States Sdim: A Qudit Stabilizer Simulator
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
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 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
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
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
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 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 Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
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
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
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
Tobias KappéKappé, Tobias LIACS, Leiden University Algebras for Deterministic Computation are Inherently Incomplete CF-GKAT: Efficient Validation of Control-Flow Transformations
Chantal KellerKeller, Chantal Université Paris SaclayFrance Committee Member in Programme Committee 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 conditional 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
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
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 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
Michalis KokologiannakisKokologiannakis, Michalis ETH ZurichSwitzerland 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 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
Eric KoskinenKoskinen, Eric Stevens Institute of TechnologyUnited States Committee Member in Program Committee within the POPL -track
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 Programme Committee within the PEPM-track
Dexter KozenKozen, Dexter Cornell UniversityUnited States A Demonic Outcome Logic for Randomized Nondeterminism
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 Republic 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 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 Type Checking Implementations in Haskell via Second-Order Abstract Syntax Towards Generic Higher-Order Unification Implementations in Haskell
Anika KumarKumar, Anika Rutgers University Sdim: A Qudit Stabilizer Simulator
Viktor KunčakKunčak, Viktor EPFL, SwitzerlandSwitzerland 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
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 Pantograph: A Fluid and Typed Structure Editor 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
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 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 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 MIT 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 Lazy Knowledge Compilation for Discrete PPLs
Robert Y. LewisLewis, Robert Y. Brown UniversityUnited States PC Member in Program Committee within the CPP-track
Fang LiLi, Fang Oklahoma Christian University Exploring Answer Set Programming for Provenance Graph-Based Cyber Threat Detection: A Novel Approach
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
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 Language design, pedagogical tool, and staged interpreter (part of PEPM) Experience Report: Stack Switching in Wasm SpecTec Committee Member in Programme Committee within the PEPM-track
Marian Lingsch-RosenfeldLingsch-Rosenfeld, Marian LMU Munich Committee Member in Artifact Evaluation Committee within the VMCAI-track
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
Jing LiuLiu, Jing UC Irvine; MPI-SP Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
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) Solvers, unite! A simple unified semantics for reasoning with assurance and agreement Farewell Welcome 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 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
Andreas LööwLööw, Andreas Imperial College London Data Structure Abstraction and Incorrectness Separation Logic
M Dougal MaclaurinMaclaurin, Dougal Committee Member in Steering Committee within the LAFI-track
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
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 Finite-Choice Logic Programming
Patrick MassotMassot, Patrick Université Paris-SaclayFrance PC Member in Program Committee within the CPP-track
Christoph MathejaMatheja, Christoph DTUDenmark Workshops Co-Chair in Organizing Committee for POPL 2025
Umang MathurMathur, Umang National University of SingaporeSingapore 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 Verifying the Fisher-Yates Shuffle Algorithm in Dafny Performant, Readable and Interoperable Rust from Dafny
Micaela MayeroMayero, Micaela LIPN, Université Paris 13France PC Member in Program Committee within the CPP-track
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 CambridgeUnited Kingdom 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 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 Compiler Design Lab; Saarland Informatics Campus; Saarland UniversityGermany 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 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 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 Programme Committee within the PEPM-track
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
Eric MugnierMugnier, Eric University of California San Diego Laurel: Unblocking Automated Verification with Large Language Models
Prasita MukherjeeMukherjee, Prasita 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 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-SWS A Semantic Approach to Robust Property Preservation
Peter MüllerMüller, Peter ETH ZurichSwitzerland Formal Foundations for Translational Separation Logic Verifiers
N Keisuke NakanoNakano, Keisuke Tohoku UniversityJapan Characterizations of Partial Well-Behaved Lenses
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 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
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 / LRDE 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 Gothenburg 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
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 Bidirectional Higher-Rank Polymorphism with Intersection and Union Types QuickSub: Efficient Iso-Recursive Subtyping
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 Oded PadonPadon, Oded Weizmann Institute of ScienceIsrael A Primal-Dual Perspective on Program Verification Algorithms
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 Committee Member in Program Committee within the POPL -track Committee Member in Programme Committee within the PEPM-track
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
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 Towards Proof Stability in SMT-based Program Verification Teaching Types and Non-Interference in Dafny 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 Co-chair in Program Committee within the PriSC-track Author in Steering Committee within the PriSC-track
Andreas PavlogiannisPavlogiannis, Andreas Aarhus UniversityDenmark Program Analysis via Multiple Context Free Language Reachability PC Member in Program Committee within the VMCAI-track
Angel Dexter Pavlov AngelovPavlov Angelov, Angel Dexter Sofia UniversityBulgaria Committee Member in AV Committee for POPL 2025
Jennifer PaykinPaykin, Jennifer IntelUnited States 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
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
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 Committee Member in Program Committee within the POPL -track
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 McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory Semantics-based program manipulation in the age of LLMs A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract) 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
Ruzica PiskacPiskac, Ruzica Yale UniversityUnited States Associate Chair in Program Committee within the POPL -track
Clément Pit-ClaudelPit-Claudel, Clément EPFLSwitzerland Session Preview Co-Chair in Organizing Committee for POPL 2025 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
Adam PocockPocock, Adam Oracle LabsUnited States Sandwood: Runtime Adaptable Probabilistic Programming for Java
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
Andrei PopescuPopescu, Andrei University of SheffieldUnited Kingdom Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
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 Data Race Freedom à la Mode Tail Modulo Cons, OCaml, and Relational Separation Logic
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 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
Robert RandRand, Robert University of ChicagoUnited States Workshops Co-Chair in Organizing Committee for POPL 2025 Compiling Qunity: From High-Level Quantum Programs to Circuits Organizing Committee in Organizing Committee within the PLanQC-track
Francesco RanzatoRanzato, Francesco Dipartimento di Matematica, University of Padova, ItalyItaly 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
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
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 Programme Committee 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 Programme Committee 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
Neea RuschRusch, Neea Augusta UniversityUnited States 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 Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
Philipp RümmerRümmer, Philipp University of Regensburg and Uppsala University PC Member in Program Committee within the VMCAI-track
S Feras SaadSaad, Feras Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the POPL -track
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 conditional rewriting
Elmer SalazarSalazar, Elmer The University of Texas at DallasUnited States C3G: Causally Constrained Counterfactual Generation
Guido SalvaneschiSalvaneschi, Guido University of St. GallenSwitzerland 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 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 On Bridging Prolog and Python to Enhance an Inductive Logic Programming System
João SaraivaSaraiva, João Committee Member in Programme Committee 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 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
Tom SchrijversSchrijvers, Tom KU LeuvenBelgium Biparsers: Exact Printing for Data Synchronisation Committee Member in Program Committee within the PADL-track
Mircea SebeSebe, Mircea UIUC Nominal Matching Logic With Fixpoints
Md Syadus SefatSefat, Md Syadus Virginia TechUnited States On Extending Incorrectness Logic with Backwards Reasoning
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
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 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
Alexandra SilvaSilva, Alexandra Cornell UniversityUnited States Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching A Demonic Outcome Logic for Randomized Nondeterminism
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 Semantics-based program manipulation in the age of LLMs The Missing Diagonal: High Level Languages for Low Level Systems (Invited Talk Abstract)
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 Keynote
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
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 Auditing Rust Crates Effectively Counterexamples in Safe Rust 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 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 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 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
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
Qinyi SunSun, Qinyi Massachusetts Institute of Technology DafnyBench: A Benchmark for Formal Software Verification
Ariadne Si SuoSuo, Ariadne Si University of Cambridge Semantic Analysis of Normalisation for Directional Logic Programming
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
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
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 Approximate Relational Reasoning for Higher-Order Probabilistic Programs A Demonic Outcome Logic for Randomized Nondeterminism 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 Session with the Coq Development Team Elpi: rule-based meta-languge for Rocq
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
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 conditional rewriting
David ThienThien, David University of California, San Diego Auditing Rust Crates Effectively
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
Jean-Baptiste TristanTristan, Jean-Baptiste Amazon Web ServicesUnited States Verifying the Fisher-Yates Shuffle Algorithm in Dafny Performant, Readable and Interoperable Rust from 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 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 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 Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination
Marcel UllrichUllrich, Marcel Saarland UniversityGermany 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
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 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 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 Programme Committee within the PEPM-track
Sören van der Wallvan der Wall, Sören PhD StudentGermany 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
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 Symbolic Automata: omega-Regularity Modulo Theories RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds 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 Co-chair in Programme Chairs within the PADL-track
Jules VillardVillard, Jules MetaUnited Kingdom 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
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 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
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
Jeffery WangWang, Jeffery CIMS, New York University Calculational Design of Hyperlogics by Abstract Interpretation
Jingbo WangWang, Jingbo Purdue University 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 Oxford 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
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 Generically Automating Separation Logic by Functors, Homomorphisms, and Modules Progressful Interpreters for Efficient WebAssembly Mechanisation 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
Christian WeilbachWeilbach, Christian University of British Columbia Partially Evaluating Higher-Order Probabilistic Programs without Stochastic Recursion to Graphical Models
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States 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 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
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
Nicolas WuWu, Nicolas Imperial College LondonUnited Kingdom Formalising Graph Algorithms with Coinduction
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 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 Programme Committee within the PEPM-track
Akihisa YamadaYamada, Akihisa National Institute of InformaticsJapan An Isabelle formalization of co-rewrite pairs for non-reachability in conditional 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
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 Lightweight functional verification of quantum programs
Qianchuan YeYe, Qianchuan University at Buffalo, SUNYUnited States 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 Verifying the Fisher-Yates Shuffle Algorithm in Dafny Day opening Randomised Testing of the Dafny Compiler: Into the CI Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny Day closing Dafny as Verification-Aware Intermediate Language for Code Generation 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
Naifeng ZhangZhang, Naifeng Carnegie Mellon University Towards Semantics Lifting for Scientific Computing: A Case Study on FFT
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
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 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 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 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 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 Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via 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 (962)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia