POPL 2026 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (1158)

A Zain K AamerAamer, Zain K University of PennsylvaniaUnited States Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
Carmine AbateAbate, Carmine Barkhausen Institute, Dresden WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
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 University of Porto & INESC TECPortugal 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-SaclayFrance Student Volunteer in Student Volunteers for POPL 2026 AdapTT: Functoriality for Dependent Type Casts
Shubh AgrawalAgrawal, Shubh Northeastern University Towards an Equational Calculus of Interventions
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 Towards formally secure compilation of verified F* programs against unverified ML contexts
Amal AhmedAhmed, Amal Northeastern University, USAUnited States Session Chair of Types 2 (part of POPL ) Cryptis: Cryptographic Reasoning in Separation Logic Panel: Promotion and tenure Panel: Work-life balance, service, and teaching Welcome from the Organizers Committee Member in Organizing Committee within the RTFM-track Specifying ABIs with Realizability and Type-Preserving Compilation 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
Keith AllenAllen, Keith University at Buffalo, SUNYUnited States Language Model for MPI
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
Malin AltenmüllerAltenmüller, Malin University of Edinburgh Strictness by Rewrite: Formalising Bipermutative Categories and Quantum Program Semantics in Agda
Guillaume AmbalAmbal, Guillaume Session Chair of Program Logics and Semantic Frameworks (part of POPL ) A Verified High-Performance Composable Object Library for Remote Direct Memory Access
Nada AminAmin, Nada Harvard UniversityUnited States Compiling to Linear Neurons Session Chair of PADL M4 (part of PADL) 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
One AnAn, One Student Volunteer in Student Volunteers for POPL 2026
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 Towards formally secure compilation of verified F* programs against unverified ML contexts
Martin AndrieuxAndrieux, Martin Université de Rennes Student Volunteer in Student Volunteers for POPL 2026
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 Session Chair of PADL M4 (part of PADL) 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
Aslan AskarovAskarov, Aslan Aarhus University Efficient Dependency Resolution in IFC-aware Decentralized Programming
Nicola AssoliniAssolini, Nicola QuantinuumItaly Video Co-Chair in AV Committee for POPL 2026 Video Co-Chair in Organizing Committee for POPL 2026 Embedding a Type-safe Quantum-Lambda Calculus in Haskell
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 RUXt: Automatic Compositional Type Safety Refutation Specialisation: Context-Dependent Reasoning in Incorrectness 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
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 Student Volunteer in Student Volunteers for POPL 2026 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 Student Volunteer in Student Volunteers for POPL 2026 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
Subarno BanerjeeBanerjee, Subarno Amazon Web ServicesUnited States Building the Cloud with Continuous Assurances using Static Analysis
Jialu BaoBao, Jialu Northeastern University Towards an Equational Calculus of Interventions 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 Tooling Design and Lessons Learned from Systematic Evaluations of the Preservation of Low-level Security Properties by Compilers with BinSec
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 Decompiling for Constant-Time Analysis
Prabal BasuBasu, Prabal Utah State UniversityUnited States Probabilistic Verification for Modular Network-on-Chip Systems
Kevin BatzBatz, Kevin Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
Kevin BatzBatz, Kevin RWTH Aachen UniversityGermany Verifying Sampling Algorithms via Distributional Invariants
Guillaume BaudartBaudart, Guillaume InriaFrance Session Chair of Fourth Session (part of LAFI)
Thomas BauereissBauereiss, Thomas University of CambridgeUnited Kingdom ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
Jonathan BaumannBaumann, Jonathan Max Planck Institute for Security and Privacy (MPI-SP) FSLH: Flexible Mechanized Speculative Load Hardening
Pascal BaumannBaumann, Pascal MPI-SWSGermany Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
Barış BayazıtBayazıt, Barış University of Toronto Student Volunteer in Student Volunteers for POPL 2026 RESpecBench: Rigorous Evaluation of Specification Generation with Automated Verification
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
Oscar Bender-StoneBender-Stone, Oscar University of Colorado at Boulder Student Volunteer in Student Volunteers for POPL 2026
Thibaut BenjaminBenjamin, Thibaut Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMFFrance 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 Session Chair of Rocq Enhancements and Extensions (part of RocqPL) Committee Member in Organizing Committee within the RocqPL-track
Marc BezemBezem, Marc University of Bergen Enhancing universe polymorphism for Rocq: Algebraic universes, consistency checking and variance inference
Karthikeyan BhargavanBhargavan, Karthikeyan Cryspen, FranceFrance Software Verification meets Real-World Cryptography 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
Eli BinghamBingham, Eli Broad Institute Typed Abstractions for Causal Probabilistic Programming
Lars BirkedalBirkedal, Lars Aarhus UniversityDenmark Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic Panel: Promotion and tenure Specifying ABIs with Realizability and Type-Preserving Compilation
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) FSLH: Flexible Mechanized Speculative Load Hardening 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
Lionel BlatterBlatter, Lionel Max Planck Institute for Security and Privacy Decompiling for Constant-Time Analysis
Sandrine BlazyBlazy, Sandrine University of RennesFrance General Chair in Organizing Committee for POPL 2026 Session Chair of Keynote (part of POPL ) 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 Session Chair of Solvers (part of VMCAI) 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
Youcef BouzidBouzid, Youcef Decompiling for Constant-Time Analysis
Matt BovelBovel, Matt EPFLSwitzerland First-Class Refinement Types in Scala
Maddy BowersBowers, Maddy Massachusetts Institute of TechnologyUnited States Sequential Monte Carlo Program Synthesis with Refinement Proposals
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
Florian BrandnerBrandner, Florian Télécom ParisFrance Towards Robust Secure Compilation in Presence of Speculative Execution
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
Ewen BROUDIN-CARADECBROUDIN-CARADEC, Ewen ENS Paris Saclay, TU Delft, INRIA Saclay, LMF Student Volunteer in Student Volunteers for POPL 2026 A specification for Agda Core’s unification algorithm for generic pattern matching
Greg BrownBrown, Greg University of EdinburghUnited Kingdom 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 Session Chair of Synthesis 2 (part of POPL ) A Logic for the Imprecision of Abstract Interpretations Committee Member in Program Committee within the POPL -track Session Chair of Short Talks (part of GiacoFest) 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 Lean4Lean: Mechanizing the Metatheory of Lean
Thomas CarottiCarotti, Thomas MIT Foundational Verification of Running-Time Bounds for Interactive Programs
Pedro CarrottCarrott, Pedro Imperial College LondonUnited Kingdom RUXt: Automatic Compositional Type Safety Refutation
Chris CasinghinoCasinghino, Chris Jane Street A Guided Tour through Oxidized OCaml Jane Street Game Night Industry Panel
Jean CasparCaspar, Jean École normale supérieure – PSL, INRIA, LS2N, CNRS S4 modal sequent calculus as intermediate logic and intermediate language (Short Paper)
Simon CastellanCastellan, Simon University of Rennes; Inria; CNRS; IRISAFrance Semantic Foundations for Laziness in Discrete Probabilistic Programming
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 Resource-Aware Hybrid Quantum Programming with General Recursion and Quantum Control
Christopĥe CharetonChareton, Christopĥe CEA, LIST, France Democratizing quantum formal verification: the path-sum way
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
Clément ChavanonChavanon, Clément INRIA Student Volunteer in Student Volunteers for POPL 2026
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 Session Chair of Artificial Inteligence (part of VMCAI) 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 A Design Proposal for GraPPL: Probabilistic Programming with Low-Level, High-Performance GPU 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
Léopold ClémentClément, Léopold Télécom Paris Towards Robust Secure Compilation in Presence of Speculative Execution
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 Session Chair of Metatheory (part of CPP) 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
Elias Rojas CollinsCollins, Elias Rojas MIT A Design Proposal for GraPPL: Probabilistic Programming with Low-Level, High-Performance GPU Programmable Inference
Katherine CollinsCollins, Katherine MIT Language-Model Probabilistic Programming for Improving Autoformalization via Cycle Consistency and Incremental Type-Checking
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
Breandan ConsidineConsidine, Breandan United States A Word Sampler for Well-Typed Functions
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
Andreea CosteaCostea, Andreea TU DelftNetherlands Mind the Boundary: Detecting Undefined Behavior Across Rust’s FFI
Nathanaëlle CourantCourant, Nathanaëlle OCamlProFrance A Lazy, Concurrent Convertibility Checker Industry Panel
Will CrichtonCrichton, Will Brown UniversityUnited States A Guided Tour through Oxidized OCaml
Raphaëlle CrubilléCrubillé, Raphaëlle On Contextual Distances in Randomized Programming: Amplification and Lower Bounds
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
Jack CzenszakCzenszak, Jack Yale UniversityUnited States Nominal Semantics for First-class Automatic Differentiation
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
Mauricio Barba da Costada Costa, Mauricio Barba MIT Language-Model Probabilistic Programming for Improving Autoformalization via Cycle Consistency and Incremental Type-Checking Sequential Monte Carlo Program Synthesis with Refinement Proposals
Raquel Fernandes da Silvada Silva, Raquel Fernandes Imperial College LondonUnited Kingdom Specialisation: Context-Dependent Reasoning in Incorrectness Separation Logic 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 Session Chair of Quantum 1 (part of POPL ) 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 Session Chair of Opening and Keynote (part of GiacoFest) 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 BlueRock SecurityGermany Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic
Lesly-Ann DanielDaniel, Lesly-Ann EURECOMFrance Session Chair of Lightning Talks (part of PriSC) 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 EPFLSwitzerland Session Chair of Separation logic (part of CPP) 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 Student Volunteer in Student Volunteers for POPL 2026 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 Session Chair of Synthesis 1 (part of POPL ) Session Chair of Keynote (part of RocqPL) Session Chair of Certified Programs and Proofs in Rocq (part of RocqPL) Committee Member in Organizing Committee within the RocqPL-track
Christophe DeleuzeDeleuze, Christophe Université Grenoble-Alpes - Grenoble INP - LCIS Compiling countermeasures against fault attacks with “Tracing LLVM”
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 Student Volunteer in Student Volunteers for POPL 2026 Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications
Yijia DengDeng, Yijia University of Wisconsin, Madison Student Volunteer in Student Volunteers for POPL 2026
Martin DesharnaisDesharnais, Martin Ludwig-Maximilians-Universität München Adding Sorts to an Isabelle Formalization of Superposition
Dominique DevrieseDevriese, Dominique KU LeuvenBelgium Calling Conventions for Secure Stack Sharing on CHERI Capability Machines in Practice
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
Tom DiversDivers, Tom University of Bristol A Concise Type System for Borrow Inference
Jenna DiVincenzo (Wise)DiVincenzo (Wise), Jenna Purdue University Opening Committee Member in Organizing Committee within the PLMW @ POPL-track
Minh DoDo, Minh University of New South Wales Student Volunteer in Student Volunteers for POPL 2026 Formally Verified Optimisations for the Pancake Compiler
Ryan DoengesDoenges, Ryan Boston College Specifying ABIs with Realizability and Type-Preserving Compilation
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
Alexandre DreweryDrewery, Alexandre INRIA Student Volunteer in Student Volunteers for POPL 2026
Derek DreyerDreyer, Derek MPI-SWSGermany Session Chair of Separation Logic (part of POPL ) Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation A Recipe for Modular Verification of Generic Tree Traversals Panel: Promotion and tenure Panel: Visibility and Impact Welcome from the Organizers 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
Owen DuckhamDuckham, Owen Northeastern UniversityUnited States Specifying ABIs with Realizability and Type-Preserving Compilation
Léon DucruetDucruet, Léon Aarhus UniversityDenmark FSLH: Flexible Mechanized Speculative Load Hardening
Ross DuncanDuncan, Ross Quantinuum Committee Member in Organizing Committee within the PLanQC-track
Ulysse Dupont-LatapieDupont-Latapie, Ulysse Laboratoire de Recherche de l'EPITA QUAPLA : a Library for Exact Linear Algebra on Quantum Computers
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
Mohamed ElsheikhElsheikh, Mohamed Barkhausen Institute, Dresden WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
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 Panel: Work-life balance, service, and teaching
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 WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
Javier EsparzaEsparza, Javier Technical University of Munich Committee Member in Program Committee within the VMCAI-track
Ran EttingerEttinger, Ran NVIDIAIsrael Teaching Automata Theory and Formal Languages with Dafny
F Claudia FaggianFaggian, Claudia CNRS, Université Paris Cité Towards Compiling Higher-Order Programs to Bayesian Networks 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
Frantisek FarkaFarka, Frantisek Barkhausen Institute, Dresden WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
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
Ole FenskeFenske, Ole Towards Representation Agnostic Probabilistic Programming
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
Jack FeserFeser, Jack BasisUnited States Typed Abstractions for Causal Probabilistic Programming
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 Opening 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
Jessica FosterFoster, Jessica University of Bristol Embedding a Type-safe Quantum-Lambda Calculus in Haskell
Nate FosterFoster, Nate Cornell University; Jane StreetUnited States How to Write a Paper
Pierre-Alain FouqueFouque, Pierre-Alain Univ Rennes, CNRS, IRISA GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses
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)
José Fragoso SantosFragoso Santos, José INESC-ID; Instituto Superior Técnico - University of LisbonPortugal How to identify security vulnerabilities in Node.js packages?
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 Session Chair of Third Session (part of LAFI) Language-Model Probabilistic Programming for Improving Autoformalization via Cycle Consistency and Incremental Type-Checking Committee Member in Steering Committee within the LAFI-track
Samantha FrohlichFrohlich, Samantha University of BristolUnited Kingdom Embedding a Type-safe Quantum-Lambda Calculus in Haskell
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
Adrian GallusGallus, Adrian RWTH Aachen University Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
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)
Philippa GardnerGardner, Philippa Imperial College LondonUnited Kingdom Towards a Mechanised Theory of Fully Featured Compositional Symbolic Execution
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
Maxime GarnierGarnier, Maxime DIENS Graphix: An Open-Source Compiler and Simulator for Measurement-Based Quantum Computation The MBQCert Project
Lorenzo GazzellaGazzella, Lorenzo Università di Pisa A logic for all reasons
Hong GeGe, Hong University of Cambridge Multi-Agent Systems for Traceable Bayesian Workflow
Martin GebserGebser, Martin University of Klagenfurt, AustriaAustria Committee Member in Program Committee within the PADL-track
Antoine GeimerGeimer, Antoine Univ. Lille, CNRS, Inria Fun with flags: How Compilers Break and Fix Constant-Time Code
Dominik GeißlerGeißler, Dominik Technische Universität BerlinGermany Probabilistic Programming Meets Automata Theory: Exact Inference using Weighted Automata
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"
Matin GhavamiGhavami, Matin Massachusetts Institute of TechnologyUnited States A Design for Massively Parallel Gibbs Sampling on the GPU via Static and Dynamic Analysis of Probabilistic Programs
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
Gaetan GilbertGilbert, Gaetan Session with the Rocq Development Team
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 Amazon Committee Member in Program Committee within the CPP-track
Andrés GoensGoens, Andrés TU DarmstadtGermany Session Chair of Decision Procedures (part of POPL ) Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
Alexander Phidias GoetzGoetz, Alexander Phidias University of Tübingen Student Volunteer in Student Volunteers for POPL 2026 Region Type System with Bidirectional Multiprompt Delimited Control
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
Laure GonnordGonnord, Laure Université Grenoble-Alpes - Grenoble INP - LCISFrance Compiling countermeasures against fault attacks with “Tracing LLVM”
Georges GonthierGonthier, Georges Inria Committee Member in Steering Committee within the CPP-track
Kiran GopinathanGopinathan, Kiran BasisUnited States Committee Member in Program Committee within the RocqPL-track
Kiran GopinathanGopinathan, Kiran University College LondonUnited Kingdom Industry Panel
Kiran GopinathanGopinathan, Kiran BasisUnited States Basis — A Programming Languages Take on Principled Foundations for AI
Andrew D. GordonGordon, Andrew D. Cogna and University of EdinburghUnited Kingdom Multi-Agent Systems for Traceable Bayesian Workflow
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
Pierre GoutagnyGoutagny, Pierre Inria and University of LilleFrance A theory of lists with combinators for SMT solvers
Solomon GrafGraf, Solomon University of Pennsylvania Student Volunteer in Student Volunteers for POPL 2026
Emlyn GrahamGraham, Emlyn DIENS Graphix: An Open-Source Compiler and Simulator for Measurement-Based Quantum Computation The MBQCert Project
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 Session Chair of Specification and Verification Methods (part of POPL ) Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
Ben GreenmanGreenman, Ben University of UtahUnited States Type Narrowing the Hard Way
Simon Oddershede GregersenGregersen, Simon Oddershede CISPA Helmholtz Center for Information SecurityGermany 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 UniversityChina 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
Hanwen GuoGuo, Hanwen University of Utah Type Narrowing the Hard Way
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 Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
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
Emmanuel HainryHainry, Emmanuel LORIA, Université de Lorraine Resource-Aware Hybrid Quantum Programming with General Recursion and Quantum Control
Aurel HamonHamon, Aurel University of Rennes - ENS Rennes Student Volunteer in Student Volunteers for POPL 2026
Michael HanusHanus, Michael Kiel UniversityGermany Session Chair of PADL T2 (part of PADL) Declarative Programming: Efficient and reliable programming with human intelligence (Invited Talk) Committee Member in Program Committee within the PADL-track
Sean Kristian Remond HarboHarbo, Sean Kristian Remond Aalborg UniversityDenmark Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
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
Sebastian HarwigHarwig, Sebastian MPI-SP and Ruhr University Bochum FSLH: Flexible Mechanized Speculative Load Hardening
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 How can Machine Learning Help Formal Proving ?
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
Fritz HengleinHenglein, Fritz University of CopenhagenDenmark Functional Quantum Circuit Simulation with Tensor Term Rank Reduction
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)
Guillaume HietHiet, Guillaume CentraleSupélec, Inria, CNRS, Univ. Rennes Modular and automatic formal verification of a RISC-V processor with security mechanisms
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 AgdaGDL: A Geometric Deep Learning Framework for Property Certification Language Model for MPI Opening Committee Member in Organizing Committee within the PLMW @ POPL-track
Tom HirschowitzHirschowitz, Tom Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 ChambéryFrance Semantic Foundations for Laziness in Discrete Probabilistic Programming
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 Towards an Equational Calculus of Interventions 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 Session Chair of Timing Side Channels (part of PriSC) FSLH: Flexible Mechanized Speculative Load Hardening Blame-aware Recomposition for Formally Secure Low-level Compiler Backends Towards formally secure compilation of verified F* programs against unverified ML contexts Announcing Security Foundations (new volume of Software Foundations) 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 A Design Proposal for GraPPL: Probabilistic Programming with Low-Level, High-Performance GPU 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
Sander HuyghebaertHuyghebaert, Sander Vrije Universiteit Brussel Calling Conventions for Secure Stack Sharing on CHERI Capability Machines in Practice
Hans HüttelHüttel, Hans Aalborg UniversityDenmark Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
I Atsushi IgarashiIgarashi, Atsushi Kyoto UniversityJapan Towards a Non-linear Quantum Lambda Calculus
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; University of GothenburgSweden 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 Session Chair of Keynote (part of POPL ) Program Chair in Program Committee within the POPL -track On grant writing Speaker in Speakers 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 Session Chair of Analysis 1 (part of VMCAI) 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
Ziyue JinJin, Ziyue Peking University The Expressiveness of Programs via Descriptive Complexity
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 LMF, CNRS, Université Paris-SaclayFrance 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
Cyprien JulesJules, Cyprien CentraleSupélec, Inria, CNRS, Univ. Rennes Student Volunteer in Student Volunteers for POPL 2026 Modular and automatic formal verification of a RISC-V processor with security mechanisms
Dustin JulianoJuliano, Dustin Indiana University IndianapolisUnited States Towards Functional Language Runtimes Without Garbage Collection
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 Strictness by Rewrite: Formalising Bipermutative Categories and Quantum Program Semantics in Agda One rig to control them all
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 University of Illinois at Urbana-ChampaignUnited States Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation
Yukiyoshi KameyamaKameyama, Yukiyoshi University of TsukubaJapan Session Chair of Types and logics (part of PEPM) Closing 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 Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
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 Typed Abstractions for Causal Probabilistic Programming
Shuanglong KanKan, Shuanglong Barkhausen Institute, DresdenGermany Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis
Madhav KandaKanda, Madhav University of Illinois Urbana-Champaign Student Volunteer in Student Volunteers for POPL 2026 Grammar-Constrained LLM Generation for Reliable and Efficient Probabilistic Program Synthesis
Johannes KanigKanig, Johannes AdaCoreFrance Managing the Proof Context in SPARK
Rikiya KashiwagiKashiwagi, Rikiya Kyoto University Towards a Non-linear Quantum Lambda Calculus
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Diagnostics in Probabilistic Program Verification Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops Verifying Sampling Algorithms via Distributional Invariants
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 Weak Accept, or: How I Learned to Write Papers and Deal with Reviews
Jingyu KeKe, Jingyu Shanghai Jiao Tong UniversityChina Piecewise Analysis of Probabilistic Programs via k-Induction
Lukas KebuladzeKebuladze, Lukas Carnegie Mellon University Student Volunteer in Student Volunteers for POPL 2026 Amortized Analysis of Splay Trees via a Lax Homomorphism
Ariel E. KellisonKellison, Ariel E. Code MetalUnited States Future-Proofing Numerical Accuracy with Formal Specifications
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 Calling Conventions for Secure Stack Sharing on CHERI Capability Machines in Practice 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 Standard Chartered Bank; Max Planck Institute for Security and Privacy (MPI-SP)Hong Kong SAR China 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-SPGermany 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
Thomas KirsteKirste, Thomas Towards Representation Agnostic Probabilistic Programming
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
Lutz KlinkenbergKlinkenberg, Lutz RWTH Aachen University Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
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
Kacper F. KorbanKorban, Kacper F. EPFLPoland Bootstrapping a Verified Compiler for an Imperative Language in Rocq
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 Session Chair of Concurrency: Types, Logics, and Libraries (part of POPL ) 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 Panel: Work-life balance, service, and teaching
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
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 InstitutGermany Scalable Type Inference for Intrinsically-Typed Binders
Ulrich KühneKühne, Ulrich Télécom Paris Towards Robust Secure Compilation in Presence of Speculative Execution
L Alfons LaarmanLaarman, Alfons Leiden UniversityNetherlands Committee Member in Program Committee within the VMCAI-track
Vincent LafeychineLafeychine, Vincent Université Paris-Saclay, CNRS, ENS Paris-Saclay, INRIA, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France.France 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 AV Committee for POPL 2026 Video Co-Chair in Organizing Committee for POPL 2026
Thomas LamiauxLamiaux, Thomas Nantes Université, Inria Nested Inductive Types for Rocq and Lean
Julien LamiroyLamiroy, Julien Université Paris Saclay Towards a New Logic for Higher Order Quantum Computation
Leonidas LampropoulosLampropoulos, Leonidas University of Maryland, College ParkGreece Committee Member in Selection Committee within the POPL Student Research Competition-track
Evangelos LamprouLamprou, Evangelos Brown University, USAUnited States Analyzing Shell Scripts
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
Thobias Seth LarsenLarsen, Thobias Seth University of Copenhagen Functional Quantum Circuit Simulation with Tensor Term Rank Reduction
Mason LaryLary, Mason University at Buffalo, SUNY AgdaGDL: A Geometric Deep Learning Framework for Property Certification
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
Dao LeLe, Dao UNSW SydneyAustralia Student Volunteer in Student Volunteers for POPL 2026 Decompilation into Interaction Trees
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
Heewon LeeLee, Heewon KAIST, Korea, South (The Republic of)South Korea Asymptotic Analysis as an Abstract Interpretation
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 Typed Abstractions for Causal Probabilistic Programming
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
Maxime LegoupilLegoupil, Maxime Aarhus University Specifying ABIs with Realizability and Type-Preserving Compilation
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 Session Chair of Analysis 3 (part of VMCAI) 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 Session with the Rocq Development Team
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 Panel: Visibility and Impact
Dorian LesbreLesbre, Dorian Université Paris-Saclay - CEA LISTFrance Committee Member in Artifact Evaluation Committee within the VMCAI-track
Michael LeuschelLeuschel, Michael HHUGermany Session Chair of PADL M3 (part of PADL) 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? Effects and Call-by-Push-Value
Alexander K. LewLew, Alexander K. Yale UniversityUnited States Probabilistic Programming with Vectorized Programmable Inference Session Chair of First Session (part of LAFI) Welcome Language-Model Probabilistic Programming for Improving Autoformalization via Cycle Consistency and Incremental Type-Checking Nominal Semantics for First-class Automatic Differentiation Sequential Monte Carlo Program Synthesis with Refinement Proposals Incremental Density Computation for Efficient 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 Student Volunteer in Student Volunteers for POPL 2026 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 Session Chair of Models 2 (part of VMCAI) 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 Session Chair of Quantum and Probabilistic Verification (part of VMCAI) 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 Session Chair of Staging and effect handlers (part of PEPM)
Andreas LindnerLindner, Andreas Uppsala universitetSweden Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Kleio LiotatiLiotati, Kleio Barkhausen Institute, Dresden WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End 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
Puming LiuLiu, Puming New York University Shanghai Semantic Completeness of Higher-Order Probabilistic Separation Logics
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
Andreas LööwLööw, Andreas Royal Holloway, University of LondonUnited Kingdom Towards a Mechanised Theory of Fully Featured Compositional Symbolic Execution
M David M. KahnM. Kahn, David Denison University Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
Stephanie MaMa, Stephanie Cornell UniversityUnited States Student Volunteer in Student Volunteers for POPL 2026
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
Eduardo MadeiraMadeira, Eduardo LASIGE, University of LisbonPortugal Student Volunteer in Student Volunteers for POPL 2026
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 Session Chair of Category Theory (part of POPL ) 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 IRIF, Université Paris CitéFrance A Correct-by-Construction Checker for Validation of Railway Data
Vikash MansinghkaMansinghka, Vikash Massachusetts Institute of Technology A Design for Massively Parallel Gibbs Sampling on the GPU via Static and Dynamic Analysis of Probabilistic Programs A Design Proposal for GraPPL: Probabilistic Programming with Low-Level, High-Performance GPU Programmable Inference Sequential Monte Carlo Program Synthesis with Refinement Proposals Incremental Density Computation for Efficient Programmable Inference
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 Language-Model Probabilistic Programming for Improving Autoformalization via Cycle Consistency and Incremental Type-Checking
William ManskyMansky, William University of Illinois ChicagoUnited States Recursive Mutexes in Separation Logic
Houssein MansourMansour, Houssein ISAE-SUPAERO Student Volunteer in Student Volunteers for POPL 2026 On Contextual Distances in Randomized Programming: Amplification and Lower Bounds
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
Filipe MarquesMarques, Filipe INESC-ID; Instituto Superior Técnico - University of LisbonPortugal How to identify security vulnerabilities in Node.js packages?
Jonathan MarriottMarriott, Jonathan University of BristolUnited Kingdom Domain-Theoretic Semantics for Functional Logic Programming
Brianna MarshallMarshall, Brianna Northeastern UniversityUnited States Specifying ABIs with Realizability and Type-Preserving Compilation
Chris MartensMartens, Chris Northeastern UniversityUnited States Committee Member in Program Committee within the POPL -track Epistemic Logic for Polyglots (Short Paper)
Thierry MartinezMartinez, Thierry DIENS Graphix: An Open-Source Compiler and Simulator for Measurement-Based Quantum Computation The MBQCert Project
Guido MartínezMartínez, Guido Microsoft ResearchUnited States Towards formally secure compilation of verified F* programs against unverified ML contexts
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 Singapore, SingaporeSingapore Session Chair of Automata 2 (part of POPL )
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
Clémentine MauriceMaurice, Clémentine Univ. Lille, Inria, CNRS Fun with flags: How Compilers Break and Fix Constant-Time Code
Nicolas MazzocchiMazzocchi, Nicolas Slovak University of Technology in BratislavaSlovakia Committee Member in Program Committee within the VMCAI-track
Giuseppe MazzottaMazzotta, Giuseppe University of CalabriaItaly Session Chair of PADL M2 (part of PADL) 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 PLMW Panel
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
Sébastien MichellandMichelland, Sébastien Université Grenoble-Alpes - Grenoble INP - LCISFrance Compiling countermeasures against fault attacks with “Tracing LLVM”
Jairo Miguel Marulanda-GiraldoMiguel Marulanda-Giraldo, Jairo University of Southampton Student Volunteer in Student Volunteers for POPL 2026 A Well-behaved Differentiable Logic 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 Grammar-Constrained LLM Generation for Reliable and Efficient Probabilistic Program Synthesis
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 The Art of Living Abroad (and Finding a Good Baguette in New York) PLMW Panel
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
David MonniauxMonniaux, David Université Grenoble Alpes - CNRS - Grenoble INP - VerimagFrance Session Chair of Secure Compilation & Verification (part of PriSC) Session Chair of Information Flow Control (part of PriSC)
Benoît MontaguMontagu, Benoît InriaFrance Industrial Relations Co-Chair in Organizing Committee for POPL 2026 Session Chair of Analysis 2 (part of VMCAI) 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 Day closing Day opening 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 INRIAFrance 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
Doruk Alp MutluMutlu, Doruk Alp Michigan State University Expanding Specification Capabilities of a Gradual Verifier with Pure Functions
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
Emma NardinoNardino, Emma École Normale Supérieure de Lyon / LIP Student Volunteer in Student Volunteers for POPL 2026
André NascimentoNascimento, André INESC-ID; Instituto Superior Técnico - University of LisbonPortugal How to identify security vulnerabilities in Node.js packages?
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 NTU SingaporeGermany 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
Timothy O'DonnellO'Donnell, Timothy Language-Model Probabilistic Programming for Improving Autoformalization via Cycle Consistency and Incremental Type-Checking
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
Gyuhyeok OhOh, Gyuhyeok Seoul National University Partial Evaluation + Global Analyser = Separate Analyser
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 Decompiling for Constant-Time Analysis 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 Renaud PacaletPacalet, Renaud Télécom Paris Towards Robust Secure Compilation in Presence of Speculative Execution
Michele PaganiPagani, Michele ENS LyonFrance Session Chair of Probabilistic Programming (part of POPL ) 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 Inria, École Normale SupérieureFrance Session Chair of Second Session (part of LAFI) Welcome Semantic Foundations for Laziness in Discrete Probabilistic Programming 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 Session Chair of Types 1 (part of POPL ) 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 PLMW Panel Committee Member in Program Committee within the PEPM-track Decoupling Resolution from Type Inference
Michele PasquaPasqua, Michele University of VeronaItaly Session Chair of Short Talks (part of GiacoFest) 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
Romir PatelPatel, Romir MIT Language-Model Probabilistic Programming for Improving Autoformalization via Cycle Consistency and Incremental Type-Checking
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 Session Chair of Automata 1 (part of POPL ) The Complexity of Testing Message-Passing Concurrency
Angel Pavlov AngelovPavlov Angelov, Angel Sofia UniversityBulgaria Video Co-Chair in AV Committee for POPL 2026
Jennifer PaykinPaykin, Jennifer University of VermontUnited States Session Chair of Quantum 2 (part of POPL ) Qudit Quantum Programming with Projective Cliffords Specification, Semantics, and Verification of Quantum Programs PLMW Panel 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
Ludovic PerretPerret, Ludovic EPITA QUAPLA : a Library for Exact Linear Algebra on Quantum Computers
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
Pierrick PhilippePhilippe, Pierrick Univ Rennes, CNRS, IRISA GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses
David PichardiePichardie, David MetaFrance Specialisation: Context-Dependent Reasoning in Incorrectness Separation Logic 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 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
Alexandre PinazzaPinazza, Alexandre EPFL Student Volunteer in Student Volunteers for POPL 2026 Interactive symbolic execution of concurrent programs in a theorem prover
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
Clement Pit-ClaudelPit-Claudel, Clement EPFL Session Chair of Program verification (part of CPP)
Clément Pit-ClaudelPit-Claudel, Clément EPFLSwitzerland Session Chair of Verified Compilation (part of POPL ) 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
Maximilian PopkoPopko, Maximilian Towards Representation Agnostic Probabilistic Programming
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 Session Chair of Rocq Developer Session and Mechanized Metatheory in Rocq (part of RocqPL) Committee Member in Program Committee within the RocqPL-track
Damien PousPous, Damien CNRS Medium-scale automation for proof assistants 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
Ari PrakashPrakash, Ari Northeastern UniversityUnited States Specifying ABIs with Realizability and Type-Preserving Compilation
Abigail PribisovaPribisova, Abigail MPI-SP and MPI-SWS Towards formally secure compilation of verified F* programs against unverified ML contexts
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
Romain PéchouxPéchoux, Romain Université de Lorraine; CNRS; Inria; LORIAFrance Resource-Aware Hybrid Quantum Programming with General Recursion and Quantum Control
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 RUXt: Automatic Compositional Type Safety Refutation Specialisation: Context-Dependent Reasoning in Incorrectness 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 Panel: Work-life balance, service, and teaching
Mathias RabingRabing, Mathias Copenhagen University A Verified Distributed Stream Processing Framework
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
Samar RahmouniRahmouni, Samar Institut Polytechnique de ParisFrance Video Co-Chair in AV Committee for POPL 2026
Abhiramon RajasekharanRajasekharan, Abhiramon The University of Texas at Dallas REGAL: Extracting implicit rules in text using LLMs with logic program feedback
Jan-Paul Ramos-DavilaRamos-Davila, Jan-Paul Boston UniversityUnited States Student Volunteer in Student Volunteers for POPL 2026
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 An Invitation to Quantum Programming Languages 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 Tooling Design and Lessons Learned from Systematic Evaluations of the Preservation of Low-level Security Properties by Compilers with BinSec
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
Mads RehofRehof, Mads University of Copenhagen Functional Quantum Circuit Simulation with Tensor Term Rank Reduction
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 A Design Proposal for GraPPL: Probabilistic Programming with Low-Level, High-Performance GPU 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 Session Chair of Functional Programming (part of POPL ) Quantum Circuits Are Just a Phase Mutability in Quantum Programming Languages
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 A Design for Massively Parallel Gibbs Sampling on the GPU via Static and Dynamic Analysis of Probabilistic Programs
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 Session Chair of Program Analysis (part of POPL ) Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
Exequiel RivasRivas, Exequiel Tallinn University of Technology; Ahrefs Towards formally secure compilation of verified F* programs against unverified ML contexts
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; University of GothenburgSweden 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
Mohamed SabtSabt, Mohamed Univ Rennes, CNRS, IRISA GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses
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 Student Volunteer in Student Volunteers for POPL 2026 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
Basile SchlosserSchlosser, Basile ENS Paris-Saclay Blame-aware Recomposition for Formally Secure Low-level Compiler Backends
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 Tooling Design and Lessons Learned from Systematic Evaluations of the Preservation of Low-level Security Properties by Compilers with BinSec Committee Member in Program Committee within the PriSC-track
Elan SemenovaSemenova, Elan Northeastern University Specifying ABIs with Realizability and Type-Preserving Compilation
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 Panel: Promotion and tenure Panel: Visibility and Impact Welcome from the Organizers 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 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 Panel: Work-life balance, service, and teaching
Xujie SiSi, Xujie University of Toronto RESpecBench: Rigorous Evaluation of Specification Generation with Automated Verification
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 Session Chair of Models 1 (part of VMCAI)
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 Student Volunteer in Student Volunteers for POPL 2026 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, USAUnited 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
Satnam SinghSingh, Satnam HarmonicUnited States Session Chair of Machine Learning (part of POPL ) Industry Panel
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
Sjúrður SkorheimSkorheim, Sjúrður University of Copenhagen Functional Quantum Circuit Simulation with Tensor Term Rank Reduction
Anna SlobodovaSlobodova, Anna Arm 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 HSE UniversityRussia Garbage Collection for Higher Inductive Types
Armando Solar-LezamaSolar-Lezama, Armando Massachusetts Institute of TechnologyUnited States Sequential Monte Carlo Program Synthesis with Refinement Proposals
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 Session Chair of Proof Assistants 2 (part of POPL ) Bounded Sort Polymorphism with Elimination Constraints Committee Member in Program Committee within the POPL -track Session Chair of Compilers (part of CPP) Enhancing universe polymorphism for Rocq: Algebraic universes, consistency checking and variance inference Nested Inductive Types for Rocq and Lean Session with the Rocq Development Team
Simon SpiesSpies, Simon Jane StreetUnited Kingdom PLMW Panel
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
Dario SteinStein, Dario A Welcome to Causal Probabilistic Programming
Dario SteinStein, Dario University of Oxford Typed Abstractions for Causal Probabilistic Programming
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
Elias StormeStorme, Elias KU LeuvenBelgium Calling Conventions for Secure Stack Sharing on CHERI Capability Machines in Practice
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 UniversityChina 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
Xianda SunSun, Xianda University of Cambridge Multi-Agent Systems for Traceable Bayesian Workflow
Hari SundarSundar, Hari Tufts UniversityUnited States DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
Ariadne Si SuoSuo, Ariadne Si University of Oxford Student Volunteer in Student Volunteers for POPL 2026
Tarun SureshSuresh, Tarun University of Illinois, Urbana-ChampaignUnited 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 Panel: Visibility and Impact
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 Efficient Dependency Resolution in IFC-aware Decentralized Programming
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 HSE UniversityRussia Garbage Collection for Higher Inductive Types
Shivanandan Tamil KumaranTamil Kumaran, Shivanandan Imperial College LondonUnited Kingdom An End-to-end Theory for Compositional Symbolic Execution: From Expressive Specifications to SMT Towards a Mechanised Theory of Fully Featured Compositional Symbolic Execution
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
Akane TaniguchiTaniguchi, Akane Institute of Science Tokyo Student Volunteer in Student Volunteers for POPL 2026 Handling the Selection Monad, Uniformly
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
Joshua B. TenenbaumTenenbaum, Joshua B. Massachusetts Institute of TechnologyUnited States Language-Model Probabilistic Programming for Improving Autoformalization via Cycle Consistency and Incremental Type-Checking Sequential Monte Carlo Program Synthesis with Refinement Proposals
Jakob TepeTepe, Jakob TU BraunschweigGermany Oriented Metrics for Bottom-Up Enumerative Synthesis
Jérémy ThibaultThibault, Jérémy EPFL Session Chair of Hardware Security (part of PriSC) Blame-aware Recomposition for Formally Secure Low-level Compiler Backends
Holger ThiesThies, Holger Kyoto University Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
Ramanathan S. ThinniyamThinniyam, Ramanathan S. Uppsala UniversitySweden Session Chair of Concurrency: Testing and Verification (part of POPL ) 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 Student Volunteer in Student Volunteers for POPL 2026 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 Student Volunteer in Student Volunteers for POPL 2026 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 Inria and Max Planck Institute for InformaticsFrance Session Chair of Proof assistants (part of CPP) 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 Session Chair of Proof Assistants (part of POPL ) 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 IndependentRomania Staging Effect Handlers for Modular Search
Caroline TrippelTrippel, Caroline Stanford University Hardware-Software Contracts for High Assurance with Applications to Side-Channel Security
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 SinicaTaiwan 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
Emma TyeTye, Emma University of StrathclydeUnited Kingdom Student Volunteer in Student Volunteers for POPL 2026
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 Grammar-Constrained LLM Generation for Reliable and Efficient Probabilistic Program Synthesis
Mateo UldemolinsUldemolins, Mateo DIENS Graphix: An Open-Source Compiler and Simulator for Measurement-Based Quantum Computation The MBQCert Project
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 Session Chair of Monads and Effects (part of POPL ) 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
Sören van der Wallvan der Wall, Sören TU BraunschweigGermany Decompiling for Constant-Time Analysis
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
Thomas Van StrydonckVan Strydonck, Thomas KULeuven Calling Conventions for Secure Stack Sharing on CHERI Capability Machines in Practice
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
Gabriele VanoniVanoni, Gabriele IRIF, Université Paris Cité Towards Compiling Higher-Order Programs to Bayesian Networks
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 Session Chair of Keynote (part of PriSC) Committee Member in Steering Committee within the PriSC-track Co-chair in Program Committee within the PriSC-track
Niki VazouVazou, Niki IMDEA Software Institute Closing Chair in Program Committee within the WITS-track
Joey Velez-GinorioVelez-Ginorio, Joey University of PennsylvaniaUnited States 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 LondonUnited Kingdom Committee Member in Program Committee within the TPSA-track Committee Member in Organizing Committee within the TPSA-track
Thomas VinetVinet, Thomas Université de Lorraine, Inria, LORIA Resource-Aware Hybrid Quantum Programming with General Recursion and Quantum Control
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
David WalkerWalker, David Princeton UniversityUnited States Monte Carlo Analysis of Probabilistic Programs
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
Meng WangWang, Meng University of BristolUnited Kingdom Embedding a Type-safe Quantum-Lambda Calculus in Haskell Session Chair of Semantics and applications (part of PEPM)
Qian (Andy) WangWang, Qian (Andy) ETH Zurich and Imperial College LondonUnited Kingdom Miri: Practical Undefined Behavior Detection for Rust
Theo WangWang, Theo University of Cambridge, University of OxfordUnited Kingdom Student Volunteer in Student Volunteers for POPL 2026 Typed Abstractions for Causal Probabilistic Programming
Xiaoyan WangWang, Xiaoyan Massachusetts Institute of TechnologyUnited States Probabilistic Programming with Vectorized Programmable Inference Sequential Monte Carlo Program Synthesis with Refinement Proposals
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. BloombergUnited States 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 Session Chair of Security and Privacy (part of POPL ) Typing Strictness Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach Associate Chair in Program Committee within the POPL -track SIGPLAN CARES Introduction Panel: Visibility and Impact On building a successful research group Speaker in Speakers 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
Pierre WilkeWilke, Pierre CentraleSupélec Modular and automatic formal verification of a RISC-V processor with security mechanisms
Hans WinderixWinderix, Hans KU LeuvenBelgium Committee Member in Program Committee within the PriSC-track
Tobias WinklerWinkler, Tobias RWTH Aachen UniversityGermany Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops Probabilistic Programming Meets Automata Theory: Exact Inference using Weighted Automata Verifying Sampling Algorithms via Distributional Invariants
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 Towards formally secure compilation of verified F* programs against unverified ML contexts
Spencer WoolfsonWoolfson, Spencer Carnegie Mellon University A Certifying Proof Assistant for Synthetic Mathematics in Lean
Kim WorrallWorrall, Kim The University of Edinburgh Student Volunteer in Student Volunteers for POPL 2026
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 Student Volunteer in Student Volunteers for POPL 2026 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 Session Chair of Types 3 (part of POPL ) Hyperfunctions: Communicating Continuations Handling Higher-Order Effectful Operations with Judgemental Monadic Laws Bayesian Separation Logic Committee Member in Program Committee within the POPL -track Revisiting the Evolution of Effects (Invited Talk) Panel: Promotion and tenure
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 Session Chair of Keynote (part of PEPM) Closing 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
Xingyu XieXie, Xingyu MPI-SPChina Student Volunteer in Student Volunteers for POPL 2026 Modular Verification of Probabilistic Constant-Time
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 Typed Abstractions for Causal Probabilistic Programming 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)
Poyraz YılanYılan, Poyraz Inria Paris & Airbus Student Volunteer in Student Volunteers for POPL 2026
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
Hyeongseo YooYoo, Hyeongseo Seoul National University and Samsung Electronics Interrupt-Aware Variable Analysis for SSD Firmware
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 Peking UniversityChina 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 Language-Model Probabilistic Programming for Improving Autoformalization via Cycle Consistency and Incremental Type-Checking Incremental Density Computation for Efficient Programmable Inference 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 Save Time and Mechanize
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 Opening Address 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 Panel: Promotion and tenure
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 Day closing DafnyPro: LLM-Assisted Automated Verification for Dafny Programs Day opening 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
Zhiyuan ZhangZhang, Zhiyuan Decompiling for Constant-Time Analysis
A. ZhaoZhao, A. Princeton Monte Carlo Analysis of Probabilistic Programs
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 University of California, San Diego 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
Francille ZhuangZhuang, Francille Purdue University Ariadne: Automatically Tuning Generator Weights Using Dynamic Sampling
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 Session Chair of Concurrency: Models (part of POPL ) 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
Daniel ZilkenZilken, Daniel Verifying Sampling Algorithms via Distributional Invariants
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 Student Volunteer in Student Volunteers for POPL 2026 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 (1158)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia