POPL 2026 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (990)

A Zain K AamerAamer, Zain K University of PennsylvaniaUnited States Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
Parosh Aziz AbdullaAbdulla, Parosh Aziz Uppsala University; Mälardalen UniversitySweden Parametrised Verification of Intel-x86 Programs Parameterized Verification of Quantum Circuits
Andreas AbelAbel, Andreas Gothenburg UniversitySweden Committee Member in Program Committee within the WITS-track
Alexandre AbreuAbreu, Alexandre INESC TEC, Faculdade de Engenharia, Universidade do Porto Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
Robin AdamsAdams, Robin Chalmers University of Technology, Gothenburg University, Sweden A Graded Modal Type Theory for Pulse Schedules
Arthur AdjedjAdjedj, Arthur ENS Paris Saclay, Université Paris-Saclay AdapTT: Functoriality for Dependent Type Casts
Alejandro AguirreAguirre, Alejandro Aarhus UniversityDenmark Verifying Probabilistic Programs Using Separation Logic Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic
Danel AhmanAhman, Danel University of LjubljanaSlovenia Committee Member in Program Committee within the CPP-track
Amal AhmedAhmed, Amal Northeastern University, USAUnited States Cryptis: Cryptographic Reasoning in Separation Logic Committee Member in Organizing Committee within the RTFM-track Committee Member in Steering Committee within the PriSC-track
Joongwon AhnAhn, Joongwon Seoul National University Retargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
Benedikt AhrensAhrens, Benedikt Delft University of TechnologyNetherlands From Semantics to Syntax: A Type Theory for Comprehension Categories Committee Member in Selection Committee within the POPL Student Research Competition-track
C. AiswaryaAiswarya, C. Chennai Mathematical InstituteIndia Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
Ozgur AkgunAkgun, Ozgur University of St Andrews, St Andrews, UKUnited Kingdom Committee Member in Program Committee within the PADL-track
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin-MadisonUnited States Generating Compilers for Qubit Mapping and Routing
Franziska AlberAlber, Franziska University of Regensburg Verification of E-Voting Algorithms in Dafny
Jonathan AldrichAldrich, Jonathan Carnegie Mellon UniversityUnited States Security Reasoning via Substructural Dependency Tracking
Abdelghani AlidraAlidra, Abdelghani Inria The HOL-Light library of Multivariate real analysis in Rocq
Clément AllainAllain, Clément INRIAFrance Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic
Bernardo AlmeidaAlmeida, Bernardo LASIGE, Faculty of Sciences, University of Lisbon Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Types as grammars
Ricardo AlmeidaAlmeida, Ricardo University of Glasgow, UK Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Guillaume AmbalAmbal, Guillaume A Verified High-Performance Composable Object Library for Remote Direct Memory Access
Nada AminAmin, Nada Harvard UniversityUnited States Compiling to Linear Neurons Committee Member in Programme Chairs within the PADL-track Holey: Staged Execution from Python to SMT (Talk Proposal)
Matthew AmyAmy, Matthew Simon Fraser UniversityCanada Committee Member in Program Committee within the POPL -track Committee Member in Organizing Committee within the PLanQC-track
Jie AnAn, Jie Institute of Software Chinese Academy of SciencesChina SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation
Bruno AndreottiAndreotti, Bruno Universidade Federal de Minas GeraisBrazil Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
Cezar-Constantin AndriciAndrici, Cezar-Constantin MPI-SPGermany 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
Joaquín AriasArias, Joaquín Universidad Rey Juan CarlosSpain Committee Member in Programme Chairs within the PADL-track
Alasdair ArmstrongArmstrong, Alasdair University of Cambridge ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
Samuel ArsacArsac, Samuel ENS LyonFrance Adhesive Category Theory for Graph Rewriting in Rocq
Kenichi AsaiAsai, Kenichi Ochanomizu UniversityJapan Committee Member in Program Committee within the PEPM-track
Flavio AscariAscari, Flavio University of KonstanzGermany U-Turn: Enhancing Incorrectness Analysis by Reversing Direction A logic for all reasons
Nicola AssoliniAssolini, Nicola University of VeronaItaly Video Co-Chair in Organizing Committee for POPL 2026
Mohamed Faouzi AtigAtig, Mohamed Faouzi Uppsala UniversitySweden Parametrised Verification of Intel-x86 Programs
Robert AtkeyAtkey, Robert University of Strathclyde Committee Member in Program Committee within the PEPM-track
Hagit AttiyaAttiya, Hagit Technion - Israel Institute of TechnologyIsrael Arbitration-Free Consistency Is Available (and Vice Versa)
Steve AwodeyAwodey, Steve Carnegie Mellon University A Certifying Proof Assistant for Synthetic Mathematics in Lean
Sacha-Élie AyounAyoun, Sacha-Élie Imperial College LondonUnited Kingdom Specialisation: Context-Dependent Reasoning in Incorrectness Separation Logic Soteria Rust: Efficient Symbolic Execution for Rust Committee Member in Program Committee within the TPSA-track Committee Member in Organizing Committee within the TPSA-track
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Rochester Institute of TechnologyUnited States Cryptis: Cryptographic Reasoning in Separation Logic Committee Member in Program Committee within the RocqPL-track
Pedro H. Azevedo de AmorimAzevedo de Amorim, Pedro H. University of OxfordUnited Kingdom Committee Member in Program Committee within the LAFI-track
Damiano AzzoliniAzzolini, Damiano University of Ferrara Solving hard combinatorial optimization problems with PyQASP
Lăcrămioara AștefănoaeiAștefănoaei, Lăcrămioara Beneficial AI Foundation A benchmark for vericoding: formally verified program synthesis
B Miriam BackensBackens, Miriam Inria & Loria, Nancy, FranceFrance Committee Member in Program Committee within the PLanQC-track
Kyungmin BaeBae, Kyungmin POSTECHSouth Korea A Formal Executable Semantics of PROMELA
Patrick BahrBahr, Patrick IT University of CopenhagenDenmark Property-Based Testing for Asynchronous Functional Reactive Programming Using Linear Temporal Logic Committee Member in Program Committee within the PADL-track
Alexander BaiBai, Alexander New York UniversityUnited States Tunable Automation in Automated Program Verification
Patrick BaillotBaillot, Patrick Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStALFrance Dependent Coeffects for Local Sensitivity Analysis
Alexander BakstBakst, Alexander CertoraUnited States Committee Member in Program Committee within the VMCAI-track
Mantas BakšysBakšys, Mantas University of Cambridge ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
A. R. BalasubramanianBalasubramanian, A. R. Technical University of MunichGermany General Decidability Results for Systems with Continuous Counters
Marcello BalducciniBalduccini, Marcello Saint Joseph's University, USA Committee Member in Program Committee within the PADL-track
Stephanie BalzerBalzer, Stephanie Carnegie Mellon UniversityUnited States TypeDis: A Type System for Disentanglement Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PEPM-track
Debangshu BanerjeeBanerjee, Debangshu UIUC Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
Rini BanerjeeBanerjee, Rini University of CambridgeUnited Kingdom Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
Jialu BaoBao, Jialu Northeastern University Committee Member in Program Committee within the LAFI-track
Mikhail BarashBarash, Mikhail University of BergenNorway Towards a Mechanization of the ECMAScript (JavaScript) Proposal "Temporal" Lambda JS à la Carte
Davide BarbarossaBarbarossa, Davide University of BathUnited Kingdom Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
Haniel BarbosaBarbosa, Haniel Universidade Federal de Minas GeraisBrazil Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
Sébastien BardinBardin, Sébastien CEA LIST, University Paris-SaclayFrance BINSEC: Adapting Symbolic Execution for Binary-level Security Committee Member in Program Committee within the VMCAI-track
Clark BarrettBarrett, Clark Stanford UniversityUnited States Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions Proof Minimization in Neural Network Verification
Aurèle BarrièreBarrière, Aurèle EPFLSwitzerland Student Volunteer Co-Chair in Organizing Committee for POPL 2026 Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications
Gilles BartheBarthe, Gilles MPI-SP; IMDEA Software InstituteGermany Traq: Estimating the Quantum Cost of Classical Programs
Prabal BasuBasu, Prabal Utah State UniversityUnited States Probabilistic Verification for Modular Network-on-Chip Systems
Thomas BauereissBauereiss, Thomas University of CambridgeUnited Kingdom ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
Pascal BaumannBaumann, Pascal MPI-SWSGermany Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
Calvin BeckBeck, Calvin University of Pennsylvania, USACanada Artifact Evaluation Co-Chair in Organizing Committee for POPL 2026 Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Aaron BembenekBembenek, Aaron University of MelbourneAustralia Committee Member in Program Committee within the PADL-track
Clara Benac EarleBenac Earle, Clara Universidad Politécnica de MadridSpain Committee Member in Program Committee within the PADL-track
Thibaut BenjaminBenjamin, Thibaut Université Paris-Saclay, CEA, ListFrance AdapTT: Functoriality for Dependent Type Casts
Jean-Philippe BernardyBernardy, Jean-Philippe Chalmers University of Technology, Gothenburg University, Sweden A Graded Modal Type Theory for Pulse Schedules
Nathalie BertrandBertrand, Nathalie INRIA RennesFrance Reachability in multi-agent transfer systems
Frédéric BessonBesson, Frédéric Committee Member in Organizing Committee within the RocqPL-track
Marc BezemBezem, Marc University of Bergen Mechanically Verified Universe Checking and Variance Inference for The Rocq Prover
Karthikeyan BhargavanBhargavan, Karthikeyan Cryspen, FranceFrance Keynote Speaker in Keynote Speaker within the Dafny-track
Malgorzata BiernackaBiernacka, Malgorzata University of Wrocław Committee Member in Program Committee within the PADL-track
Lars BirkedalBirkedal, Lars Aarhus UniversityDenmark Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic
Adem BizidBizid, Adem MIT A benchmark for vericoding: formally verified program synthesis
Jasmin BlanchetteBlanchette, Jasmin Ludwig-Maximilians-Universität MünchenGermany Adding Sorts to an Isabelle Formalization of Superposition
Roberto BlancoBlanco, Roberto Max Planck Institute for Security and Privacy (MPI-SP) Committee Member in Program Committee within the PriSC-track
Frédéric BlanquiBlanqui, Frédéric Inria The HOL-Light library of Multivariate real analysis in Rocq
Sandrine BlazyBlazy, Sandrine University of RennesFrance General Chair in Organizing Committee for POPL 2026 Committee Member in Steering Committee within the CPP-track
Gregory BlikeBlike, Gregory University of Massachusetts at BostonUnited States A Modular Static Cost Analysis for GPU Warp-Level Parallelism
Roderick BloemBloem, Roderick Graz University of TechnologyAustria Parameterized Infinite-State Reactive Synthesis
Jonah BoeBoe, Jonah Hill Air Force Base, UtahUnited States Probabilistic Verification for Modular Network-on-Chip Systems
Rose BohrerBohrer, Rose National Institute of Advanced Industrial Science and Technology (AIST), JapanJapan Committee Member in Program Committee within the POPL -track
Borzoo BonakdarpourBonakdarpour, Borzoo Michigan State UniversityUnited States Efficient Discovery of Actual Causality in Stochastic Systems Committee Member in Program Committee within the VMCAI-track
Robert I. BoothBooth, Robert I. University of Oxford Denotational semantics for stabiliser quantum programs
Ahmed BouajjaniBouajjani, Ahmed Université Paris CitéFrance Parametrised Verification of Intel-x86 Programs
Olivier BouissouBouissou, Olivier Amazon Web ServicesUnited States ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification DafnyPro: LLM-Assisted Automated Verification for Dafny Programs Committee Member in Steering Committee Chairs within the Dafny-track
Thomas BourgeatBourgeat, Thomas EPFLSwitzerland Towards composable proofs of cache coherence protocols Committee Member in Program Committee within the RocqPL-track
Mathis Bouverot-DupuisBouverot-Dupuis, Mathis INRIA & École Normale SupérieureFrance Sulfur: Substitution Generation using a Logical Framework Code Generation via Meta-programming in Dependently Typed Proof Assistants
Matt BovelBovel, Matt EPFL First-Class Refinement Types in Scala
William J. BowmanBowman, William J. University of British ColumbiaCanada Committee Member in Program Committee within the PEPM-track
Benoît BoyerBoyer, Benoît Mitsubishi Electric R&D Centre Europe, Rennes, FranceFrance Verification of Generic VHDL Designs and Their Translation to Rocq A Correct-by-Construction Checker for Validation of Railway Data
Jonathan Immanuel BrachthäuserBrachthäuser, Jonathan Immanuel University of TübingenGermany Committee Member in Program Committee within the WITS-track
Joachim BreitnerBreitner, Joachim Lean FRO, LLCGermany Committee Member in Program Committee within the WITS-track
Einar Broch JohnsenBroch Johnsen, Einar University of OsloNorway Layers of Confluence for Actors
Greg BrownBrown, Greg University of Edinburgh A Dependent Language with Type-Safe Program Extraction
Roberto BruniBruni, Roberto University of PisaItaly U-Turn: Enhancing Incorrectness Analysis by Reversing Direction A logic for all reasons
Harry BryantBryant, Harry Swansea University Formal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq
Sergiu BursucBursuc, Sergiu Beneficial AI Foundation A benchmark for vericoding: formally verified program synthesis
Roger BurtonpatelBurtonpatel, Roger University of PennsylvaniaUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Oliver ButterleyButterley, Oliver Beneficial AI Foundation A benchmark for vericoding: formally verified program synthesis
William E. ByrdByrd, William E. University of Alabama at BirminghamUnited States Committee Member in Program Committee within the PADL-track
Robert BüttnerBüttner, Robert University of Regensburg Verification of E-Voting Algorithms in Dafny
C Matthew CaesarCaesar, Matthew UIUC Declarative Debugging for Modern Networks
Martina CamaioniCamaioni, Martina EPFLSwitzerland Towards composable proofs of cache coherence protocols
Brian CampbellCampbell, Brian University of EdinburghUnited Kingdom ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
Marco CampionCampion, Marco Inria Paris - ENS - Université PSLFrance A Logic for the Imprecision of Abstract Interpretations Committee Member in Program Committee within the POPL -track Committee Member in Organizing Committee within the GiacoFest-track
Filip Cano CórdobaCano Córdoba, Filip Institute of Science and Technology AustriaAustria Committee Member in Program Committee within the VMCAI-track
Noé CanvaCanva, Noé Inria Saclay & Université Paris-Saclay A Correct-by-Construction Checker for Validation of Railway Data
Xiuqing CaoCao, Xiuqing Zhejiang Sci-Tech UniversityChina A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamical Models
Mario CarneiroCarneiro, Mario Chalmers University of Technology A Certifying Proof Assistant for Synthetic Mathematics in Lean TBD
Thomas CarottiCarotti, Thomas MIT Foundational Verification of Running-Time Bounds for Interactive Programs
Chris CasinghinoCasinghino, Chris Jane Street A Guided Tour through Oxidized OCaml
Jean CasparCaspar, Jean École normale supérieure – PSL, INRIA, LS2N, CNRS S4 modal sequent calculus as intermediate logic and intermediate language (Short Paper)
Laura M. CastroCastro, Laura M. University of A CoruñaSpain Committee Member in Program Committee within the PADL-track
David Castro-PerezCastro-Perez, David University of KentUnited Kingdom A Synthetic Reconstruction of Multiparty Session Types
Ethan CecchettiCecchetti, Ethan University of Wisconsin-MadisonUnited States Generating Compilers for Qubit Mapping and Routing
Gabriele CeciliaCecilia, Gabriele Augusta University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Milan CeskaCeska, Milan Brno University of Technology Czechia Committee Member in Program Committee within the VMCAI-track
Devora Chait-RothChait-Roth, Devora New York UniversityUnited States Consistent Updates for Scalable Microservices
Tej ChajedChajed, Tej UW-MadisonUnited States Committee Member in Program Committee within the PriSC-track
Koushik ChakrabortyChakraborty, Koushik Utah State UniversityUnited States Probabilistic Verification for Modular Network-on-Chip Systems
Soham ChakrabortyChakraborty, Soham TU DelftNetherlands Committee Member in Selection Committee within the POPL Student Research Competition-track
Marek ChalupaChalupa, Marek Institute of Science and Technology Austria Co-chair in Artifact Evaluation Committee within the VMCAI-track
Antoine Chambert-LoirChambert-Loir, Antoine Université Paris Cité Formalizing polynomial laws and the universal divided power algebra
Bor-Yuh Evan ChangChang, Bor-Yuh Evan University of Colorado Boulder & AmazonUnited States Towards Cumulative Abstract Semantics via Handlers (Short Paper)
Nicolas ChappeChappe, Nicolas CNRS - VerimagFrance A Family of Sims with Diverging Interests
Kostia ChardonnetChardonnet, Kostia Université de Lorraine, CNRS, Inria, LORIA Compiling Quantum Lambda-Terms into Circuits via the Geometry of Interaction
Arthur CharguéraudCharguéraud, Arthur InriaFrance (TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection
Chun Yin ChauChau, Chun Yin HKUST (The Hong Kong University of Science and Technology) The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types
Dong ChenChen, Dong Huawei Technologies Co., Ltd Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Hanxi ChenChen, Hanxi Cornell University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Liang-Ting ChenChen, Liang-Ting Academia SinicaTaiwan Can we formalise type theory intrinsically without any compromise? A case study in Cubical Agda
Liqian ChenChen, Liqian National University of Defense TechnologyChina Committee Member in Program Committee within the VMCAI-track
Qinlin ChenChen, Qinlin Nanjing UniversityChina ChiSA: Static Analysis for Lightweight Chisel Verification
Yanning ChenChen, Yanning University of TorontoCanada Extensible Data Types with Ad-Hoc Polymorphism
Yu-Fang ChenChen, Yu-Fang Academia SinicaTaiwan Parameterized Verification of Quantum Circuits Co-chair in Organizing Committee within the VMCAI-track Co-chair in Program Committee within the VMCAI-track Verifying Repeat-Until-Success Circuits with AutoQ
Chih-Hong ChengCheng, Chih-Hong Carl von Ossietzky Universität Oldenburg & Chalmers University of TechnologyGermany Committee Member in Program Committee within the VMCAI-track
Marco ChiesaChiesa, Marco KTH Royal Institute of Technology Toward Automated, Contamination-free Dafny Benchmark Generation
Ionel Emilian ChiosaChiosa, Ionel Emilian MIT A benchmark for vericoding: formally verified program synthesis
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Foundational Verification of Running-Time Bounds for Interactive Programs Committee Member in Steering Committee within the CPP-track
Youngchan ChoCho, Youngchan The University of ChicagoUnited States Efficiently Verifying Quantum Programs with Few T Gates
Gregory ChocklerChockler, Gregory University of SurreyUnited Kingdom A Verified High-Performance Composable Object Library for Remote Direct Memory Access
Karen ChungChung, Karen Massachusetts Institute of TechnologyUnited States Probabilistic Programming with Vectorized Programmable Inference
Dulma ChurchillChurchill, Dulma MetaUnited Kingdom An LLVM frontend for Infer for Swift analysis
Ștefan CiobâcăCiobâcă, Ștefan Alexandru Ioan Cuza University of IasiRomania The Design of an Interactive Proof Mode for Dafny
Reinis CirponsCirpons, Reinis St Andrews University Certifying the decidability of the word problem in monoids at large
Jürgen CitoCito, Jürgen TU WienAustria Committee Member in Program Committee within the LAFI-track
Jesper CockxCockx, Jesper Delft University of TechnologyNetherlands Committee Member in Program Committee within the PADL-track
Tiago CogumbreiroCogumbreiro, Tiago University of Massachusetts at BostonUnited States A Modular Static Cost Analysis for GPU Warp-Level Parallelism
Cyril CohenCohen, Cyril Inria, CNRS, ENS Lyon, UCBL, LIPFrance Committee Member in Program Committee within the CPP-track Implementing parametricity in Rocq-ELPI
Joshua M. CohenCohen, Joshua M. Amazon Web Services Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Andrea ColledanColledan, Andrea University of Bologna; Centre Inria d’Université Côte d’AzurItaly On Circuit Description Languages, Indexed Monads, and Resource Analysis
Cole ComfortComfort, Cole INRIA Paris-Saclay Denotational semantics for stabiliser quantum programs
Youyou CongCong, Youyou Institute of Science TokyoJapan Committee Member in Program Committee within the PADL-track
Scott ConstableConstable, Scott Intel CorporationUnited States Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Basil L. ContovounesiosContovounesios, Basil L. Hungary Tracking Dynamically Bound Variable Dependencies
Diana CostaCosta, Diana LASIGE, University of LisbonPortugal Types as grammars
Nathanaëlle CourantCourant, Nathanaëlle OCamlProFrance A Lazy, Concurrent Convertibility Checker
Will CrichtonCrichton, Will Brown UniversityUnited States A Guided Tour through Oxidized OCaml
Chen CuiCui, Chen University of Hong KongChina Local Contextual Type Inference
Jiacai CuiCui, Jiacai Nanjing UniversityChina ChiSA: Static Analysis for Lightweight Chisel Verification
Joseph W. CutlerCutler, Joseph W. University of PennsylvaniaUnited States Typing Strictness
D Loris D'AntoniD'Antoni, Loris University of California at San DiegoUnited States Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models
Emanuele D'OsualdoD'Osualdo, Emanuele University of KonstanzGermany RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
Raquel Fernandes da Silvada Silva, Raquel Fernandes Imperial College LondonUnited Kingdom Specialisation: Context-Dependent Reasoning in Incorrectness Separation Logic
Sander R. DahmenDahmen, Sander R. Vrije Universiteit Amsterdam Committee Member in Program Committee within the CPP-track
Ugo Dal LagoDal Lago, Ugo University of Bologna; Centre Inria d’Université Côte d’AzurItaly On Circuit Description Languages, Indexed Monads, and Resource Analysis Compiling Quantum Lambda-Terms into Circuits via the Geometry of Interaction Committee Member in Program Committee within the PLanQC-track
Mila Dalla PredaDalla Preda, Mila University of VeronaItaly A Logic for the Imprecision of Abstract Interpretations Committee Member in Program Committee within the POPL -track Committee Member in Organizing Committee within the GiacoFest-track
Mads DamDam, Mads KTHSweden Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Hoang-Hai DangDang, Hoang-Hai BedRock SystemsGermany Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic
Lesly-Ann DanielDaniel, Lesly-Ann EURECOMFrance Committee Member in Steering Committee within the PriSC-track Committee Member in Steering Committee within the PriSC-track Co-chair in Program Committee within the PriSC-track
Nils Anders DanielssonDanielsson, Nils Anders University of GothenburgSweden Normalisation for First-Class Universe Levels
Ornela DardhaDardha, Ornela University of GlasgowUnited Kingdom Committee Member in Program Committee within the POPL -track
Thibault DardinierDardinier, Thibault ETH ZurichSwitzerland Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the TPSA-track
Sopam DasguptaDasgupta, Sopam The University of Texas at Dallas Interpretable Configuration Optimization for Static Program Verification via Rule-Based and Counterfactual Reasoning
Davide DavoliDavoli, Davide MPI-SPGermany Committee Member in Program Committee within the PriSC-track
Alexis de Colnetde Colnet, Alexis TU WienAustria Counting and Sampling Traces in Regular Languages
Valeria de Paivade Paiva, Valeria Topos InstituteUnited States Committee Member in Program Committee within the POPL -track
Coen De RooverDe Roover, Coen Vrije Universiteit BrusselBelgium Committee Member in Program Committee within the VMCAI-track
Noé De SantoDe Santo, Noé University of PennsylvaniaUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Paulo Emílio de Vilhenade Vilhena, Paulo Emílio Imperial College London A Relational Separation Logic for Effect Handlers Committee Member in Program Committee within the POPL -track
Benjamin DelawareDelaware, Benjamin Purdue UniversityUnited States Committee Member in Organizing Committee within the RocqPL-track
Remi DelmasDelmas, Remi Amazon Web Services ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
Victor DengDeng, Victor EPFL; École Normale Supérieure - PSL - CNRSSwitzerland Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications
Martin DesharnaisDesharnais, Martin Ludwig-Maximilians-Universität München Adding Sorts to an Isabelle Formalization of Superposition
Rémi Di GuardiaDi Guardia, Rémi IRIF (CNRS, Université Paris Cité)France Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Luca Di StefanoDi Stefano, Luca Technische Universität WienAustria Committee Member in Artifact Evaluation Committee within the VMCAI-track
Tomás DiazDiaz, Tomás University of ChileChile Bounded Sort Polymorphism with Elimination Constraints
Fabian Franz DießlDießl, Fabian Franz University of Regensburg Verification of E-Voting Algorithms in Dafny
Rayna DimitrovaDimitrova, Rayna CISPA, GermanyGermany Committee Member in Program Committee within the POPL -track
Rayna DimitrovaDimitrova, Rayna CISPA Helmholtz Center for Information Security Committee Member in Selection Committee within the POPL Student Research Competition-track
Jenna DiVincenzo (Wise)DiVincenzo (Wise), Jenna Purdue University Committee Member in Organizing Committee within the PLMW @ POPL-track
Greta DolcettiDolcetti, Greta Ca’ Foscari University of VeniceItaly Committee Member in Artifact Evaluation Committee within the VMCAI-track
Brijesh DongolDongol, Brijesh University of SurreyUnited Kingdom A Verified High-Performance Composable Object Library for Remote Direct Memory Access
Quinn DoughertyDougherty, Quinn Beneficial AI Foundation A benchmark for vericoding: formally verified program synthesis
Paul DownenDownen, Paul University of Massachusetts at LowellUnited States Committee Member in Program Committee within the PEPM-track
Derek DreyerDreyer, Derek MPI-SWSGermany Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation A Recipe for Modular Verification of Generic Tree Traversals Committee Member in Organizing Committee within the RTFM-track
Claire DrossDross, Claire AdaCoreFrance Managing the Proof Context in SPARK
Ke DuDu, Ke Recursive Mutexes in Separation Logic
Catherine DuboisDubois, Catherine ENSIIE Paris-Evry Committee Member in Program Committee within the CPP-track
Ross DuncanDuncan, Ross Quantinuum Committee Member in Organizing Committee within the PLanQC-track
Arpita DuttaDutta, Arpita National University of SingaporeSingapore Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
E Gabriel EbnerEbner, Gabriel Microsoft ResearchUnited States Committee Member in Program Committee within the CPP-track
Dimitrios J. EconomouEconomou, Dimitrios J. University of Cambridge Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
Theodore EhrenborgEhrenborg, Theodore Beneficial AI Foundation A benchmark for vericoding: formally verified program synthesis
Aria B. EideEide, Aria B. University of Bergen Towards a Mechanization of the ECMAScript (JavaScript) Proposal "Temporal"
Richard A. EisenbergEisenberg, Richard A. Jane StreetUnited States A Guided Tour through Oxidized OCaml
Rida Ait El ManssourEl Manssour, Rida Ait University of OxfordUnited Kingdom Determination Problems for Orbit Closures and Matrix Groups
Neta EladElad, Neta Tel Aviv UniversityIsrael Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
Laila ElbeheiryElbeheiry, Laila MPI-SWS A Recipe for Modular Verification of Generic Tree Traversals
Constantin EneaEnea, Constantin LIX, CNRS, Ecole Polytechnique Verifying Almost-Sure Termination for Randomized Distributed Algorithms Arbitration-Free Consistency Is Available (and Vice Versa) Committee Member in Program Committee within the POPL -track
Andres ErbsenErbsen, Andres Google Foundational Verification of Running-Time Bounds for Interactive Programs
Esra ErdemErdem, Esra Sabanci UniversityTurkey Committee Member in Program Committee within the PADL-track
Sebastian ErdwegErdweg, Sebastian KITGermany Stateful Differential Operators for Incremental Computing Committee Member in Program Committee within the PEPM-track
Julian ErhardErhard, Julian TU Munich; LMU MunichGermany Data Race Detection by Digest-Driven Abstract Interpretation
Gidon ErnstErnst, Gidon LMU MunichGermany Committee Member in Program Committee within the VMCAI-track
Sebastian ErtelErtel, Sebastian Barkhausen Institute, Dresden Scalable Type Inference for Intrinsically-Typed Binders
Javier EsparzaEsparza, Javier Technical University of Munich Committee Member in Program Committee within the VMCAI-track
Ran EttingerEttinger, Ran NVIDIA and Ben-Gurion University of the Negev and Israel Academic College in Ramat Gan Teaching Automata Theory and Formal Languages with Dafny
F Claudia FaggianFaggian, Claudia CNRS, Université Paris Cité Committee Member in Program Committee within the PLanQC-track
Uli FahrenbergFahrenberg, Uli Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMFFrance Discrete and Continuous Models for Concurrent Systems: From Petri Nets to Directed Spaces
Florian FaissoleFaissole, Florian Mitsubishi Electric R&D Centre EuropeFrance Verification of Generic VHDL Designs and Their Translation to Rocq
Chris FallinFallin, Chris F5United States Committee Member in Steering Committee within the PriSC-track
Andong FanFan, Andong University of TorontoCanada Type Inference Techniques: Implementation and Formalization, Better Together
Yuyou FanFan, Yuyou University of UtahUnited States Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
Wang FangFang, Wang University of EdinburghUnited Kingdom Hadamard-Pi: Equational Quantum Programming
Naïm Camille FavierFavier, Naïm Camille Chalmers University of Technology and University of GothenburgSweden Normalisation for First-Class Universe Levels
Aleksandr FedchinFedchin, Aleksandr Tufts UniversityUnited States DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
Grigory FedyukovichFedyukovich, Grigory Florida State UniversityUnited States Committee Member in Program Committee within the VMCAI-track
Thiago FelicissimoFelicissimo, Thiago InriaFrance Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Shenghua FengFeng, Shenghua Institute of Software at Chinese Academy of SciencesChina Piecewise Analysis of Probabilistic Programs via k-Induction
Yuan FengFeng, Yuan Tsinghua UniversityChina An Expressive Assertion Language for Quantum Programs
Laouen FernetFernet, Laouen University of Copenhagen Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
María Inés de Frutos FernándezFernández, María Inés de Frutos University of Bonn Formalizing polynomial laws and the universal divided power algebra
Francisco FerreiraFerreira, Francisco Royal Holloway, University of London A Synthetic Reconstruction of Multiparty Session Types
Daniela FerreiroFerreiro, Daniela Technical University of Madrid and IMDEA Software Institute Multi-Configurable Search Rules in Prolog and Application to Testing
Nathanaël FijalkowFijalkow, Nathanaël CNRS, LaBRI, University of BordeauxFrance Is Program Synthesis Soluble in Large Language Models? Committee Member in Program Committee within the POPL -track
Dana FismanFisman, Dana Ben-Gurion UniversityIsrael Atomic Gliders and Cellular Automata as Language Generators
Davide FissoreFissore, Davide Inria Determinacy Checking for Elpi: an Higher-Order Logic Programming Language with Cut
Matthew FlattFlatt, Matthew University of UtahUnited States Committee Member in Program Committee within the PADL-track
Eugene FlesselleFlesselle, Eugene EPFLSwitzerland Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yannick ForsterForster, Yannick INRIAFrance PLMW Co-Chair in Organizing Committee for POPL 2026 Nested Inductive Types for Rocq and Lean Committee Member in Organizing Committee within the PLMW @ POPL-track Code Generation via Meta-programming in Dependently Typed Proof Assistants Committee Member in Program Committee within the WITS-track
Jeffrey S. FosterFoster, Jeffrey S. Tufts UniversityUnited States DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
Simon FowlerFowler, Simon University of GlasgowUnited Kingdom Committee Member in Program Committee within the PADL-track
Andrew FoxFox, Andrew University of Colorado BoulderUnited States Towards Cumulative Abstract Semantics via Handlers (Short Paper)
Justine FrankFrank, Justine University of Maryland, College Park Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-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
Asta Halkjær FromFrom, Asta Halkjær University of CopenhagenDenmark Committee Member in Program Committee within the CPP-track
Aymeric FromherzFromherz, Aymeric InriaFrance Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the PriSC-track
Hongfei FuFu, Hongfei Shanghai Jiao Tong UniversityChina Piecewise Analysis of Probabilistic Programs via k-Induction
Zhoulai FuFu, Zhoulai State University of New York, Korea Committee Member in Program Committee within the POPL -track
G Marco GaboardiGaboardi, Marco Boston UniversityUnited States Cryptis: Cryptographic Reasoning in Separation Logic Committee Member in Program Committee within the POPL -track
Sankalp GambhirGambhir, Sankalp Ecole Polytechnique Federale de Lausanne (EPFL) Committee Member in Artifact Evaluation Committee within the VMCAI-track
Vijay GaneshGanesh, Vijay Georgia TechUnited States Committee Member in Program Committee within the VMCAI-track
Luis GarciaGarcia, Luis Epistemic Logic for Polyglots (Short Paper)
Deepak GargGarg, Deepak MPI-SWSGermany Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation A Recipe for Modular Verification of Generic Tree Traversals
Poorva GargGarg, Poorva University of California, Los AngelesIndia Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Program Committee within the LAFI-track
Ilias GarnierGarnier, Ilias France Committee Member in Program Committee within the LAFI-track
Lorenzo GazzellaGazzella, Lorenzo Università di Pisa A logic for all reasons
Martin GebserGebser, Martin University of Klagenfurt, AustriaAustria Committee Member in Program Committee within the PADL-track
Aina Linn GeorgesGeorges, Aina Linn Max Planck Institute for Software Systems (MPI-SWS)Germany Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation
Herman GeuversGeuvers, Herman Radboud University Nijmegen, Netherlands A systematic approach to "Well-founded recursion done right"
Seyedhamed GhavamniaGhavamnia, Seyedhamed Bloomberg AMPLE: Fine-grained File Access Policies for Server Applications
Arka GhoshGhosh, Arka Université de Bordeaux / LaBRI Committee Member in Artifact Evaluation Committee within the VMCAI-track
Roberto GiacobazziGiacobazzi, Roberto University of ArizonaUnited States A Logic for the Imprecision of Abstract Interpretations Committee Member in Program Committee within the VMCAI-track
Paolo G. GiarrussoGiarrusso, Paolo G. Delft University of Technology Recursive Mutexes in Separation Logic
Marco GiuntiGiunti, Marco University of AlgarvePortugal Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Giulia GiustiGiusti, Giulia ENS LyonFrance JAX Autodiff from a Linear Logic Perspective
Vladimir GladshteinGladshtein, Vladimir Foundational Multi-Modal Program Verifiers Velvet: A Multi-Modal Verifier for Effectful Programs Lessons from Building an Auto-Active Verifier in Lean
Robert GlückGlück, Robert University of CopenhagenDenmark Committee Member in Program Committee within the PEPM-track
Shilpi GoelGoel, Shilpi Centaur Technology, Inc. Committee Member in Program Committee within the CPP-track
Andrés GoensGoens, Andrés TU DarmstadtGermany Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
Arnaud GolfouseGolfouse, Arnaud Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France Creusot: Formal verification of Rust programs Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
Anitha GollamudiGollamudi, Anitha University of Massachusetts LowellUnited States Committee Member in Program Committee within the PriSC-track
Kirill GolubevGolubev, Kirill University of TurkuFinland Lambda JS à la Carte
Hannah GommerstadtGommerstadt, Hannah Vassar College Diversity, Equity, and Inclusion Chair in Organizing Committee for POPL 2026
Sergey GoncharovGoncharov, Sergey University of BirminghamUnited Kingdom Committee Member in Program Committee within the POPL -track
Georges GonthierGonthier, Georges Inria Committee Member in Steering Committee within the CPP-track
Kiran GopinathanGopinathan, Kiran University of Illinois Urbana ChampaignUnited States Committee Member in Program Committee within the RocqPL-track
Colin GordonGordon, Colin Drexel UniversityUnited States Associate Chair in Program Committee within the POPL -track
Roberta GoriGori, Roberta Diaprtimento di Informatica, Universita' di Pisa, Italy U-Turn: Enhancing Incorrectness Analysis by Reversing Direction A logic for all reasons
Roberta GoriGori, Roberta University of PisaItaly Committee Member in Program Committee within the TPSA-track
Sebastien GouezelGouezel, Sebastien CNRS and Rennes University Higher order differential calculus in Mathlib
Hemant GouniGouni, Hemant Carnegie Mellon UniversityUnited States Security Reasoning via Substructural Dependency Tracking
Gavin GrayGray, Gavin Brown UniversityUnited States A Guided Tour through Oxidized OCaml
Michael GreenbergGreenberg, Michael Stevens Institute of TechnologyUnited States Industrial Relations Co-Chair in Organizing Committee for POPL 2026 Analyzing Shell Scripts
Ben GreenmanGreenman, Ben University of Utah, USA Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
Simon Oddershede GregersenGregersen, Simon Oddershede New York UniversityUnited States Verifying Probabilistic Programs Using Separation Logic
Benjamin GregoireGregoire, Benjamin INRIA Committee Member in Program Committee within the PriSC-track
Robert GriesemerGriesemer, Robert GoogleUnited States Welterweight Go: Boxing, Structural Subtyping, and Generics
Harrison GrodinGrodin, Harrison Carnegie Mellon UniversityUnited States Abstraction Functions as Types
Samuel GroßGroß, Samuel GoogleSwitzerland The V8 Sandbox: From Compiler Correctness to Runtime Containment
Samuel GruetterGruetter, Samuel ETH Zurich Foundational Verification of Running-Time Bounds for Interactive Programs Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the RocqPL-track
Yawen GuanGuan, Yawen EPFLSwitzerland Precise Reasoning about Container-Internal Pointers with Logical Pinning Tracking Dynamically Bound Variable Dependencies
Zhichao GuanGuan, Zhichao Peking University Inferring Typing Rules for Contextual Sugars
Roberto GuancialeGuanciale, Roberto KTH Royal Institute of TechnologySweden Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Marco GuarnieriGuarnieri, Marco IMDEA Software InstituteSpain Committee Member in Steering Committee within the PriSC-track
Massin GuerdiGuerdi, Massin Ludwig-Maximilians-Universität MünchenGermany A Lambda-Superposition Tactic for Isabelle/HOL
Simon GuilloudGuilloud, Simon EPFLSwitzerland Committee Member in Program Committee within the VMCAI-track
Rui GuoGuo, Rui Zhejiang Sci-Tech UniversityChina A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamical Models
Ashutosh GuptaGupta, Ashutosh Committee Member in Program Committee within the VMCAI-track
Gopal GuptaGupta, Gopal The University of Texas at Dallas Interpretable Configuration Optimization for Static Program Verification via Rule-Based and Counterfactual Reasoning REGAL: Extracting implicit rules in text using LLMs with logic program feedback Committee Member in Program Committee within the PADL-track
Arie GurfinkelGurfinkel, Arie University of WaterlooCanada Committee Member in Program Committee within the POPL -track
Armaël GuéneauGuéneau, Armaël Université Paris-Saclay - CNRS - ENS Paris-Saclay - InriaFrance Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
Lennard GäherGäher, Lennard MPI-SWSGermany Building Blocks for Step-Indexed Program Logics
H Thomas HaasHaas, Thomas TU BraunschweigGermany Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
Darion HaaseHaase, Darion RWTH Aachen University Diagnostics in Probabilistic Program Verification
Matthew HagueHague, Matthew Royal Holloway University of LondonUnited Kingdom General Decidability Results for Systems with Continuous Counters Committee Member in Program Committee within the POPL -track
Michael HanusHanus, Michael Kiel UniversityGermany Declarative Programming: Efficient and reliable programming with human intelligence (Invited Talk) Committee Member in Program Committee within the PADL-track
Russ HarmerHarmer, Russ CNRSFrance Adhesive Category Theory for Graph Rewriting in Rocq
Robert HarperHarper, Robert Carnegie Mellon UniversityUnited States Abstraction Functions as Types Mechanizing Synthetic Tait Computability in Istari
Michael HartHart, Michael Queen's University Belfast Efficient Parallel Compilation and Profiling of Quantum Circuits at Large Scales
Arnd HartmannsHartmanns, Arnd University of TwenteNetherlands Probabilistic Verification for Modular Network-on-Chip Systems
Philipp G. HaselwarterHaselwarter, Philipp G. Aarhus UniversityDenmark Verifying Probabilistic Programs Using Separation Logic
Jakub HavlíkHavlík, Jakub Brno University of Technology Verifying Repeat-Until-Success Circuits with AutoQ
Chris HawblitzelHawblitzel, Chris Microsoft ResearchUnited States Tunable Automation in Automated Program Verification
Amaury HayatHayat, Amaury Ecole nationale des Ponts et ChausséesFrance TBA
Sina HazratpourHazratpour, Sina Johns Hopkins University A Certifying Proof Assistant for Synthetic Mathematics in Lean
Loic HelouetHelouet, Loic INRIAFrance Reachability in multi-agent transfer systems
Ludovic HenrioHenrio, Ludovic University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIPFrance Layers of Confluence for Actors
Yann HerklotzHerklotz, Yann EPFLSwitzerland Towards composable proofs of cache coherence protocols Committee Member in Program Committee within the Dafny-track
Manuel HermenegildoHermenegildo, Manuel Technical University of Madrid (UPM) and IMDEA Software InstituteSpain Multi-Configurable Search Rules in Prolog and Application to Testing
Roland HerrmannHerrmann, Roland University of Regensburg Verification of E-Voting Algorithms in Dafny
Chris HeunenHeunen, Chris University of EdinburghUnited Kingdom Quantum Circuits Are Just a Phase Hadamard-Pi: Equational Quantum Programming One rig to control them all Committee Member in Program Committee within the PLanQC-track
Brandon HewerHewer, Brandon Quotient Polymorphism
Michal HečkoHečko, Michal Brno University of TechnologyCzechia Parameterized Verification of Quantum Circuits Committee Member in Artifact Evaluation Committee within the VMCAI-track
Soichiro HidakaHidaka, Soichiro Hosei UniversityJapan Incrementalizing Haskell implementation of Putback-based Bidirectional Transformation Language BiGUL (Short Paper)
Kesha HietalaHietala, Kesha Sandia National LaboratoriesUnited States Committee Member in Program Committee within the PLanQC-track
Jonas Kastberg HinrichsenHinrichsen, Jonas Kastberg Aalborg UniversityDenmark Committee Member in Program Committee within the POPL -track Building Blocks for Step-Indexed Program Logics
Kengo HirataHirata, Kengo University of EdinburghUnited Kingdom RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
Andrew K. HirschHirsch, Andrew K. University at Buffalo, SUNYUnited States PLMW Co-Chair in Organizing Committee for POPL 2026 Committee Member in Organizing Committee within the PLMW @ POPL-track
Florent HivertHivert, Florent Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA Certifying the decidability of the word problem in monoids at large Committee Member in Program Committee within the CPP-track
Shing Hin HoHo, Shing Hin Imperial College LondonUnited Kingdom Bayesian Separation Logic
George HodgkinsHodgkins, George University of ColoradoUnited States A Verified High-Performance Composable Object Library for Remote Direct Memory Access
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
Jana HofmannHofmann, Jana Microsoft Azure ResearchUnited Kingdom Committee Member in Program Committee within the PriSC-track
Steven HoltzenHoltzen, Steven Northeastern UniversityUnited States Committee Member in Steering Committee within the LAFI-track
Lukáš HolíkHolík, Lukáš Brno University of Technology; Aalborg UniversityCzechia Parameterized Verification of Quantum Circuits Committee Member in Program Committee within the VMCAI-track
Chih-Duo HongHong, Chih-Duo National Chengchi UniversityTaiwan Committee Member in Program Committee within the VMCAI-track
Naohiko HoshinoHoshino, Naohiko Sojo UniversityJapan Compiling Quantum Lambda-Terms into Circuits via the Geometry of Interaction
Johannes HostertHostert, Johannes ETH ZurichSwitzerland Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany Committee Member in Steering Committee within the CPP-track Committee Member in Steering Committee within the PriSC-track
Raymond HuHu, Raymond Queen Mary University of LondonUnited Kingdom Welterweight Go: Boxing, Structural Subtyping, and Generics
Zhenjiang HuHu, Zhenjiang Peking UniversityChina Committee Member in Program Committee within the POPL -track Inferring Typing Rules for Contextual Sugars Committee Member in Program Committee within the PEPM-track
Joseph HuaHua, Joseph Carnegie Mellon University A Certifying Proof Assistant for Synthetic Mathematics in Lean
Qifan HuangHuang, Qifan Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of SciencesChina Committee Member in Artifact Evaluation Committee within the VMCAI-track
Yulong HuangHuang, Yulong University of CambridgeUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Simon HudonHudon, Simon SkyLabs AI Verification of Templated Code in C++
David HudákHudák, David Brno University of Technology Committee Member in Artifact Evaluation Committee within the VMCAI-track
Joffrey HuguetHuguet, Joffrey AdaCoreFrance Managing the Proof Context in SPARK
Kees HuizingHuizing, Kees Eindhoven University of Technology Formal Verification of Minimax Algorithms
Mathieu HuotHuot, Mathieu MIT Probabilistic Programming with Vectorized Programmable Inference
Chung-Kil HurHur, Chung-Kil Seoul National UniversitySouth Korea Coco: Corecursion with Compositional Heterogeneous Productivity Committee Member in Program Committee within the CPP-track
Graham HuttonHutton, Graham University of NottinghamUnited Kingdom Quotient Polymorphism Committee Member in Program Committee within the POPL -track
Hans HüttelHüttel, Hans Department of Computer Science, Aalborg UniversityDenmark Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
I Daniela InclezanInclezan, Daniela Miami University, USA Committee Member in Program Committee within the PADL-track
Apoorv IngleIngle, Apoorv University of IowaUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Verbauwhede IngridIngrid, Verbauwhede KU LeuvenBelgium Committee Member in Program Committee within the PriSC-track
Alex IonescuIonescu, Alex Chalmers University of Technology and University of Gothenburg Towards Lightweight and Efficient Choreographic Cloud Services
Omri IsacIsac, Omri The Hebrew University of JerusalemIsrael Proof Minimization in Neural Network Verification
Shachar ItzhakyItzhaky, Shachar TechnionIsrael Enhancing Symbolic Execution with Machine-Checked Safety Proofs
Yusuke IzawaIzawa, Yusuke Tokyo Metropolitan UniversityJapan Committee Member in Program Committee within the PEPM-track
Yusuf IzmirliogluIzmirlioglu, Yusuf University of Roehampton United Kingdom Committee Member in Program Committee within the PADL-track
Joe IzraelevitzIzraelevitz, Joe University of Colorodo Boulder A Verified High-Performance Composable Object Library for Remote Direct Memory Access
Noa IzsakIzsak, Noa CISPA Helmholtz Center for Information Security, GermanyGermany Atomic Gliders and Cellular Automata as Language Generators
J Suresh JagannathanJagannathan, Suresh Purdue UniversityUnited States PC Chair in Organizing Committee for POPL 2026 Program Chair in Program Committee within the POPL -track On grant writing Speaker in Speakers and Panelists within the RTFM-track
Georges-Axel JaloyanJaloyan, Georges-Axel Ministère de l'Économie et des FinancesFrance Committee Member in Program Committee within the Dafny-track
Ara JamalzadehJamalzadeh, Ara University of TorontoCanada Extensible Data Types with Ad-Hoc Polymorphism
Patrick JanoschekJanoschek, Patrick University of Regensburg Verification of E-Voting Algorithms in Dafny
Thomas P. JensenJensen, Thomas P. INRIA Rennes Co-chair in Organizing Committee within the VMCAI-track Co-chair in Program Committee within the VMCAI-track
Johan JeuringJeuring, Johan Utrecht UniversityNetherlands Hole Refinements for Polymorphic Type-and-Example Driven Synthesis
Ruyi JiJi, Ruyi Peking UniversityChina Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
Shengyi JiangJiang, Shengyi The University of Hong KongChina Local Contextual Type Inference
Zhan JINGJING, Zhan Shanghai Jiao Tong University Abstract VCG: Tie-breaking rules in VCG mechanism design
Evan JohnsonJohnson, Evan NYUUnited States Committee Member in Program Committee within the PriSC-track
Eddie JonesJones, Eddie University of BristolUnited Kingdom Domain-Theoretic Semantics for Functional Logic Programming Committee Member in Program Committee within the POPL -track
Sung-Shik JongmansJongmans, Sung-Shik University of GroningenNetherlands A Synthetic Reconstruction of Multiparty Session Types
Jacques-Henri JourdanJourdan, Jacques-Henri CNR, LMFFrance Creusot: Formal verification of Rust programs Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
Jacques-Henri JourdanJourdan, Jacques-Henri Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles Committee Member in Program Committee within the Dafny-track
Pierre JouvelotJouvelot, Pierre Abstract VCG: Tie-breaking rules in VCG mechanism design
Ralf JungJung, Ralf ETH ZurichSwitzerland Student Research Competition Co-Chair in Organizing Committee for POPL 2026 Miri: Practical Undefined Behavior Detection for Rust Student Research Competition Co-Chair in Selection Committee within the POPL Student Research Competition-track
Sebastian JungesJunges, Sebastian Committee Member in Program Committee within the VMCAI-track
Jaakko JärviJärvi, Jaakko University of TurkuFinland Lambda JS à la Carte
K Robin KaarsgaardKaarsgaard, Robin University of Southern DenmarkDenmark Hadamard-Pi: Equational Quantum Programming One rig to control them all
David M. KahnKahn, David M. Carnegie Mellon UniversityUnited States Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
Konstantinos KallasKallas, Konstantinos University of California, Los AngelesUnited States Analyzing Shell Scripts
David Kaloper-MeršinjakKaloper-Meršinjak, David University of CambridgeUnited Kingdom Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
Adharsh KamathKamath, Adharsh UIUCUnited States Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation
Yukiyoshi KameyamaKameyama, Yukiyoshi University of TsukubaJapan Welcome Committee Member in Organizing Committee within the PEPM-track
Benjamin Lucien KaminskiKaminski, Benjamin Lucien Saarland University; University College LondonGermany Committee Member in Program Committee within the TPSA-track
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories
Shuanglong KanKan, Shuanglong Barkhausen Institute, DresdenGermany Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis
Johannes KanigKanig, Johannes AdaCoreFrance Managing the Proof Context in SPARK
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Diagnostics in Probabilistic Program Verification
Hiroyuki KatsuraKatsura, Hiroyuki University of Cambridge Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
Guy KatzKatz, Guy The Hebrew University of JerusalemIsrael Proof Minimization in Neural Network Verification
Ryan KavanaghKavanagh, Ryan Université du Québec à MontréalCanada Rocq CARVe-ing: A Library for Substructural Meta-Theory
Alex KavvosKavvos, Alex University of BristolUnited Kingdom Domain-Theoretic Semantics for Functional Logic Programming
Jingyu KeKe, Jingyu Shanghai Jiao Tong UniversityChina Piecewise Analysis of Probabilistic Programs via k-Induction
Ariel E. KellisonKellison, Ariel E. Cornell UniversityUnited States TBD
George KenisonKenison, George Liverpool John Moores University Determination Problems for Orbit Closures and Matrix Groups
Dominic KennedyKennedy, Dominic University of UtahUnited States Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
Marie KerjeanKerjean, Marie CNRS, Université Sorbonne Paris NordFrance Session Chair of Formalized mathematics (part of CPP) Committee Member in Program Committee within the CPP-track
Delia KesnerKesner, Delia Université Paris Cité - CNRS - IRIFFrance Committee Member in Program Committee within the POPL -track
Steven KeuchelKeuchel, Steven KU LeuvenBelgium Committee Member in Program Committee within the PriSC-track
Ayrat KhalimovKhalimov, Ayrat Committee Member in Artifact Evaluation Committee within the VMCAI-track
Harun KhanKhan, Harun Stanford University Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
Jam Kabeer Ali KhanKhan, Jam Kabeer Ali Max Planck Institute for Security and Privacy (MPI-SP); The University of Hong Kong (HKU)Germany Traq: Estimating the Quantum Cost of Classical Programs
Donnacha Oisín KidneyKidney, Donnacha Oisín Imperial College LondonUnited Kingdom Hyperfunctions: Communicating Continuations
Jaewoo KimKim, Jaewoo Seoul National University Coco: Corecursion with Compositional Heterogeneous Productivity
Yonghyun KimKim, Yonghyun MPI-SP Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Benjamin KimockKimock, Benjamin Lansweeper NVUnited States Miri: Practical Undefined Behavior Detection for Rust
Zachary KincaidKincaid, Zachary Princeton UniversityUnited States Network Change Validation with Relational NetKAT Context-Free-Language Reachability for Almost-Commuting Transition Systems
Oleg KiselyovKiselyov, Oleg Tohoku UniversityJapan Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
Gerwin KleinKlein, Gerwin Proofcraft and UNSW SydneyAustralia Committee Member in Steering Committee within the CPP-track
Dominik KlumppKlumpp, Dominik LIX - CNRS - École Polytechnique; University of FreiburgFrance The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
Åsmund Aqissiaq Arild KløvstadKløvstad, Åsmund Aqissiaq Arild University of Oslo (UiO) Layers of Confluence for Actors
Naoki KobayashiKobayashi, Naoki University of TokyoJapan Committee Member in Program Committee within the PEPM-track
Thomas KoehlerKoehler, Thomas ICube Lab - CNRS - Université de StrasbourgFrance Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
Jan KofroňKofroň, Jan Charles UniversityCzechia Committee Member in Program Committee within the VMCAI-track
Michalis KokologiannakisKokologiannakis, Michalis ETH ZurichSwitzerland Committee Member in Program Committee within the POPL -track
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University and Southampton UniversityUnited Kingdom Committee Member in Program Committee within the POPL -track
Soonho KongKong, Soonho Amazon Web Services ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
Konrad KordingKording, Konrad University of PennsylvaniaUnited States Compiling to Linear Neurons
Joomy KorkutKorkut, Joomy BloombergUnited States A Rose Tree is Blooming (Proof Pearl) Crane Lowers Rocq Safely into C++ Committee Member in Program Committee within the PriSC-track
Ivana KostadinovicKostadinovic, Ivana University of Regensburg Verification of E-Voting Algorithms in Dafny
Dejan KosticKostic, Dejan KTH Royal Institute of Technology Toward Automated, Contamination-free Dafny Benchmark Generation
Angeliki Koutsoukou-ArgyrakiKoutsoukou-Argyraki, Angeliki Royal Holloway, University of LondonUnited Kingdom Committee Member in Program Committee within the CPP-track
Laura KovacsKovacs, Laura Vienna University of Technology (TU Wien)Austria Associate Chair in Program Committee within the POPL -track
András KovácsKovács, András University of Gothenburg and Chalmers University of TechnologySweden Canonicity for Indexed Inductive-Recursive Types Observing Definitional Equality
Maite KramarzKramarz, Maite University of TorontoCanada Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Klaus KraßnitzerKraßnitzer, Klaus ISTA Committee Member in Artifact Evaluation Committee within the VMCAI-track
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands A Relational Separation Logic for Effect Handlers Associate Chair in Program Committee within the POPL -track A Recipe for Modular Verification of Generic Tree Traversals Building Blocks for Step-Indexed Program Logics
Shankaranarayanan KrishnaKrishna, Shankaranarayanan IIT BombayIndia Committee Member in Program Committee within the POPL -track
Shriram KrishnamurthiKrishnamurthi, Shriram Brown UniversityUnited States A Guided Tour through Oxidized OCaml
Neel KrishnaswamiKrishnaswami, Neel University of CambridgeUnited Kingdom Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
Sean Kristian Remond HarboKristian Remond Harbo, Sean Department of Computer Science, Aalborg University Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
Mathias Faber KristiansenKristiansen, Mathias Faber IT University of Copenhagen Property-Based Testing for Asynchronous Functional Reactive Programming Using Linear Temporal Logic
Ondřej KubánekKubánek, Ondřej Chalmers University of TechnologySweden Normalisation for First-Class Universe Levels
Jure KukovecKukovec, Jure Beneficial AI Foundation A benchmark for vericoding: formally verified program synthesis
K Narayan KumarKumar, K Narayan Chennai Mathematical InstituteIndia Parametrised Verification of Intel-x86 Programs
Viktor KunčakKunčak, Viktor EPFL, SwitzerlandSwitzerland Committee Member in Steering Committee within the VMCAI-track
Vitaly KurinKurin, Vitaly Neapolis University PafosCyprus Foundational Multi-Modal Program Verifiers Velvet: A Multi-Modal Verifier for Effectful Programs
Max KurzeKurze, Max Barkhausen Institut Scalable Type Inference for Intrinsically-Typed Binders
L Alfons LaarmanLaarman, Alfons Leiden UniversityNetherlands Committee Member in Program Committee within the VMCAI-track
Vincent LafeychineLafeychine, Vincent Université Paris-Saclay Creusot: Formal verification of Rust programs
Ambroise LafontLafont, Ambroise Ecole PolytechniqueFrance Committee Member in Program Committee within the POPL -track
Miriam Lagunes-RochinLagunes-Rochin, Miriam University of FreiburgGermany The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
Ori LahavLahav, Ori Tel Aviv UniversityIsrael Committee Member in Program Committee within the POPL -track
Christopher LamLam, Christopher University of Illinois at Urbana-ChampaignUnited States Video Co-Chair in Organizing Committee for POPL 2026
Thomas LamiauxLamiaux, Thomas Nantes Université, Inria Nested Inductive Types for Rocq and Lean
Leonidas LampropoulosLampropoulos, Leonidas University of Maryland, College ParkGreece Committee Member in Selection Committee within the POPL Student Research Competition-track
Julien LangeLange, Julien Royal Holloway University of LondonUnited Kingdom A Modular Static Cost Analysis for GPU Warp-Level Parallelism Welterweight Go: Boxing, Structural Subtyping, and Generics
Dominique Larchey-WendlingLarchey-Wendling, Dominique Université de Lorraine, CNRS, LORIAFrance Bar Inductive Predicates for Constructive Algebra in Rocq
Andrea LarettoLaretto, Andrea Tallinn University of TechnologyEstonia Di- is for Directed: First-Order Directed Type Theory via Dinaturality
Pascal LasnierLasnier, Pascal University of Cambridge Brack: A Verified Compiler for Scheme via CakeML
Pascal Y. LasnierLasnier, Pascal Y. A One-Pass CPS Transform with Simulation on the Nose
Andrea LattuadaLattuada, Andrea VMware ResearchSwitzerland Tunable Automation in Automated Program Verification
Nils LauermannLauermann, Nils University of CambridgeUnited Kingdom ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
Andrew LawrenceLawrence, Andrew Siemens Mobility Formal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq
Thierry LecomteLecomte, Thierry CLEARSYFrance Committee Member in Program Committee within the Dafny-track
Doyoon LeeLee, Doyoon Seoul National University Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling
Jaeseong LeeLee, Jaeseong The University of Texas at Dallas Interpretable Configuration Optimization for Static Program Verification via Rule-Based and Counterfactual Reasoning
Jay LeeLee, Jay Seoul National UniversitySouth Korea Retargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
Michael LeeLee, Michael University of Cambridge, UK Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
Nian-Ze LeeLee, Nian-Ze National Taiwan University, TaiwanTaiwan Committee Member in Program Committee within the VMCAI-track
Wonyeol LeeLee, Wonyeol POSTECHSouth Korea Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation Committee Member in Program Committee within the POPL -track
Woosuk LeeLee, Woosuk Hanyang UniversitySouth Korea Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling
Peter Lefanu LumsdaineLefanu Lumsdaine, Peter Stockholm UniversitySweden Committee Member in Program Committee within the CPP-track
Engel LefaucheuxLefaucheux, Engel Université de Lorraine; CNRS; Inria; LORIAFrance Reachability in multi-agent transfer systems
K. Rustan M. LeinoLeino, K. Rustan M. AmazonUnited States The Design of an Interactive Proof Mode for Dafny Committee Member in Steering Committee Chairs within the Dafny-track
Matthieu LemerreLemerre, Matthieu Université Paris-Saclay - CEA ListFrance Committee Member in Program Committee within the VMCAI-track
Louis LemonnierLemonnier, Louis University of Edinburgh Quantum Circuits Are Just a Phase One rig to control them all
Ondřej LengálLengál, Ondřej Brno University of TechnologyCzechia Parameterized Verification of Quantum Circuits Co-chair in Organizing Committee within the VMCAI-track Co-chair in Program Committee within the VMCAI-track Verifying Repeat-Until-Success Circuits with AutoQ
Meven Lennon-BertrandLennon-Bertrand, Meven Inria – Université Paris CitéFrance AdapTT: Functoriality for Dependent Type Casts Verifying Dependent Type-checkers
Nicola LeoneLeone, Nicola University of Calabria, Italy Solving hard combinatorial optimization problems with PyQASP
Yann LerayLeray, Yann Nantes Université; InriaFrance Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally
Jérôme LerouxLeroux, Jérôme LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, FranceFrance Committee Member in Program Committee within the VMCAI-track Committee Member in Artifact Evaluation Committee within the VMCAI-track
Xavier LeroyLeroy, Xavier Collège de France - PSL UniversityFrance A Lazy, Concurrent Convertibility Checker
Dorian LesbreLesbre, Dorian Université Paris-Saclay - CEA LISTFrance Committee Member in Artifact Evaluation Committee within the VMCAI-track
Michael LeuschelLeuschel, Michael HHUGermany Using Prolog to Translate Set Theory and B to SAT
Michael LeuschelLeuschel, Michael University of Düsseldorf Committee Member in Program Committee within the PADL-track
Paul Blain LevyLevy, Paul Blain University of BirminghamUnited Kingdom What Is a Monoid?
Alexander K. LewLew, Alexander K. Yale UniversityUnited States Probabilistic Programming with Vectorized Programmable Inference Committee Member in Organizing Committee within the LAFI-track Co-chair in Program Committee within the LAFI-track
Marco LewisLewis, Marco InriaFrance Finding Photonics Circuits via δ-weakening SMT
Celia Mengyue LiLi, Celia Mengyue University of BristolUnited Kingdom A Complementary Approach to Incorrectness Typing Domain-Theoretic Semantics for Functional Logic Programming
Gushu LiLi, Gushu University of PennsylvaniaUnited States Committee Member in Program Committee within the PLanQC-track
Runming LiLi, Runming Carnegie Mellon UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment Abstraction Functions as Types Mechanizing Synthetic Tait Computability in Istari
Thea LiLi, Thea Inria, LMF, ENS Paris-Saclay, Université Paris-Saclay Quantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic Approach
Xuyang LiLi, Xuyang Purdue University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yang LiLi, Yang Zhejiang Sci-Tech UniversityChina A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamical Models
Yong LiLi, Yong Institute of Software, Chinese Academy of SciencesChina SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation Co-chair in Artifact Evaluation Committee within the VMCAI-track
Yue LiLi, Yue Nanjing UniversityChina ChiSA: Static Analysis for Lightweight Chisel Verification
Steven LibbyLibby, Steven University of Portland A Functional Logic Perspective on Indentation-Sensitive Parsing (Short Paper)
Daniel R. LicataLicata, Daniel R. Wesleyan UniversityUnited States Committee Member in Program Committee within the POPL -track
Jack Liell-CockLiell-Cock, Jack University of OxfordUnited Kingdom An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories The Relative Monadic Metalanguage
Hyoungjin LimLim, Hyoungjin KAIST Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
Sangho LimLim, Sangho KAISTSouth Korea Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
Anthony Widjaja LinLin, Anthony Widjaja TU Kaiserslautern; MPI-SWSGermany Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis Understanding Transformers through the Lens of Logic and Automata
Jyun-Ao LinLin, Jyun-Ao National Taipei University of TechnologyTaiwan Parameterized Verification of Quantum Circuits Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the VMCAI-track Verifying Repeat-Until-Success Circuits with AutoQ
Shaowei LinLin, Shaowei Beneficial AI Foundation A benchmark for vericoding: formally verified program synthesis
Wang LinLin, Wang A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamical Models
Sam LindleyLindley, Sam University of EdinburghUnited Kingdom An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories Rows and Capabilities as Modal Effects
Andreas LindnerLindner, Andreas Uppsala universitetSweden Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Cyrus LiuLiu, Cyrus Samsung SemiconductorUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Junyi LiuLiu, Junyi University of Maryland A Pulse-Level DSL for Real-Time Quantum Control with Hardware Compilation and Emulation
Tsung-Han LiuLiu, Tsung-Han EPFL Tracking Dynamically Bound Variable Dependencies
Y. Annie LiuLiu, Y. Annie Stony Brook UniversityUnited States Committee Member in Program Committee within the PADL-track
Yiyun LiuLiu, Yiyun University of PennsylvaniaUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach
Zengyu LiuLiu, Zengyu National University of Defense TechnologyChina Committee Member in Artifact Evaluation Committee within the VMCAI-track
Zongyuan LiuLiu, Zongyuan Aarhus UniversityDenmark ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
Fang-Yi LoLo, Fang-Yi Academia Sinica Verifying Repeat-Until-Success Circuits with AutoQ
Andrés Lomelí GarduñoLomelí Garduño, Andrés Huawei Dresden Research CenterGermany Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
Fosco LoregianLoregian, Fosco Tallinn University of TechnologyEstonia Di- is for Directed: First-Order Directed Type Theory via Dinaturality
Cade LuekerLueker, Cade University of Colorado Boulder Towards Cumulative Abstract Semantics via Handlers (Short Paper)
Matthew LutzeLutze, Matthew Aarhus University Committee Member in Program Committee within the WITS-track
Jean-Christophe LéchenetLéchenet, Jean-Christophe Université Côte d’Azur, Inria Mechanized Dominator Tree Certification
Pedro López-GarcíaLópez-García, Pedro IMDEA Software Institute Multi-Configurable Search Rules in Prolog and Application to Testing
M Lydie MabilMabil, Lydie InriaFrance Local Arrangements Co-Chair in Organizing Committee for POPL 2026
Dougal MaclaurinMaclaurin, Dougal Committee Member in Steering Committee within the LAFI-track
Benedikt MaderbacherMaderbacher, Benedikt Graz University of TechnologyAustria Parameterized Infinite-State Reactive Synthesis
Anil MadhavapeddyMadhavapeddy, Anil University of Cambridge, UKUnited Kingdom A Guided Tour through Oxidized OCaml
Mark MadlerMadler, Mark University of ColoradoUnited States A Verified High-Performance Composable Object Library for Remote Direct Memory Access
Ratul MahajanMahajan, Ratul University of Washington, Intentionet Network Change Validation with Relational NetKAT
Assia MahboubiMahboubi, Assia INRIAFrance Certifying the decidability of the word problem in monoids at large
Kenji MaillardMaillard, Kenji InriaFrance Bounded Sort Polymorphism with Elimination Constraints AdapTT: Functoriality for Dependent Type Casts Committee Member in Program Committee within the POPL -track Committee Member in Selection Committee within the POPL Student Research Competition-track Sulfur: Substitution Generation using a Logical Framework
Samson MainMain, Samson University of BristolUnited Kingdom Domain-Theoretic Semantics for Functional Logic Programming
Geoffrey MainlandMainland, Geoffrey Drexel UniversityUnited States Committee Member in Program Committee within the PEPM-track
Rupak MajumdarMajumdar, Rupak MPI-SWSGermany General Decidability Results for Systems with Continuous Counters Verifying Almost-Sure Termination for Randomized Distributed Algorithms
Petar MaksimovićMaksimović, Petar Nethermind; Imperial College LondonUnited Kingdom Committee Member in Program Committee within the TPSA-track
Dhruv MakwanaMakwana, Dhruv University of Cambridge Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
Gregory MalechaMalecha, Gregory Skylabs AIUnited States Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic Recursive Mutexes in Separation Logic Verification of Templated Code in C++
Éléonore MangelMangel, Éléonore Univ. Paris Cité - CNRS - InriaFrance Classical Notions of Computation and the Hasegawa-Thielecke Theorem
Matteo ManighettiManighetti, Matteo Inria & École PolytechniqueFrance A Correct-by-Construction Checker for Validation of Railway Data
Vikash K. MansinghkaMansinghka, Vikash K. Massachusetts Institute of TechnologyUnited States Probabilistic Programming with Vectorized Programmable Inference Committee Member in Program Committee within the POPL -track
William ManskyMansky, William University of Illinois ChicagoUnited States Recursive Mutexes in Separation Logic
Claude MarchéMarché, Claude Inria Saclay & Université Paris-Saclay A Correct-by-Construction Checker for Validation of Railway Data
Virgil MarionneauMarionneau, Virgil ENS Rennes Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic
Jonathan MarriottMarriott, Jonathan University of BristolUnited Kingdom Domain-Theoretic Semantics for Functional Logic Programming
Chris MartensMartens, Chris Northeastern UniversityUnited States Committee Member in Program Committee within the POPL -track Epistemic Logic for Polyglots (Short Paper)
Tomaz MascarenhasMascarenhas, Tomaz Universidade Federal de Minas Gerais Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
Isabella MastroeniMastroeni, Isabella University of VeronaItaly Committee Member in Program Committee within the VMCAI-track
Cristina MatacheMatache, Cristina University of Edinburgh An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories
Christoph MathejaMatheja, Christoph DTUDenmark Committee Member in Program Committee within the POPL -track
George MatheosMatheos, George Massachusetts Institute of TechnologyUnited States Probabilistic Programming with Vectorized Programmable Inference
Umang MathurMathur, Umang National University of SingaporeSingapore Counting and Sampling Traces in Regular Languages The Complexity of Testing Message-Passing Concurrency
Yusuke MatsushitaMatsushita, Yusuke Kyoto UniversityJapan RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
Nicolas MazzocchiMazzocchi, Nicolas Slovak University of Technology in BratislavaSlovakia Committee Member in Program Committee within the VMCAI-track
Giuseppe MazzottaMazzotta, Giuseppe University of CalabriaItaly Solving hard combinatorial optimization problems with PyQASP Committee Member in Program Committee within the PADL-track
John McAllisterMcAllister, John Queen's University Belfast Efficient Parallel Compilation and Profiling of Quantum Circuits at Large Scales
Conor McBrideMcBride, Conor Committee Member in Program Committee within the WITS-track
Christopher McNallyMcNally, Christopher Massachusetts Institute of TechnologyUnited States Quantum Circuits Are Just a Phase
Kuldeep S. MeelMeel, Kuldeep S. University of TorontoCanada Counting and Sampling Traces in Regular Languages
Jingyi MeiMei, Jingyi Leiden UniversityNetherlands Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Artifact Evaluation Committee within the VMCAI-track
Antero MejrMejr, Antero Tufts UniversityUnited States DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
Stephen MellMell, Stephen Student Volunteer Co-Chair in Organizing Committee for POPL 2026
Paul-André MellièsMelliès, Paul-André Univ. Paris Cité - CNRS - InriaFrance Classical Notions of Computation and the Hasegawa-Thielecke Theorem
Guillaume MelquiondMelquiond, Guillaume Université Paris-Saclay - CNRS - ENS Paris-Saclay - InriaFrance Certifying the decidability of the word problem in monoids at large
Kayvan MemarianMemarian, Kayvan University of Cambridge Committee Member in Program Committee within the POPL -track Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
Alexandra MendesMendes, Alexandra Faculty of Engineering, University of Porto & INESC TECPortugal Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs Committee Member in Program Committee within the PADL-track
Junjie MengMeng, Junjie School of Computer Science and Technology, Tongji UniversityChina SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation
Ștefan MercașMercaș, Ștefan Alexandru Ioan Cuza University, Iasi, Romania The Design of an Interactive Proof Mode for Dafny
Rodrigo MesquitaMesquita, Rodrigo Well-Typed LLPPortugal Lazy Linearity for a Core Functional Language
Roland MeyerMeyer, Roland TU BraunschweigGermany Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models Oriented Metrics for Bottom-Up Enumerative Synthesis
Jairo Miguel Marulanda-GiraldoMiguel Marulanda-Giraldo, Jairo University of Southampton Formalizing a First-order Differentiable Logic with MathComp
Vincent MihalkovičMihalkovič, Vincent Mr Committee Member in Artifact Evaluation Committee within the VMCAI-track
Dale MillerMiller, Dale INRIA Saclay and LIX/Institut Polytechnique de ParisFrance Committee Member in Steering Committee within the CPP-track A positive perspective on term representation (Invited Talk)
Antoine MinéMiné, Antoine Sorbonne UniversitéFrance Committee Member in Program Committee within the VMCAI-track Towards automatic functional correctness in the Mopsa static analyzer
Sasa MisailovicMisailovic, Sasa University of Illinois at Urbana-ChampaignUnited States Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation
Haruto MishinaMishina, Haruto Waseda University Graph Rewriting Language as a Platform for Quantum Diagrammatic Calculi
James MitchellMitchell, James St Andrews University Certifying the decidability of the word problem in monoids at large
Abdalrhman MohamedMohamed, Abdalrhman Stanford University Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
Alexandre MoineMoine, Alexandre New York UniversityUnited States All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs TypeDis: A Type System for Disentanglement (TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection Committee Member in Program Committee within the VMCAI-track
Abtin MolaviMolavi, Abtin University of Wisconsin-Madison Generating Compilers for Qubit Mapping and Routing
Alberto MomiglianoMomigliano, Alberto Università degli Studi di Milano Rocq CARVe-ing: A Library for Substructural Meta-Theory
Raphaël MonatMonat, Raphaël Inria and University of LilleFrance Try-Mopsa: Relational Static Analysis in Your Pocket Towards automatic functional correctness in the Mopsa static analyzer
Benoît MontaguMontagu, Benoît InriaFrance Industrial Relations Co-Chair in Organizing Committee for POPL 2026 Committee Member in Program Committee within the VMCAI-track
Jane MooreMoore, Jane Queen's University Belfast Efficient Parallel Compilation and Profiling of Quantum Circuits at Large Scales
José MoralesMorales, José IMDEA Software InstituteSpain Multi-Configurable Search Rules in Prolog and Application to Testing Committee Member in Program Committee within the PADL-track
Andreia MordidoMordido, Andreia University of LisbonPortugal Types as grammars
Harshit Jitendra MotwaniMotwani, Harshit Jitendra MPI-SWSGermany Verifying Almost-Sure Termination for Randomized Distributed Algorithms
Naïm Moussaoui RemilMoussaoui Remil, Naïm Inria & ENS \| PSL, Paris, FranceFrance Termination Resilience Static Analysis
Yannick MoyMoy, Yannick ANSSIFrance Committee Member in Program Committee Chairs within the Dafny-track
Sayan MukherjeeMukherjee, Sayan Univ Rennes, Inria, CNRS, IRISA, France Committee Member in Artifact Evaluation Committee within the VMCAI-track
Niek MullenersMulleners, Niek Utrecht UniversityNetherlands Hole Refinements for Polymorphic Type-and-Example Driven Synthesis
Guillaume Munch-MaccagnoniMunch-Maccagnoni, Guillaume Inria - LS2N - CNRSFrance Classical Notions of Computation and the Hasegawa-Thielecke Theorem S4 modal sequent calculus as intermediate logic and intermediate language (Short Paper)
Adithya MuraliMurali, Adithya University of WisconsinUnited States Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions Committee Member in Program Committee within the POPL -track
Eduardo Sánchez MuñozMuñoz, Eduardo Sánchez UnaffiliatedSpain Miri: Practical Undefined Behavior Detection for Rust
Andrew MyersMyers, Andrew Cornell University Committee Member in Steering Committee within the PriSC-track
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology Verified VCG and Verified Compiler for Dafny Brack: A Verified Compiler for Scheme via CakeML A One-Pass CPS Transform with Simulation on the Nose Committee Member in Program Committee within the PADL-track
Sibylle MöhleMöhle, Sibylle University of Regensburg Verification of E-Voting Algorithms in Dafny
Lasse MøldrupMøldrup, Lasse Aarhus UniversityDenmark The Complexity of Testing Message-Passing Concurrency
Niklas MückMück, Niklas MPI-SWSGermany Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation
Markus Müller-OlmMüller-Olm, Markus University of MünsterGermany Committee Member in Program Committee within the POPL -track
N Shaan NagyNagy, Shaan University of California at San DiegoUnited States ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models
Niyousha NajmaeiNajmaei, Niyousha École PolytechniqueFrance From Semantics to Syntax: A Type Theory for Comprehension Categories
Keisuke NakanoNakano, Keisuke Tohoku UniversityJapan Committee Member in Program Committee within the PEPM-track
Yeonwoo NamNam, Yeonwoo Seoul National UniversitySouth Korea Coco: Corecursion with Compositional Heterogeneous Productivity
Kedar NamjoshiNamjoshi, Kedar Nokia Bell LabsUnited States Consistent Updates for Scalable Microservices
Aleksandar NanevskiNanevski, Aleksandar IMDEA Software InstituteSpain Committee Member in Program Committee within the POPL -track
Jorge A. NavasNavas, Jorge A. CertoraUnited States Committee Member in Program Committee within the VMCAI-track
Wojciech NawrockiNawrocki, Wojciech Carnegie Mellon UniversityUnited States A Certifying Proof Assistant for Synthetic Mathematics in Lean
Luca NegriniNegrini, Luca Ca’ Foscari University of VeniceItaly Committee Member in Program Committee within the VMCAI-track
Hamed NematiNemati, Hamed KTH Royal Institute of TechnologySweden Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Max S. NewNew, Max S. University of MichiganUnited States Committee Member in Selection Committee within the POPL Student Research Competition-track
Daniel NezamabadiNezamabadi, Daniel ETH ZurichGermany Verified VCG and Verified Compiler for Dafny
Kim NguyễnNguyễn, Kim Université Paris-SaclayFrance Committee Member in Program Committee within the POPL -track
Christian Emil NielsenNielsen, Christian Emil IT University of Copenhagen Property-Based Testing for Asynchronous Functional Reactive Programming Using Linear Temporal Logic
Tobias NipkowNipkow, Tobias Technische Universität München Committee Member in Steering Committee within the CPP-track
Fredrik Nordvall ForsbergNordvall Forsberg, Fredrik University of StrathclydeUnited Kingdom Can we formalise type theory intrinsically without any compromise? A case study in Cubical Agda
Paige Randall NorthNorth, Paige Randall Utrecht UniversityNetherlands From Semantics to Syntax: A Type Theory for Comprehension Categories Committee Member in Program Committee within the POPL -track Committee Member in Selection Committee within the POPL Student Research Competition-track
Filippo Alberto Edoardo Nuccio Mortarino Majno di CapriglioNuccio Mortarino Majno di Capriglio, Filippo Alberto Edoardo Inria, Université Jean Monnet Saint-ÉtienneFrance Session Chair of Formalized mathematics (part of CPP) Committee Member in Program Committee within the CPP-track
Andreas NuytsNuyts, Andreas KU Leuven, BelgiumBelgium Committee Member in Program Committee within the POPL -track
O Alistair O'BrienO'Brien, Alistair University of Cambridge Omnidirectional type inference for ML
Henrik ObackOback, Henrik University of Regensburg Verification of E-Voting Algorithms in Dafny
Ocan Sankur Ocan Sankur University of Rennes, France / Inria, France / CNRS, France / IRISA, FranceFrance Verification of Generic VHDL Designs and Their Translation to Rocq
Ana Oliveira Da CostaOliveira Da Costa, Ana IST Austria, AustriaAustria Committee Member in Artifact Evaluation Committee within the VMCAI-track
Bruno C. d. S. OliveiraOliveira, Bruno C. d. S. University of Hong KongChina Local Contextual Type Inference
Santiago Arranz OlmosOlmos, Santiago Arranz Max Planck Institute for Security and Privacy Committee Member in Program Committee within the PriSC-track
Jan OnderkaOnderka, Jan University of FreiburgGermany Input-based Three-Valued Abstraction Refinement
Klaus OstermannOstermann, Klaus University of TübingenGermany Committee Member in Program Committee within the POPL -track
P Michele PaganiPagani, Michele ENS LyonFrance JAX Autodiff from a Linear Logic Perspective Committee Member in Program Committee within the POPL -track
Karl PalmskogPalmskog, Karl KTH Royal Institute of TechnologySweden Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Jens PalsbergPalsberg, Jens University of California, Los Angeles (UCLA)United States Committee Member in Program Committee within the PLanQC-track
Pavel PanchekhaPanchekha, Pavel University of UtahUnited States Committee Member in Selection Committee within the POPL Student Research Competition-track
Luca PaparazzoPaparazzo, Luca Inria, IRISA, Université de RennesFrance Reachability in multi-agent transfer systems
Hugo PaquetPaquet, Hugo École Normale Supérieure, PSL University & INRIAFrance Committee Member in Organizing Committee within the LAFI-track Co-chair in Program Committee within the LAFI-track
Zoe ParaskevopoulouParaskevopoulou, Zoe National Technical University of AthensGreece Committee Member in Program Committee within the CPP-track
Lionel ParreauxParreaux, Lionel Hong Kong University of Science and TechnologyHong Kong SAR China The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PEPM-track Decoupling Resolution from Type Inference
Michele PasquaPasqua, Michele University of VeronaItaly Committee Member in Organizing Committee within the GiacoFest-track
Paul PataultPatault, Paul Université Paris-Saclay - Laboratoire de Méthodes Formelles France Explicit Abstraction Barrier for Autoactive Verification
Aurélie PatierPatier, Aurélie University of RennesFrance Local Arrangements Co-Chair in Organizing Committee for POPL 2026
Marco PatrignaniPatrignani, Marco University of TrentoItaly Committee Member in Program Committee within the POPL -track Committee Member in Steering Committee within the PriSC-track
Andreas PavlogiannisPavlogiannis, Andreas Aarhus UniversityDenmark The Complexity of Testing Message-Passing Concurrency
Jennifer PaykinPaykin, Jennifer University of VermontUnited States Qudit Quantum Programming with Projective Cliffords TBA Committee Member in Program Committee within the PLanQC-track
Anurudh PeduriPeduri, Anurudh Ruhr University BochumGermany Traq: Estimating the Quantum Cost of Classical Programs
Xuanyu PengPeng, Xuanyu University of California at San DiegoUnited States Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
Yuxiang PengPeng, Yuxiang Purdue UniversityUnited States A Pulse-Level DSL for Real-Time Quantum Control with Hardware Compilation and Emulation Committee Member in Program Committee within the PLanQC-track
Gijs PenningsPennings, Gijs Eindhoven University of Technology A systematic approach to "Well-founded recursion done right"
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
Lorenzo PerticonePerticone, Lorenzo Chalmers University of Technology, Gothenburg University, Sweden A Graded Modal Type Theory for Pulse Schedules
Basile PesinPesin, Basile Ecole Nationale de l'Aviation Civile (ENAC) Verifying Synchronous Dataflow Programs with SMTCoq
Roberto PettinauPettinau, Roberto Carl von Ossietzky Universität Oldenburg / University of Oldenburg Committee Member in Artifact Evaluation Committee within the VMCAI-track
Frank PfenningPfenning, Frank Carnegie Mellon University, USAUnited States Security Reasoning via Substructural Dependency Tracking
Kittiphon PhalakarnPhalakarn, Kittiphon National Institute of InformaticsJapan Committee Member in Artifact Evaluation Committee within the VMCAI-track
David PichardiePichardie, David MetaFrance Current State of the Industrial-Strength Infer Static Analysis Platform Specialisation: Context-Dependent Reasoning in Incorrectness Separation Logic Committee Member in Program Committee within the TPSA-track On transitioning from academia to industry Speaker in Speakers and Panelists within the RTFM-track
Jean Pichon-PharabodPichon-Pharabod, Jean Aarhus UniversityDenmark Committee Member in Program Committee within the CPP-track
Brigitte PientkaPientka, Brigitte McGill UniversityCanada Committee Member in Steering Committee within the CPP-track Rocq CARVe-ing: A Library for Substructural Meta-Theory
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States Typing Strictness Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
Frank PiessensPiessens, Frank KU LeuvenBelgium Committee Member in Steering Committee within the PriSC-track
Wout PiessensPiessens, Wout KU Leuven, Belgium An efficient compiler for the IDP-Z3 knowledge base system
Nikhil PimpalkharePimpalkhare, Nikhil Princeton University Context-Free-Language Reachability for Almost-Commuting Transition Systems
Jakob PiribauerPiribauer, Jakob TU DresdenGermany Committee Member in Program Committee within the VMCAI-track
Paolo PistonePistone, Paolo Université Claude Bernard Lyon 1 Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages Compiling Quantum Lambda-Terms into Circuits via the Geometry of Interaction
Clément Pit-ClaudelPit-Claudel, Clément EPFLSwitzerland Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications Precise Reasoning about Container-Internal Pointers with Logical Pinning Tracking Dynamically Bound Variable Dependencies Scalable Type Inference for Intrinsically-Typed Binders
Andreas PodelskiPodelski, Andreas University of FreiburgGermany Committee Member in Program Committee within the POPL -track Committee Member in Steering Committee within the VMCAI-track
Nadia PolikarpovaPolikarpova, Nadia University of California at San DiegoUnited States ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models
Adrien PommelletPommellet, Adrien EPITA / LREFrance Committee Member in Program Committee within the VMCAI-track
Hernán Ponce de LeónPonce de León, Hernán Huawei Dresden Research CenterGermany Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
Enrico PontelliPontelli, Enrico Committee Member in Program Committee within the PADL-track
Francesco PontiggiaPontiggia, Francesco TU Wien Committee Member in Artifact Evaluation Committee within the VMCAI-track
Jeremy PopePope, Jeremy Chalmers University of Technology, Gothenburg University, Sweden A Graded Modal Type Theory for Pulse Schedules
François PottierPottier, François InriaFrance (TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the RocqPL-track
Damien PousPous, Damien CNRS Adhesive Category Theory for Graph Rewriting in Rocq
Christian PovedaPoveda, Christian UnaffiliatedColombia Miri: Practical Undefined Behavior Detection for Rust
Diogo PoçasPoças, Diogo Instituto de Telecomunicações, University of Lisbon Types as grammars
Swarn PriyaPriya, Swarn Virginia TechUnited States Committee Member in Program Committee within the RocqPL-track
Benjamin PrzybockiPrzybocki, Benjamin Carnegie Mellon UniversityUnited States Characterizing Sets of Theories That Can Be Disjointly Combined
Sophie PullPull, Sophie University of BristolUnited Kingdom A Complementary Approach to Incorrectness Typing
Christopher PultePulte, Christopher University of CambridgeUnited Kingdom Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
Violet Ka I PunPun, Violet Ka I Western Norway University of Applied SciencesNorway Layers of Confluence for Actors
Thibaut PéramiPérami, Thibaut University of CambridgeUnited Kingdom ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
George PîrleaPîrlea, George National University of SingaporeSingapore Veil: Automated and Interactive Verification of Transition Systems Foundational Multi-Modal Program Verifiers Velvet: A Multi-Modal Verifier for Effectful Programs Lessons from Building an Auto-Active Verifier in Lean
Corina S. PăsăreanuPăsăreanu, Corina S. Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the POPL -track
Q 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 A Verified High-Performance Composable Object Library for Remote Direct Memory Access U-Turn: Enhancing Incorrectness Analysis by Reversing Direction Bayesian Separation Logic Specialisation: Context-Dependent Reasoning in Incorrectness Separation Logic Soteria Rust: Efficient Symbolic Execution for Rust Committee Member in Program Committee within the TPSA-track Committee Member in Organizing Committee within the TPSA-track
Arshia RafieioskoueiRafieioskouei, Arshia Michigan State UniversityUnited States Efficient Discovery of Actual Causality in Stochastic Systems
Mukund RaghothamanRaghothaman, Mukund University of Southern CaliforniaUnited States Committee Member in Program Committee within the PADL-track
Abhiramon RajasekharanRajasekharan, Abhiramon The University of Texas at Dallas REGAL: Extracting implicit rules in text using LLMs with logic program feedback
Steven RamsayRamsay, Steven University of BristolUnited Kingdom A Complementary Approach to Incorrectness Typing
Robert RandRand, Robert University of ChicagoUnited States Workshops Co-Chair in Organizing Committee for POPL 2026 Efficiently Verifying Quantum Programs with Few T Gates Committee Member in Organizing Committee within the PLanQC-track Committee Member in Program Committee within the PLanQC-track
Keith RandallRandall, Keith GoogleUnited States Welterweight Go: Boxing, Structural Subtyping, and Generics
Francesco RanzatoRanzato, Francesco University of PadovaItaly Committee Member in Program Committee within the VMCAI-track
Stefan RatschanRatschan, Stefan The Czech Academy of SciencesCzechia Input-based Three-Valued Abstraction Refinement
Frédéric RecoulesRecoules, Frédéric CEA, List BINSEC: Adapting Symbolic Execution for Binary-level Security Committee Member in Artifact Evaluation Committee within the VMCAI-track
Idan RefaeliRefaeli, Idan Hebrew University of JerusalemIsrael Proof Minimization in Neural Network Verification
John RegehrRegehr, John University of UtahUnited States Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
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 Committee Member in Organizing Committee within the PLanQC-track
Thomas RepsReps, Thomas University of Wisconsin-MadisonUnited States Context-Free-Language Reachability for Almost-Commuting Transition Systems
McCoy Reynolds BeckerReynolds Becker, McCoy MIT Probabilistic Programming with Vectorized Programmable Inference
Andrew ReynoldsReynolds, Andrew University of IowaUnited States Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
Morten RhigerRhiger, Morten Committee Member in Program Committee within the PEPM-track
Fracesco RiccaRicca, Fracesco University of CalabriaItaly Solving hard combinatorial optimization problems with PyQASP
Alex RiceRice, Alex University of EdinburghUnited Kingdom Quantum Circuits Are Just a Phase
Diletta RigoRigo, Diletta Dipartimento di Matematica, University of Padova, ItalyItaly Committee Member in Artifact Evaluation Committee within the VMCAI-track
Martin C. RinardRinard, Martin C. Massachusetts Institute of TechnologyUnited States Probabilistic Programming with Vectorized Programmable Inference
Talia RingerRinger, Talia University of Illinois at Urbana-ChampaignUnited States Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the RocqPL-track
Sam RitchieRitchie, Sam Massachusetts Institute of TechnologyUnited States Probabilistic Programming with Vectorized Programmable Inference
Xavier RivalRival, Xavier Inria - CNRS - Ecole Normale Superieure de Paris - PSL UniversityFrance Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
Paul RobertRobert, Paul CEA LIST Committee Member in Artifact Evaluation Committee within the VMCAI-track
Kenneth RogaleRogale, Kenneth Michigan State UniversityUnited States Efficient Discovery of Actual Causality in Stochastic Systems
Morgan RogersRogers, Morgan University Sorbonne Paris 13France What Is a Monoid?
Enrique Román-CalvoRomán-Calvo, Enrique University of FreiburgGermany Arbitration-Free Consistency Is Available (and Vice Versa)
Shuge RongRong, Shuge Carnegie Mellon University A Certifying Proof Assistant for Synthetic Mathematics in Lean
Johann RosainRosain, Johann ENS LyonFrance Bounded Sort Polymorphism with Elimination Constraints
Neil Julien RossRoss, Neil Julien Dalhousie UniversityCanada Committee Member in Program Committee within the PLanQC-track
Marcus RosselRossel, Marcus Barkhausen Institut; TU DarmstadtGermany Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
Sanghamitra RoyRoy, Sanghamitra Utah State UniversityUnited States Probabilistic Verification for Modular Network-on-Chip Systems
Fabian RuchRuch, Fabian UnaffiliatedSweden Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Neea RuschRusch, Neea Uppsala UniversitySweden Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Alejandro RussoRusso, Alejandro Chalmers University of Technology, Sweden / University of Gothenburg, Sweden / DPella AB, SwedenSweden Towards Lightweight and Efficient Choreographic Cloud Services
Louis RustenholzRustenholz, Louis Universidad Politécnica de Madrid (UPM) and IMDEA Software InstituteSpain Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Didier RémyRémy, Didier Inria Omnidirectional type inference for ML
Philipp RümmerRümmer, Philipp University of Regensburg and Uppsala University Verification of E-Voting Algorithms in Dafny
S William S. MosesS. Moses, William University of Illinois Urbana-ChampaignUnited States Committee Member in Program Committee within the LAFI-track
Feras SaadSaad, Feras Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the LAFI-track
Amr SabrySabry, Amr Indiana UniversityUnited States Committee Member in Program Committee within the POPL -track
Claudio Sacerdoti CoenSacerdoti Coen, Claudio University of Bologna The HOL-Light library of Multivariate real analysis in Rocq
Daniel SainatiSainati, Daniel University of PennsylvaniaUnited States Typing Strictness
Prakash SaivasanSaivasan, Prakash Institute of Mathematical SciencesIndia Parametrised Verification of Intel-x86 Programs Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
Ken SakayoriSakayori, Ken University of TokyoJapan On Circuit Description Languages, Indexed Monads, and Resource Analysis
Guido SalvaneschiSalvaneschi, Guido University of St. GallenSwitzerland Committee Member in Selection Committee within the POPL Student Research Competition-track
Michael SammlerSammler, Michael Institute of Science and Technology AustriaAustria Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation Committee Member in Program Committee within the POPL -track A Recipe for Modular Verification of Generic Tree Traversals Committee Member in Program Committee within the CPP-track
David SananSanan, David Singapore Institute of Technology Committee Member in Program Committee within the POPL -track
Sriram SankaranarayananSankaranarayanan, Sriram University of Colorado, BoulderUnited States Committee Member in Steering Committee within the VMCAI-track
Victor SannierSannier, Victor Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStALFrance Dependent Coeffects for Local Sensitivity Analysis
N. Ege SaraçSaraç, N. Ege CISPA Helmholtz Center for Information Security Committee Member in Artifact Evaluation Committee within the VMCAI-track
Zeynep G. SaribaturSaribatur, Zeynep G. TU WienAustria Committee Member in Program Committee within the PADL-track
Abhiroop SarkarSarkar, Abhiroop ETH ZurichSwitzerland Committee Member in Program Committee within the PriSC-track
Félix Sassus-BourdaSassus-Bourda, Félix ENS Paris Saclay Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic
Udaya SathiyamoorthySathiyamoorthy, Udaya University of Massachusetts at BostonUnited States A Modular Static Cost Analysis for GPU Warp-Level Parallelism
V.R. SathiyanarayanaSathiyanarayana, V.R. MPI-SWSGermany Verifying Almost-Sure Termination for Randomized Distributed Algorithms
Ryosuke SatoSato, Ryosuke Tokyo University of Agriculture and TechnologyJapan Committee Member in Program Committee within the POPL -track
Sota SatoSato, Sota Kyoto UniversityJapan Committee Member in Artifact Evaluation Committee within the VMCAI-track
Rif A. SaurousSaurous, Rif A. GoogleUnited States Probabilistic Programming with Vectorized Programmable Inference
Ömer Faruk SayilirSayilir, Ömer Faruk University of Twente Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Mariano ScazzarielloScazzariello, Mariano RISE Research Institutes of Sweden Toward Automated, Contamination-free Dafny Benchmark Generation
Ina SchaeferSchaefer, Ina KITGermany Committee Member in Program Committee within the PLanQC-track
Gabriel SchererScherer, Gabriel Université Paris Cité - Inria - CNRSFrance Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic Committee Member in Program Committee within the POPL -track Omnidirectional type inference for ML
Oli SchererScherer, Oli UnaffiliatedGermany Miri: Practical Undefined Behavior Detection for Rust
Alan SchmittSchmitt, Alan InriaFrance Workshops Co-Chair in Organizing Committee for POPL 2026
Rudi SchneiderSchneider, Rudi TU BerlinGermany Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
William SchoberSchober, William Università della Svizzera italiana Towards a Hierarchical Quantum Circuit Language
Christoph SchollScholl, Christoph University of FreiburgGermany Committee Member in Program Committee within the VMCAI-track
Tom SchrijversSchrijvers, Tom KU LeuvenBelgium An efficient compiler for the IDP-Z3 knowledge base system Committee Member in Program Committee within the PADL-track Staging Effect Handlers for Modular Search Committee Member in Program Committee within the PEPM-track
Philipp SchröerSchröer, Philipp RWTH Aachen UniversityGermany Diagnostics in Probabilistic Program Verification
Michael SchwarzSchwarz, Michael National University of SingaporeSingapore Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Data Race Detection by Digest-Driven Abstract Interpretation
Frank SchüsseleSchüssele, Frank University of FreiburgGermany The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
Lia SchützeSchütze, Lia MPI-SWSGermany Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
Monika SeisenbergerSeisenberger, Monika Swansea University Formal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq
Yanis SellamiSellami, Yanis CEA, List, Univ. Grenoble Alpes BINSEC: Adapting Symbolic Execution for Binary-level Security Committee Member in Program Committee within the PriSC-track
Ilya SergeySergey, Ilya National University of SingaporeSingapore Foundational Multi-Modal Program Verifiers Velvet: A Multi-Modal Verifier for Effectful Programs Lessons from Building an Auto-Active Verifier in Lean Committee Member in Program Committee within the Dafny-track Committee Member in Organizing Committee within the RTFM-track
Anton SetzerSetzer, Anton Swansea University Formal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq
Peter SewellSewell, Peter University of CambridgeUnited Kingdom ArchSem: Reusable Rigorous Semantics of Relaxed Architectures Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach On long-term research vision Speaker in Speakers and Panelists within the RTFM-track
Zhong ShaoShao, Zhong Yale UniversityUnited States Committee Member in Steering Committee within the CPP-track
Yue ShiShi, Yue Princeton University A Pulse-Level DSL for Real-Time Quantum Control with Hardware Compilation and Emulation
Zheng ShiShi, Zheng National University of SingaporeSingapore The Complexity of Testing Message-Passing Concurrency
Shweta ShindeShinde, Shweta ETH ZurichSwitzerland Committee Member in Steering Committee within the PriSC-track
Zev ShiraziShirazi, Zev University of OxfordUnited Kingdom The Relative Monadic Metalanguage
Mahsa ShirmohammadiShirmohammadi, Mahsa CNRSFrance Determination Problems for Orbit Closures and Matrix Groups Committee Member in Program Committee within the POPL -track
Sharon ShohamShoham, Sharon Tel Aviv UniversityIsrael Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
Filip SieczkowskiSieczkowski, Filip Heriot-Watt UniversityUnited Kingdom Committee Member in Program Committee within the POPL -track
Stephen F. SiegelSiegel, Stephen F. University of DelawareUnited States Committee Member in Program Committee within the VMCAI-track
Mihaela SighireanuSighireanu, Mihaela University Paris-Saclay, ENS Paris-Saclay, CNRS, LMFFrance TypedC: Spatial Memory Safety for Low Level Programs by Abstract Interpretation
Mihaela SighireanuSighireanu, Mihaela University Paris-Saclay, ENS Paris-Saclay, CNRS, LMFFrance Committee Member in Program Committee within the VMCAI-track
Julien SignolesSignoles, Julien Université Paris-Saclay, CEA, ListFrance Committee Member in Program Committee within the VMCAI-track
Alexandra SilvaSilva, Alexandra Cornell UniversityUnited States Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
Gil SilvaSilva, Gil LASIGE, University of Lisbon Types as grammars
Mário SilvaSilva, Mário Inria Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Abhishek Kr SinghSingh, Abhishek Kr IIIT HyderabadIndia Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Alok SinghSingh, Alok Beneficial AI Foundation A benchmark for vericoding: formally verified program synthesis
Gagandeep SinghSingh, Gagandeep University of Illinois at Urbana-Champaign; VMware ResearchUnited States Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation
Pratap SinghSingh, Pratap CMU Foundational Verification of Running-Time Bounds for Interactive Programs
Vidush SinghalSinghal, Vidush Purdue UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Rob SisonSison, Rob UNSW SydneyAustralia Committee Member in Program Committee within the PriSC-track
KC SivaramakrishnanSivaramakrishnan, KC IIT Madras and TaridesIndia A Guided Tour through Oxidized OCaml
Opale SjöstedtSjöstedt, Opale Imperial College London Soteria Rust: Efficient Symbolic Execution for Rust
Anna SlobodovaIntelSlobodovaIntel, Anna Centaur Technology Committee Member in Program Committee within the CPP-track
Colin SmithSmith, Colin Massachusetts Institute of TechnologyUnited States Probabilistic Programming with Vectorized Programmable Inference
Finn SmithSmith, Finn St Andrews University Certifying the decidability of the word problem in monoids at large
Pavel SokolovSokolov, Pavel National Research University Higher School of Economics, Faculty of Computer Science Garbage Collection for Higher Inductive Types
Thomas SomersSomers, Thomas Radboud University Nijmegen Building Blocks for Step-Indexed Program Logics
Byoungho SonSon, Byoungho POSTECHSouth Korea A Formal Executable Semantics of PROMELA
Matthieu SozeauSozeau, Matthieu InriaFrance Bounded Sort Polymorphism with Elimination Constraints Committee Member in Program Committee within the POPL -track Mechanically Verified Universe Checking and Variance Inference for The Rocq Prover Nested Inductive Types for Rocq and Lean
B SrivathsanSrivathsan, B Chennai Mathematical InstituteIndia Committee Member in Program Committee within the VMCAI-track
Gaëtan StaquetStaquet, Gaëtan Nantes Université - École Centrale Nantes - CNRS - LS2N - UMR 6004France Committee Member in Artifact Evaluation Committee within the VMCAI-track
Kathrin StarkStark, Kathrin Heriot-Watt UniversityUnited Kingdom Student Research Competition Co-Chair in Organizing Committee for POPL 2026 Student Research Competition Co-Chair in Selection Committee within the POPL Student Research Competition-track Conference Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track Sulfur: Substitution Generation using a Logical Framework
Sam StatonStaton, Sam University of OxfordUnited Kingdom An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories The Relative Monadic Metalanguage Associate Chair in Program Committee within the POPL -track Committee Member in Program Committee within the PLanQC-track
Deian StefanStefan, Deian University of California at San DiegoUnited States Committee Member in Steering Committee within the PriSC-track
Leo StefanescoStefanesco, Leo University of CambridgeUnited Kingdom Committee Member in Program Committee within the POPL -track
Michel SteuwerSteuwer, Michel TU BerlinGermany Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
Marielle StoelingaStoelinga, Marielle University of Twente and Radboud University, NijmegenNetherlands Committee Member in Program Committee within the VMCAI-track
Jan StrejcekStrejcek, Jan Masaryk UniversityCzechia Committee Member in Program Committee within the VMCAI-track
Terru StübingerStübinger, Terru Karlsruhe Institut für Technologie Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Bonan SuSu, Bonan Tsinghua University An Expressive Assertion Language for Quantum Programs
Emmanuel Suarez AcevedoSuarez Acevedo, Emmanuel Cornell UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Kohei SuenagaSuenaga, Kohei Graduate School of Informatics, Kyoto UniversityJapan Committee Member in Program Committee within the VMCAI-track
Hari SundarSundar, Hari Tufts UniversityUnited States DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
Tarun SureshSuresh, Tarun United States Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States Session Chair of Keynote 2 and Paper 2 (part of CPP) Business Meeting PC Chair in Organizing Committee within the CPP-track PC Chair in Program Committee within the CPP-track
David SwaseySwasey, David Riverside Research Verification of Templated Code in C++
Wouter SwierstraSwierstra, Wouter Utrecht University, NetherlandsNetherlands Hole Refinements for Polymorphic Type-and-Example Driven Synthesis
Hira Taqdees SyedaSyeda, Hira Taqdees Amazon Web ServicesGermany Committee Member in Program Committee within the CPP-track
Steffan SølvstenSølvsten, Steffan Aarhus UniversityDenmark Multi-variable Quantification of BDDs in External Memory using Nested Sweeping
T Nicolas TabareauTabareau, Nicolas InriaFrance Bounded Sort Polymorphism with Elimination Constraints Session Chair of Keynote 1 and Paper 1 (part of CPP)
Nicolas TabareauTabareau, Nicolas Inria Business Meeting
Nicolas TabareauTabareau, Nicolas InriaFrance 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 Nested Inductive Types for Rocq and Lean
Islam TalipovTalipov, Islam National Research University Higher School of Economics, Faculty of Computer Science Garbage Collection for Higher Inductive Types
Max TanTan, Max MIT A benchmark for vericoding: formally verified program synthesis
Tian TanTan, Tian Nanjing UniversityChina ChiSA: Static Analysis for Lightweight Chisel Verification
Yong Kiam TanTan, Yong Kiam *Institute for Infocomm Research, ASTAR** Verified VCG and Verified Compiler for Dafny
Wenhao TangTang, Wenhao The University of EdinburghUnited Kingdom Rows and Capabilities as Modal Effects
Swamit TannuTannu, Swamit University of Wisconsin-MadisonUnited States Generating Compilers for Qubit Mapping and Routing
Éric TanterTanter, Éric University of ChileChile Bounded Sort Polymorphism with Elimination Constraints Committee Member in Program Committee within the POPL -track
Runzhou TaoTao, Runzhou University of Maryland, College ParkUnited States Committee Member in Program Committee within the POPL -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 Web Chair in Organizing Committee for POPL 2026 All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants Committee Member in Program Committee within the POPL -track Committee Member in Steering Committee Chairs within the Dafny-track
Enrico TassiTassi, Enrico INRIAFrance Determinacy Checking for Elpi: an Higher-Order Logic Programming Language with Cut
Christine TassonTasson, Christine Sorbonne Université — LIP6France Committee Member in Steering Committee within the LAFI-track
Max TegmarkTegmark, Max Massachusetts Institute of Technology A benchmark for vericoding: formally verified program synthesis
Kayo TeiTei, Kayo Waseda UniversityJapan Graph Rewriting Language as a Platform for Quantum Diagrammatic Calculi
Jakob TepeTepe, Jakob TU BraunschweigGermany Oriented Metrics for Bottom-Up Enumerative Synthesis
Holger ThiesThies, Holger Kyoto University Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
Ramanathan S. ThinniyamThinniyam, Ramanathan S. Uppsala UniversitySweden General Decidability Results for Systems with Continuous Counters Parameterized Verification of Quantum Circuits Committee Member in Program Committee within the POPL -track
Amin TimanyTimany, Amin Aarhus UniversityDenmark Committee Member in Steering Committee within the CPP-track
Roxana-Mihaela TimonTimon, Roxana-Mihaela Alexandru Ioan Cuza University, Iasi, Romania The Design of an Interactive Proof Mode for Dafny
Cesare TinelliTinelli, Cesare University of IowaUnited States Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
Laura TitoloTitolo, Laura Code MetalUnited States Committee Member in Program Committee within the POPL -track
Andy TockmanTockman, Andy Massachussetts Institute of Technology Foundational Verification of Running-Time Bounds for Interactive Programs
Guilherme V. ToledoToledo, Guilherme V. Bar-Ilan UniversityIsrael Characterizing Sets of Theories That Can Be Disjointly Combined
Andrew TolmachTolmach, Andrew Portland State University Committee Member in Program Committee within the PriSC-track
Bernardo ToninhoToninho, Bernardo Instituto Superior Técnico - University of LisbonPortugal Lazy Linearity for a Core Functional Language Welterweight Go: Boxing, Structural Subtyping, and Generics
Matthew TooheyToohey, Matthew University of TorontoCanada Extensible Data Types with Ad-Hoc Polymorphism
Balazs TothToth, Balazs Ludwig-Maximilians-Universität München Adding Sorts to an Isabelle Formalization of Superposition
Sophie TourretTourret, Sophie Max Planck Institute for Informatics Committee Member in Program Committee within the CPP-track
Masaki ToyodaToyoda, Masaki Hosei UniversityJapan Incrementalizing Haskell implementation of Putback-based Bidirectional Transformation Language BiGUL (Short Paper)
David TrabishTrabish, David TechnionIsrael Enhancing Symbolic Execution with Machine-Checked Safety Proofs
Dmitriy TraytelTraytel, Dmitriy University of CopenhagenDenmark Committee Member in Program Committee within the POPL -track Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Steering Committee within the CPP-track
Alexandru TrifanovTrifanov, Alexandru None Staging Effect Handlers for Modular Search
Jean-Baptiste TristanTristan, Jean-Baptiste AmazonUnited States Committee Member in Steering Committee Chairs within the Dafny-track Committee Member in Steering Committee within the LAFI-track
Tzu-Chun TsaiTsai, Tzu-Chun Academia Sinica Can we formalise type theory intrinsically without any compromise? A case study in Cubical Agda
Wei-Lun TsaiTsai, Wei-Lun Academia Sinica Verifying Repeat-Until-Success Circuits with AutoQ
Takeshi TsukadaTsukada, Takeshi Chiba UniversityJapan Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PLanQC-track
Andrea TurriniTurrini, Andrea Institute of Software, Chinese Academy of SciencesChina SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation
U Kazunori UedaUeda, Kazunori Waseda UniversityJapan Graph Rewriting Language as a Platform for Quantum Diagrammatic Calculi
Shubham UgareUgare, Shubham MetaUnited States Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation
Caterina UrbanUrban, Caterina Inria Paris - ENS - Université PSLFrance A Logic for the Imprecision of Abstract Interpretations Termination Resilience Static Analysis
Henning UrbatUrbat, Henning Friedrich-Alexander-University Erlangen-NürnbergGermany Higher-Order Behavioural Conformances via Fibrations
V Viktor VafeiadisVafeiadis, Viktor MPI-SWSGermany A Verified High-Performance Composable Object Library for Remote Direct Memory Access
Benoît ValironValiron, Benoît Université Paris-Saclay, CNRS, CentraleSupélec, LMF Finding Photonics Circuits via δ-weakening SMT
Tomas Vallejos ParadaVallejos Parada, Tomas Inria Trocq parametricity translations for inductives
Milla ValnetValnet, Milla Sorbonne UniversitéFrance Towards automatic functional correctness in the Mopsa static analyzer
Simcha van Collemvan Collem, Simcha Radboud University NijmegenNetherlands A Relational Separation Logic for Effect Handlers
Jaco van de Polvan de Pol, Jaco Aarhus UniversityDenmark Multi-variable Quantification of BDDs in External Memory using Nested Sweeping
Huub van de Weteringvan de Wetering, Huub Eindhoven University of Technology Formal Verification of Minimax Algorithms
Niels van der Weidevan der Weide, Niels Radboud UniversityNetherlands From Semantics to Syntax: A Type Theory for Comprehension Categories Committee Member in Program Committee within the CPP-track
Tom van Dijkvan Dijk, Tom University of TwenteNetherlands Committee Member in Program Committee within the VMCAI-track
David Van HornVan Horn, David University of MarylandUnited States Committee Member in Program Committee within the POPL -track
Bram VandenbogaerdeVandenbogaerde, Bram Software Languages Lab, Vrije Universiteit BrusselBelgium Committee Member in Artifact Evaluation Committee within the VMCAI-track
Simon VandeveldeVandevelde, Simon KU Leuven, Belgium An efficient compiler for the IDP-Z3 knowledge base system
Julien VanegueVanegue, Julien Imperial College London; BloombergUnited States AMPLE: Fine-grained File Access Policies for Server Applications Committee Member in Program Committee within the TPSA-track
Anton VaronkaVaronka, Anton TU Wien Determination Problems for Orbit Closures and Matrix Groups
Vasco T. VasconcelosVasconcelos, Vasco T. LASIGE, University of LisbonPortugal Types as grammars
Nikos VasilakisVasilakis, Nikos Brown UniversityUnited States Analyzing Shell Scripts
Marco VassenaVassena, Marco Utrecht UniversityNetherlands Committee Member in Program Committee within the POPL -track Committee Member in Steering Committee within the PriSC-track Co-chair in Program Committee within the PriSC-track
Niki VazouVazou, Niki IMDEA Software Institute Chair in Program Committee within the WITS-track
Joey Velez-GinorioVelez-Ginorio, Joey Compiling to Linear Neurons
Niccolò VeltriVeltri, Niccolò IT University of CopenhagenDenmark Di- is for Directed: First-Order Directed Type Theory via Dinaturality
Joost VennekensVennekens, Joost KU Leuven An efficient compiler for the IDP-Z3 knowledge base system Committee Member in Program Committee within the PADL-track
Freek VerbeekVerbeek, Freek Open Universiteit & Virginia Tech Committee Member in Program Committee within the PriSC-track
Quentin VermandeVermande, Quentin Université Côte d'Azur, Inria Cylindrical Algebraic Decomposition in Coq/Rocq
Jules VillardVillard, Jules MetaUnited Kingdom Committee Member in Program Committee within the TPSA-track Committee Member in Organizing Committee within the TPSA-track
Mahesh ViswanathanViswanathan, Mahesh University of Illinois at Urbana-ChampaignUnited States Committee Member in Program Committee within the POPL -track
Kilian VoßVoß, Kilian University of Regensburg Verification of E-Voting Algorithms in Dafny
Matthijs VákárVákár, Matthijs Utrecht University Committee Member in Steering Committee within the LAFI-track
W Nick WaddoupsWaddoups, Nick nick.waddoups@usu.eduUnited States Probabilistic Verification for Modular Network-on-Chip Systems
Philip WadlerWadler, Philip University of EdinburghUnited Kingdom Welterweight Go: Boxing, Structural Subtyping, and Generics
Masaki WagaWaga, Masaki Kyoto UniversityJapan Committee Member in Program Committee within the VMCAI-track
Ryo WakizakaWakizaka, Ryo Kyoto UniversityJapan RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
David WalkerWalker, David Network Change Validation with Relational NetKAT
Johannes WallnerWallner, Johannes Graz University of TechnologyAustria Committee Member in Program Committee within the PADL-track
Michael WalterWalter, Michael Ruhr-Universität Bochum Traq: Estimating the Quantum Cost of Classical Programs
Anduo WangWang, Anduo Temple University, USA Declarative Debugging for Modern Networks Partial Evaluation as a primitive in modern network troubleshooting (Talk Proposal)
Changjie WangWang, Changjie KTH Royal Institute of Technology Toward Automated, Contamination-free Dafny Benchmark Generation
Chao WangWang, Chao University of Southern CaliforniaUnited States Committee Member in Program Committee within the POPL -track
Di WangWang, Di Peking UniversityChina Committee Member in Program Committee within the POPL -track Inferring Typing Rules for Contextual Sugars
Qian (Andy) WangWang, Qian (Andy) ETH Zurich and Imperial College LondonUnited Kingdom Miri: Practical Undefined Behavior Detection for Rust
Xiaoyan WangWang, Xiaoyan Massachusetts Institute of TechnologyUnited States Probabilistic Programming with Vectorized Programmable Inference
Yuepeng WangWang, Yuepeng Simon Fraser UniversityCanada Committee Member in Program Committee within the POPL -track
Yuting WangWang, Yuting Shanghai Jiao Tong UniversityChina Committee Member in Program Committee within the POPL -track
Kazuki WatanabeWatanabe, Kazuki National Institute of Informatics; SOKENDAIJapan Committee Member in Program Committee within the VMCAI-track
Conrad WattWatt, Conrad Nanyang Technological UniversitySingapore Virtualization Chair in Organizing Committee for POPL 2026
Matthew Z. WeaverWeaver, Matthew Z. Bloomberg L.P. Crane Lowers Rocq Safely into C++
Guannan WeiWei, Guannan Tufts UniversityUnited States Committee Member in Program Committee within the PEPM-track
Shiyi WeiWei, Shiyi University of Texas at DallasUnited States Interpretable Configuration Optimization for Static Program Verification via Rule-Based and Counterfactual Reasoning
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States Typing Strictness Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach Associate Chair in Program Committee within the POPL -track On building a successful research group Speaker in Speakers and Panelists within the RTFM-track
Philipp WendlerWendler, Philipp LMU Munich Committee Member in Program Committee within the VMCAI-track
Scott WesleyWesley, Scott Dalhousie University Towards a Hierarchical Quantum Circuit Language Committee Member in Program Committee within the PLanQC-track
Wieger WesselinkWesselink, Wieger Eindhoven University of Technology Formal Verification of Minimax Algorithms
Sam WestrickWestrick, Sam New York UniversityUnited States All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs TypeDis: A Type System for Disentanglement Committee Member in Program Committee within the PADL-track
Leo WhiteWhite, Leo Jane StreetUnited Kingdom Committee Member in Program Committee within the PEPM-track
John WickersonWickerson, John Imperial College LondonUnited Kingdom Committee Member in Program Committee within the POPL -track
Thomas WiesWies, Thomas New York UniversityUnited States Consistent Updates for Scalable Microservices Committee Member in Program Committee within the VMCAI-track
Hans WinderixWinderix, Hans KU LeuvenBelgium Committee Member in Program Committee within the PriSC-track
Sam WinnickWinnick, Sam Simon Fraser University; University of WaterlooCanada Qudit Quantum Programming with Projective Cliffords
Théo WinterhalterWinterhalter, Théo INRIAFrance Bounded Sort Polymorphism with Elimination Constraints Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally Committee Member in Program Committee within the POPL -track Sulfur: Substitution Generation using a Logical Framework
Spencer WoolfsonWoolfson, Spencer Carnegie Mellon University A Certifying Proof Assistant for Synthetic Mathematics in Lean
James WorrellWorrell, James University of OxfordUnited Kingdom Determination Problems for Orbit Closures and Matrix Groups Committee Member in Program Committee within the POPL -track
Ines WrightWright, Ines Aarhus UniversityDenmark A Relational Separation Logic for Effect Handlers
Changshun WuWu, Changshun Université Grenoble Alpes Committee Member in Artifact Evaluation Committee within the VMCAI-track
Haoze WuWu, Haoze Stanford UniversityUnited States Proof Minimization in Neural Network Verification
Nicolas WuWu, Nicolas Imperial College LondonUnited Kingdom Hyperfunctions: Communicating Continuations Handling Higher-Order Effectful Operations with Judgemental Monadic Laws Bayesian Separation Logic Committee Member in Program Committee within the POPL -track
Shiyang WuWu, Shiyang Shanghai Jiao Tong UniversityChina Piecewise Analysis of Probabilistic Programs via k-Induction
Valentina WuWu, Valentina Faculdade de Engenharia, Universidade do Porto Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
Yu-Hsuan WuWu, Yu-Hsuan Academia Sinica A Pulse-Level DSL for Real-Time Quantum Control with Hardware Compilation and Emulation
X Li-yao XiaXia, Li-yao LMF, Inria, Université Paris-SaclayFrance Creusot: Formal verification of Rust programs
Ningning XieXie, Ningning University of TorontoCanada Publicity Chair in Organizing Committee for POPL 2026 Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks Extensible Data Types with Ad-Hoc Polymorphism Welcome Committee Member in Organizing Committee within the PEPM-track Type Inference Techniques: Implementation and Formalization, Better Together
Szumi XieXie, Szumi Eötvös Loránd University (ELTE)Hungary Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yingfei XiongXiong, Yingfei Peking UniversityChina Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
Alex XuXu, Alex Carnegie Mellon UniversityUnited States TypeDis: A Type System for Disentanglement
Amanda XuXu, Amanda University of Wisconsin-Madison Generating Compilers for Qubit Mapping and Routing
Han XuXu, Han Princeton UniversityUnited States Network Change Validation with Relational NetKAT
Runqing XuXu, Runqing KITGermany Stateful Differential Operators for Incremental Computing
Xiaoquan XuXu, Xiaoquan VC-Qiskit: Automated–Interactive Verification of Qiskit Passes with Minimal Intrusion
Yiming XuXu, Yiming LMU Munich A Certifying Proof Assistant for Synthetic Mathematics in Lean
Yingte XuXu, Yingte A Unified Assertion-Based Framework for Classical-Quantum Program Verification
Xu XueXue, Xu University of Hong KongChina Local Contextual Type Inference
Y Jeremy YallopYallop, Jeremy University of CambridgeUnited Kingdom Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks Committee Member in Program Committee within the POPL -track Brack: A Verified Compiler for Scheme via CakeML A One-Pass CPS Transform with Simulation on the Nose
Akihisa YamadaYamada, Akihisa AISTJapan Committee Member in Program Committee within the CPP-track
Naoki YamamotoYamamoto, Naoki Waseda UniversityJapan Graph Rewriting Language as a Platform for Quantum Diagrammatic Calculi
Hongseok YangYang, Hongseok KAISTRepublic of Korea Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
Shengyuan YangYang, Shengyuan University of Wisconsin-Madison Quantum Assertion Testing Without Mid-Circuit Measurement: Strategies and Lower Bounds
Tengshun YangYang, Tengshun Institute of Software at Chinese Academy of SciencesChina Piecewise Analysis of Probabilistic Programs via k-Induction
Zhixuan YangYang, Zhixuan Imperial College LondonUnited Kingdom Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
Yue YaoYao, Yue Carnegie Mellon UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Mechanizing Synthetic Tait Computability in Istari
Qianchuan YeYe, Qianchuan University at Buffalo, SUNYUnited States Committee Member in Program Committee within the POPL -track
Zhentao YeYe, Zhentao Peking UniversityChina Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
Kwangkeun YiYi, Kwangkeun Seoul National University Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling Retargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
Mingsheng YingYing, Mingsheng Institute of Software at Chinese Academy of Sciences; Tsinghua UniversityChina An Expressive Assertion Language for Quantum Programs VC-Qiskit: Automated–Interactive Verification of Qiskit Passes with Minimal Intrusion
Nobuko YoshidaYoshida, Nobuko University of OxfordUnited Kingdom Committee Member in Program Committee within the POPL -track
Neringa YoungYoung, Neringa Lithuania SIGPLAN Conference Manager in Organizing Committee for POPL 2026
Geunyeol YuYu, Geunyeol Pohang University of Science and Technology (POSTECH)South Korea Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tailai YuYu, Tailai Tsinghua University Inferring Typing Rules for Contextual Sugars
Tz-Ching YuYu, Tz-Ching EPFL Towards composable proofs of cache coherence protocols
Charles YuanYuan, Charles University of Wisconsin–MadisonUnited States Quantum Assertion Testing Without Mid-Circuit Measurement: Strategies and Lower Bounds Programming Abstractions for Quantum Linear Algebra Committee Member in Program Committee within the PLanQC-track
Z Daniel ZackonZackon, Daniel McGill UniversityCanada Rocq CARVe-ing: A Library for Substructural Meta-Theory
Enea ZaffanellaZaffanella, Enea University of ParmaItaly Committee Member in Program Committee within the VMCAI-track
Fabian ZaiserZaiser, Fabian MIT Committee Member in Program Committee within the Dafny-track Committee Member in Program Committee within the LAFI-track
George ZakhourZakhour, George University of St. GallenSwitzerland Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yannick ZakowskiZakowski, Yannick InriaFrance Web Chair in Organizing Committee for POPL 2026 test1 Layers of Confluence for Actors Conference Chair in Organizing Committee within the CPP-track
Vadim ZalivaZaliva, Vadim Tufts University, USAUnited States Artifact Evaluation Co-Chair in Organizing Committee for POPL 2026 Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Vladimir ZamdzhievZamdzhiev, Vladimir InriaFrance Quantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic Approach Committee Member in Organizing Committee within the PLanQC-track PC Chair in Program Committee within the PLanQC-track
Marco ZanellaZanella, Marco University of Padova, ItalyItaly Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Compiling to Linear Neurons
Georg ZetzscheZetzsche, Georg MPI-SWSGermany General Decidability Results for Systems with Continuous Counters Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
Stefan ZetzscheZetzsche, Stefan Amazon Web ServicesUnited Kingdom ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification DafnyPro: LLM-Assisted Automated Verification for Dafny Programs Committee Member in Program Committee Chairs within the Dafny-track
Naijun ZhanZhan, Naijun Peking University; Zhongguancun LabChina Piecewise Analysis of Probabilistic Programs via k-Induction
Zhongsheng ZhanZhan, Zhongsheng Nanjing UniversityChina ChiSA: Static Analysis for Lightweight Chisel Verification
Liao ZhangZhang, Liao Shanghai Jiao Tong University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Miaomiao ZhangZhang, Miaomiao School of Computer Science and Technology, Tongji UniversityChina SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation
Qirun ZhangZhang, Qirun Georgia Institute of TechnologyUnited States Committee Member in Program Committee within the POPL -track
Xin ZhangZhang, Xin Peking UniversityChina Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages Fuzzing Guided by Bayesian Program Analysis
Yifan ZhangZhang, Yifan Peking UniversityChina Fuzzing Guided by Bayesian Program Analysis
Yizhou ZhangZhang, Yizhou University of WaterlooCanada Committee Member in Program Committee within the RocqPL-track Committee Member in Program Committee within the LAFI-track
Zhen ZhangZhang, Zhen Utah State UniversityUnited States Probabilistic Verification for Modular Network-on-Chip Systems
Hanrui ZhaoZhao, Hanrui Committee Member in Artifact Evaluation Committee within the VMCAI-track
Huan ZhaoZhao, Huan National University of SingaporeSingapore Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Miranda ZhaoZhao, Miranda MIT A benchmark for vericoding: formally verified program synthesis
Pinhan ZhaoZhao, Pinhan University of MichiganUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Qiyuan ZhaoZhao, Qiyuan National University of SingaporeSingapore Veil: Automated and Interactive Verification of Transition Systems Foundational Multi-Modal Program Verifiers Velvet: A Multi-Modal Verifier for Effectful Programs Lessons from Building an Auto-Active Verifier in Lean
Dinghong ZhongZhong, Dinghong Tufts University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Li ZhouZhou, Li Institute of Software at Chinese Academy of SciencesChina An Expressive Assertion Language for Quantum Programs Committee Member in Program Committee within the VMCAI-track VC-Qiskit: Automated–Interactive Verification of Qiskit Passes with Minimal Intrusion
Timothy ZhouZhou, Timothy ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models
Shaopeng ZhuZhu, Shaopeng Industry Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ekaterina ZhuchkoZhuchko, Ekaterina Tallinn University of Technology Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Hannah ZicarelliZicarelli, Hannah University of Massachusetts at BostonUnited States A Modular Static Cost Analysis for GPU Warp-Level Parallelism
Noam ZilbersteinZilberstein, Noam Cornell UniversityUnited States Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants Modeling Incorrectness and Unknown Functions with Angelic and Demonic Nondeterminism Committee Member in Program Committee within the TPSA-track Committee Member in Organizing Committee within the TPSA-track
Yoni ZoharZohar, Yoni Characterizing Sets of Theories That Can Be Disjointly Combined
Margherita ZorziZorzi, Margherita Committee Member in Program Committee within the PLanQC-track
Elena ZuccaZucca, Elena University of GenoaItaly Committee Member in Program Committee within the POPL -track
Lenore ZuckZuck, Lenore UICUnited States Committee Member in Steering Committee within the VMCAI-track
Joseph ZulloZullo, Joseph Purdue UniversityUnited States Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems
Matthias ZumkellerZumkeller, Matthias University of FreiburgGermany The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
Ø Vebjørn S. ØiestadØiestad, Vebjørn S. University of Bergen Towards a Mechanization of the ECMAScript (JavaScript) Proposal "Temporal"
Š Vojtěch ŠtěpančíkŠtěpančík, Vojtěch InriaFrance Implementing parametricity in Rocq-ELPI

POPL 2026 Contributors

Results (990)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia