POPL 2025 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (625)

A Parosh Aziz AbdullaAbdulla, Parosh Aziz Uppsala University, Sweden Verifying Quantum Circuits with Level-Synchronized Tree Automata PC Member in Program Committee within the VMCAI-track
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 Approximate Relational Reasoning for Higher-Order Probabilistic Programs Modelling Recursion and Probabilistic Choice in Guarded Type Theory
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 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
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
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 Committee Member in Program Committee within the PADL-track Committee Member in Programme Committee within the PEPM-track
Matthew AmyAmy, Matthew Simon Fraser UniversityCanada 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
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
Jaime AriasArias, Jaime CNRS; LIPN; Université Sorbonne Paris NordFrance Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
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
Mohamed Faouzi AtigAtig, Mohamed Faouzi Uppsala University, SwedenSweden Committee Member in Program Committee within the POPL -track
Robert AtkeyAtkey, Robert University of Strathclyde 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 Committee Member in Program Committee within the TPSA-track
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Rochester Institute of Technology, USAUnited States Committee Member in Program Committee within the POPL -track
B Michael BackesBackes, Michael Cispa Helmholtz Center for Information Security Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
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
Stephanie BalzerBalzer, Stephanie Carnegie Mellon UniversityUnited States 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
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 A quantitative probabilistic relational Hoare logic
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
Ryan BeckettBeckett, Ryan Microsoft Research, USA Committee Member in Program Committee within the POPL -track
Julia BelyakovaBelyakova, Julia Purdue UniversityUnited States Derivative-Guided Symbolic Execution
Clara Benac EarleBenac Earle, Clara Universidad Politécnica de MadridSpain Committee Member in Program Committee within the PADL-track
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States PC Member in Program Committee within the CPP-track
Malgorzata BiernackaBiernacka, Malgorzata University of Wrocław Committee Member in Program Committee within the PADL-track
Lars BirkedalBirkedal, Lars Aarhus UniversityDenmark Approximate Relational Reasoning for Higher-Order Probabilistic Programs Modelling Recursion and Probabilistic Choice in Guarded Type Theory
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
Clément BlaudeauBlaudeau, Clément InriaFrance Avoiding signature avoidance in ML modules with zippers
Sandrine BlazyBlazy, Sandrine University of RennesFrance 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
Ahmed BouajjaniBouajjani, Ahmed IRIF, Université Paris DiderotFrance PC Member in Program Committee within the VMCAI-track
Frédéric BourBour, Frédéric TaridesFrance Tail Modulo Cons, OCaml, and Relational Separation Logic
Oliver BračevacBračevac, Oliver EPFL, LAMPSwitzerland Committee Member in Program Committee within the POPL -track
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
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
Chris CasinghinoCasinghino, Chris Jane Street Data Race Freedom à la Mode
Laura M. CastroCastro, Laura M. University of A CoruñaSpain Committee Member in Program Committee within the PADL-track
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
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
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 Organizer in Organizing Committee within the PLMW @ POPL-track
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
Dong ChenChen, Dong Huawei Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
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
Xin ChenChen, Xin University of New Mexico, USAUnited States PC Member in Program Committee within the VMCAI-track
Yo-Ga ChenChen, Yo-Ga Academia Sinica Verifying Quantum Circuits with Level-Synchronized Tree Automata
Yu-Fang ChenChen, Yu-Fang Academia SinicaTaiwan Verifying Quantum Circuits with Level-Synchronized Tree Automata
James CheneyCheney, James University of EdinburghUnited Kingdom 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
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States 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 Alma Mater Studiorum - Università di BolognaItaly The Duality of Abstraction
Cheng-En ChuangChuang, Cheng-En University at BuffaloUnited States Semantic Logical Relations for Timed Message-Passing Protocols
Pierre ClairambaultClairambault, Pierre CNRS & LIS, Aix-Marseille UniversitéFrance Committee Member in Program Committee within the POPL -track
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 Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Andrea ColledanColledan, Andrea University of Bologna & INRIA Sophia Antipolis 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
Chen CuiCui, Chen University of Hong KongChina Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
D Loris D'AntoniD'Antoni, Loris UCSDUnited States PC Member in Program Committee within the VMCAI-track
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
Ugo Dal LagoDal Lago, Ugo University of Bologna & INRIA Sophia AntipolisItaly 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
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
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
Benjamin DelawareDelaware, Benjamin Purdue UniversityUnited States 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
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
Stephen DolanDolan, Stephen Jane StreetUnited Kingdom Data Race Freedom à la Mode
Alastair F. DonaldsonDonaldson, Alastair F. Imperial College LondonUnited Kingdom 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 Data Race Freedom à la Mode
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 Symbolic Automata: omega-Regularity Modulo Theories
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
Michael EmmiEmmi, Michael Amazon Web ServicesUnited States Committee Member in Program Committee within the POPL -track
Esra ErdemErdem, Esra Sabanci UniversityTurkey Co-chair in Programme Chairs within the PADL-track
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
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
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
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
Daniel FeldanFeldan, Daniel New York University Committee Member in Artifact Evaluation Committee within the VMCAI-track
Bernd FinkbeinerFinkbeiner, Bernd CISPA Helmholtz Center for Information SecurityGermany Coinductive Proofs for Temporal Hyperliveness
Cormac FlanaganFlanagan, Cormac University of California at Santa Cruz Committee Member in Program Committee within the POPL -track
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
Mario FrankFrank, Mario University of PotsdamGermany Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Cameron FreerFreer, Cameron Massachusetts Institute of TechnologyUnited States Committee Member in Steering Committee within the LAFI-track
Daniel FruminFrumin, Daniel University of GroningenNetherlands PC Member in Program Committee within the CPP-track
Zhoulai FuFu, Zhoulai State University of New York, Korea On Extending Incorrectness Logic with Backwards Reasoning
G Joshua GancherGancher, Joshua Northeastern UniversityUnited States 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
Poorva GargGarg, Poorva University of California, Los AngelesIndia Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Simon J. GayGay, Simon J. University of Glasgow, UKUnited Kingdom The Duality of Abstraction
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) 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
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
Pavel GolovinGolovin, Pavel MPI-SWS RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
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
Andrew D. GordonGordon, Andrew D. Cogna and University of EdinburghUnited Kingdom Committee Member in Program Committee within the LAFI-track
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
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 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 Committee Member in Program Committee within the PADL-track
H Sebastian HackHack, Sebastian Saarland University, Saarland Informatics CampusGermany 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
Michael HanusHanus, Michael Kiel UniversityGermany Committee Member in Program Committee within the PADL-track
Philipp G. HaselwarterHaselwarter, Philipp G. Aarhus UniversityDenmark Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Deyuan (Mike) HeHe, Deyuan (Mike) Princeton UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
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
Manuel HermenegildoHermenegildo, Manuel Technical University of Madrid (UPM) and IMDEA Software InstituteSpain Committee Member in Programme Committee within the PEPM-track
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
Kengo HirataHirata, Kengo University of Edinburgh 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
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the POPL -track
Steven HoltzenHoltzen, Steven Northeastern UniversityUnited States 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 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 Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
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 A Dependent Type Theory for Meta-programming with Intensional Analysis
Zhenjiang HuHu, Zhenjiang Peking UniversityChina Biparsers: Exact Printing for Data Synchronisation Committee Member in Programme Committee within the PEPM-track
Chung-Kil HurHur, Chung-Kil Seoul National UniversitySouth Korea VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
I Daniela InclezanInclezan, Daniela Miami UniversityUnited States Committee Member in Program Committee within the PADL-track
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
Yusuf IzmirliogluIzmirlioglu, Yusuf United Kingdom Committee Member in Program Committee within the PADL-track
J Suresh JagannathanJagannathan, Suresh Purdue UniversityUnited States 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
Tomi JanhunenJanhunen, Tomi Tampere UniversityFinland Committee Member in Program Committee within the PADL-track
Sumit JhaJha, Sumit Florida International University, USAUnited States Committee Member in Program Committee within the VMCAI-track
Ranjit JhalaJhala, Ranjit UCSD Generic Refinement Types
Limin JiaJia, Limin Carnegie Mellon University 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 The University of Hong Kong 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
Ivan KabashnyiKabashnyi, Ivan JetBrains Research, Constructor University Bremen, Germany Relaxed Memory Concurrency Re-executed
Gowtham KakiKaki, Gowtham University of Colorado at BoulderUnited States Committee Member in Program Committee within the POPL -track
Cezary KaliszykKaliszyk, Cezary University of MelbourneAustralia PC Member in Program Committee within the CPP-track
Benjamin Lucien KaminskiKaminski, Benjamin Lucien Saarland University; University College LondonGermany A Taxonomy of Hoare-Like Logics Committee Member in Program Committee within the TPSA-track Committee Member in Program Committee within the POPL -track
Jeehoon KangKang, Jeehoon KAISTSouth Korea PC Member in Program Committee within the CPP-track
Tobias KappéKappé, Tobias LIACS, Leiden University CF-GKAT: Efficient Validation of Control-Flow Transformations Algebras for Deterministic Computation are Inherently Incomplete
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
Artem KhyzhaKhyzha, Artem Arm LtdUnited Kingdom Committee Member in Program Committee within the POPL -track
Oisín KidneyKidney, Oisín Imperial College LondonUnited Kingdom Formalising Graph Algorithms with Coinduction
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 VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
Yoonseung KimKim, Yoonseung Yale UniversityUnited States VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
Zachary KincaidKincaid, Zachary Princeton UniversityUnited States Associate Chair in Program Committee within the POPL -track
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
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
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
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 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
Neel KrishnaswamiKrishnaswami, Neel University of CambridgeUnited Kingdom Student Research Competition Co-Chair in Organizing Committee for POPL 2025 Fulminate: Testing CN Separation-Logic Specifications in C Student Research Competition Chair in Selection Committee within the POPL Student Research Competition-track
Viktor KunčakKunčak, Viktor EPFL, SwitzerlandSwitzerland PC Member in Program Committee within the VMCAI-track
Cole KurashigeKurashige, Cole UCSD Generic Refinement Types
L Shadaj LaddadLaddad, Shadaj University of California at BerkeleyUnited States Flo: a Semantic Foundation for Progressive Stream Processing
Ambroise LafontLafont, Ambroise Ecole PolytechniqueFrance PC Member in Program Committee within the CPP-track
Christopher LamLam, Christopher University of Illinois, Urbana-ChampaignUnited States Audio/Video Co-Chairs in Organizing 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 Committee Member in Program Committee within the PADL-track
Vincent LaporteLaporte, Vincent Inria 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
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 Verifying Quantum Circuits with Level-Synchronized Tree Automata
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
Michael LeuschelLeuschel, Michael HHUGermany Committee Member in Program Committee within the PADL-track
Robert Y. LewisLewis, Robert Y. Brown UniversityUnited States PC Member in Program Committee within the CPP-track
Kwing Hei LiLi, Kwing Hei Aarhus UniversityDenmark Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Liyi LiLi, Liyi Iowa State UniversityUnited States Committee Member in Program Committee within the PLanQC-track
Runming LiLi, Runming Carnegie Mellon University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
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
Jack Liell-CockLiell-Cock, Jack University of Oxford Compositional imprecise probability: a solution from graded monads and Markov categories
Jyun-Ao LinLin, Jyun-Ao National Taipei University of TechnologyTaiwan 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 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
Cyrus LiuLiu, Cyrus Samsung SemiconductorUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
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 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 Verifying Quantum Circuits with Level-Synchronized Tree Automata
Sirui LuLu, Sirui University of WashingtonUnited States TensorRight: Automated Verification of Tensor Graph Rewrites
Xiaokun LuanLuan, Xiaokun Peking University Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
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
M Dougal MaclaurinMaclaurin, Dougal Committee Member in Steering Committee within the LAFI-track
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
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 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
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
Darko MarinovMarinov, Darko University of Illinois at Urbana-ChampaignUnited States Committee Member in Program Committee within the POPL -track
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
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
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 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
Eric MercerMercer, Eric Brigham Young UniversityUnited States Committee Member in Program Committee within the VMCAI-track
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 Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the VMCAI-track
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 PC Member in Program Committee within the CPP-track
Antoine MinéMiné, Antoine Sorbonne UniversitéFrance PC Member in Program Committee within the VMCAI-track
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
David MonniauxMonniaux, David Université Grenoble Alpes - CNRS - Grenoble INP - VerimagFrance 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
Sergio MoverMover, Sergio École PolytechniqueFrance PC Member in Program Committee within the VMCAI-track
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 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
Peter MüllerMüller, Peter ETH ZurichSwitzerland Formal Foundations for Translational Separation Logic Verifiers
N 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
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
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 QuickSub: Efficient Iso-Recursive Subtyping Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
Santiago Arranz OlmosOlmos, Santiago Arranz Max Planck Institute for Security and Privacy Preservation of speculative constant-time by compilation
Cyrus OmarOmar, Cyrus University of MichiganUnited States Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus Committee Member in Program Committee within the POPL -track
C.-H. Luke OngOng, C.-H. Luke NTU 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 Committee Member in Program Committee within the POPL -track
Hugo PaquetPaquet, Hugo LIPN, Université Sorbonne Paris NordFrance Committee Member in Program Committee within the LAFI-track
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 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 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
Jennifer PaykinPaykin, Jennifer Intel LabsUnited States 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
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
Lauren PickPick, Lauren UC Berkeley and UW-Madison Committee Member in Program Committee within the POPL -track
Brigitte PientkaPientka, Brigitte McGill UniversityCanada 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 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
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
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 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
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 Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
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
Vinayak PrabhuPrabhu, Vinayak Colorado State UniversityUnited States PC Member in Program Committee within the VMCAI-track
Jacob PrinzPrinz, Jacob University of Maryland, College Park Pantograph: A Fluid and Typed Structure Editor
Swarn PriyaPriya, Swarn Virginia TechUnited States 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
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 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
Mukund RaghothamanRaghothaman, Mukund University of Southern CaliforniaUnited States Committee Member in Program Committee within the POPL -track
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
Robert RandRand, Robert University of ChicagoUnited States Workshops Co-Chair in Organizing Committee for POPL 2025 Organizing Committee in Organizing Committee within the PLanQC-track
Francesco RanzatoRanzato, Francesco Dipartimento di Matematica, University of Padova, ItalyItaly The Best of Abstract Interpretations
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
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
Tiark RompfRompf, Tiark Purdue UniversityUnited States Committee Member in Programme Committee within the PEPM-track
Neil Julien RossRoss, Neil Julien Dalhousie UniversityCanada Committee Member in Program Committee within the PLanQC-track
Andreas RossbergRossberg, Andreas IndependentGermany Committee Member in Program Committee within the WAW-track
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
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
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 MPI-SWSGermany Program logics à la carte Formal Foundations for Translational Separation Logic Verifiers Committee Member in Program Committee within the PriSC-track
David SananSanan, David Nanyang Technological University, SingaporeSingapore Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
David SananSanan, David Singapore Institute of Technology Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
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
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
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
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
Tom SchrijversSchrijvers, Tom KU LeuvenBelgium Biparsers: Exact Printing for Data Synchronisation Committee Member in Program Committee within the PADL-track
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
Ilya SergeySergey, Ilya National University of SingaporeSingapore Industrial Relations Co-Chair in Organizing Committee for POPL 2025
Peter SewellSewell, Peter University of CambridgeUnited Kingdom Fulminate: Testing CN Separation-Logic Specifications in C
Bhakti ShahShah, Bhakti University of St. Andrews Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Amir ShaikhhaShaikhha, Amir University of EdinburghUnited Kingdom Committee Member in Program Committee within the LAFI-track
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
Subodh SharmaSharma, Subodh IIT DelhiIndia PC Member in Program Committee within the VMCAI-track
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 A Primal-Dual Perspective on Program Verification Algorithms Axe 'Em: Eliminating Spurious States with Induction Axioms Associate Chair in Program Committee within the POPL -track
Alexandra SilvaSilva, Alexandra Cornell UniversityUnited States 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
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
Armando Solar-LezamaSolar-Lezama, Armando Massachusetts Institute of TechnologyUnited States Program Chair in Organizing Committee for POPL 2025 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
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
Matthieu SozeauSozeau, Matthieu InriaFrance All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
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 Co-chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
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 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 Compositional imprecise probability: a solution from graded monads and Markov categories Committee Member in Program Committee within the LAFI-track
Deian StefanStefan, Deian University of California at San DiegoUnited States Author in Steering Committee within the PriSC-track
Dario SteinStein, Dario University of Oxford Committee Member in Program Committee within the LAFI-track
Alexander J. SummersSummers, Alexander J. University of British ColumbiaCanada Formal Foundations for Translational Separation Logic Verifiers
Jun SunSun, Jun Singapore Management UniversitySingapore Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States Committee Member in Program Committee within the WITS-track
T Nicolas TabareauTabareau, Nicolas InriaFrance All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants PC Chair in Organizing Committee within the CPP-track PC Chair in Program Committee within the CPP-track
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 Committee Member in Program Committee within the PADL-track
Joseph TassarottiTassarotti, Joseph New York UniversityUnited States A Demonic Outcome Logic for Randomized Nondeterminism Approximate Relational Reasoning for Higher-Order Probabilistic Programs PC Member in Program Committee within the CPP-track Author in Selection Committee within the POPL Student Research Competition-track Steering Committee Chair in Steering Committee Chairs within the Dafny-track
Christine TassonTasson, Christine Sorbonne Université — LIP6France Committee Member in Steering Committee within the LAFI-track
Mohit TekriwalTekriwal, Mohit Lawrence Livermore National LaboratoryUnited States 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
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
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
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 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 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
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 A Primal-Dual Perspective on Program Verification Algorithms Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order 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
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
Orpheas van Rooijvan Rooij, Orpheas 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 Co-chair in Program Committee within the PriSC-track Committee Member in Steering Committee within the PriSC-track
Margus VeanesVeanes, Margus Microsoft Research RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds Symbolic Automata: omega-Regularity Modulo Theories Committee Member in Program Committee within the POPL -track
Joost VennekensVennekens, Joost KU Leuven Committee Member in Program Committee within the PADL-track
Freek VerbeekVerbeek, Freek Open Universiteit & Virginia Tech On Extending Incorrectness Logic with Backwards Reasoning
Lena VerschtVerscht, Lena RWTH Aachen University; Saarland UniversityGermany 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
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
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 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
Michael WalterWalter, Michael Ruhr-Universität Bochum Committee Member in Program Committee within the PLanQC-track
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
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
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
Conrad WattWatt, Conrad Nanyang Technological UniversitySingapore Virtualization Chair in Organizing Committee for POPL 2025 Progressful Interpreters for Efficient WebAssembly Mechanisation Generically Automating Separation Logic by Functors, Homomorphisms, and Modules PC Member in Program Committee within the CPP-track Organizing Chair in Organizers within the WAW-track Committee Member in Program Committee within the PriSC-track
Anjiang WeiWei, Anjiang Stanford UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
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
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
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
Nicolas WuWu, Nicolas Imperial College LondonUnited Kingdom Formalising Graph Algorithms with Coinduction
X Anxhelo XhebrajXhebraj, Anxhelo NVIDIAUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ningning XieXie, Ningning University of Toronto; Google DeepMindCanada 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
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
Peisen YaoYao, Peisen Zhejiang UniversityChina Committee Member in Program Committee within the POPL -track
Yue YaoYao, Yue Carnegie Mellon University Semantic Logical Relations for Timed Message-Passing Protocols
Qianchuan YeYe, Qianchuan University at Buffalo, SUNYUnited States Committee Member in Program Committee within the CoqPL-track
Lia YehYeh, Lia University of Oxford Committee Member in Program Committee within the PLanQC-track
Mingsheng YingYing, Mingsheng Institute of Software at Chinese Academy of Sciences; Tsinghua UniversityChina Committee Member in Program Committee within the POPL -track
Irene YoonYoon, Irene InriaFrance 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 Derivative-Guided Symbolic Execution
Tomofumi YukiYuki, Tomofumi Maximal Simplification of Polyhedral Reductions
Z 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 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 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
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 Committee Member in Steering Committee within the CPP-track
Stefan ZetzscheZetzsche, Stefan Amazon Web ServicesUnited Kingdom 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 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
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
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
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
Zhe ZhouZhou, Zhe Purdue University Derivative-Guided Symbolic Execution
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 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
Damien ZuffereyZufferey, Damien SonarSourceSwitzerland Committee Member in Program Committee within the POPL -track
Maaike Annebet ZwartZwart, Maaike Annebet IT University of Copenhagen Modelling Recursion and Probabilistic Choice in Guarded Type Theory
Ž Đorđe ŽikelićŽikelić, Đorđe Singapore Management University, SingaporeSingapore PC Member in Program Committee within the VMCAI-track

POPL 2025 Contributors

Results (625)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia