Overview
POPL 2026 will host an ACM Student Research Competition, where undergraduate and graduate students can present their original research before a panel of judges and conference attendees. This year’s competition will consist of three rounds:
-
Round 1, Extended abstract: All students are encouraged to submit an extended abstract outlining their research. The submission should be up to three pages using “\documentclass[acmsmall,nonacm]{acmart}”.
-
Round 2, Poster at POPL: Based on the submissions, a panel of judges will select the most promising entrants to participate in a poster session at POPL. In the poster session, students will be able to interact with POPL attendees and judges. After the poster session, three finalists in each category (graduate/undergraduate) will be selected to advance to the next round.
-
Round 3, Oral presentation at POPL: The last round will consist of a short oral live presentation at POPL to compete for the final awards in each category. This round will also select an overall winner who will advance to the ACM SRC Grand Finals.
Call for Submissions
POPL invites students to participate in the Student Research Competition in order to present their research and get feedback from prominent members of the programming language research community. Please submit your extended abstracts through HotCRP: https://popl26src.hotcrp.com
Submissions must be original research that is not already published at POPL or another conference or journal. One of the goals of the SRC is to give students feedback on ongoing, unpublished work. Furthermore, the submission must be authored solely by the student. If the work is collaborative with others and/or part of a larger group project, the submission should make clear what the student’s role was and should focus on that portion of the work.
Each submission should include the student author’s name and e-mail address; institutional affiliation; research advisor’s name; ACM student member number; category (undergraduate or graduate); research title; and an extended abstract addressing the following:
-
What problem does the submitted work try to solve and why is that problem important?
-
What is the state-of-the-art in related areas and how the submitted work departs from others?
-
Sufficient background information and details of the presented approach to allow POPL audiences to appreciate the presented work.
The submission should be up to three pages using ‘\documentclass[acmsmall,nonacm]{acmart}’. The submission does not itself need to start with an “abstract”; the introduction can start immediately after the author list. Reference lists do not count towards the three-page limit. You may write appendices after the three-page limit, but please be noted that the committee is not required to read them.
This year, we will have two review cycles. For each submission, one of the following decisions will be made:
-
Accept: submissions that proceed to the next round unconditionally.
-
Conditional Accept: submissions that receive revision suggestions from the PC members. Authors will have 3 days to revise the submission accordingly and then resubmit. The revised submissionss will then be re-evaluated, and either accepted or rejected.
-
Reject: submissions that will not proceed to the next round.
Prizes
The top three graduate and the top three undergraduate winners will receive prizes of $500, $300, and $200, respectively.
-
All six winners will receive award medals and a one-year complimentary ACM student membership, including a subscription to ACM’s Digital Library.
-
The names of the winners will be posted on the SRC website.
-
The first-place winners of the SRC will be invited to participate in the ACM SRC Grand Finals, an online round of competitions among the winners of other conference-hosted SRCs.
Eligibility
The SRC is open to both undergraduate (not in a PhD/master’s program) and graduate students (in a PhD/master’s program). Upon submission, entrants must be enrolled as a student at their universities and be current ACM student members.
Furthermore, there are some constraints on what kind of work may be submitted:
-
Previously published work: Submissions should consist of original work (not yet accepted for publication). If the work is a continuation of previously published work, the submission should focus on the contribution over what has already been published. We encourage students to see this as an opportunity to get early feedback and exposure for the work they plan to submit to the next POPL.
-
Collaborative work: Graduate students are encouraged to submit work they have been conducting in collaboration with others, including advisors, internship mentors, or other students. However, graduate submissions are individual, so they must focus on the contributions of the student.
-
Team submissions: Team projects will be only accepted from undergrads. One person should be designated by the team to make the oral presentation. If a graduate student is part of a group research project and wishes to participate in an SRC, they can submit and present their individual contribution to the group research project.
This program is tentative and subject to change.
Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:00 | |||
09:00 60mKeynote | Medium-scale automation for proof assistants POPL Damien Pous CNRS | ||
10:30 - 12:10 | |||
10:30 25mTalk | A Modular Static Cost Analysis for GPU Warp-Level Parallelism POPL Gregory Blike University of Massachusetts at Boston, Hannah Zicarelli University of Massachusetts at Boston, Udaya Sathiyamoorthy University of Massachusetts at Boston, Julien Lange Royal Holloway University of London, Tiago Cogumbreiro University of Massachusetts at Boston DOI | ||
10:55 25mTalk | ChiSA: Static Analysis for Lightweight Chisel Verification POPL Jiacai Cui Nanjing University, Qinlin Chen Nanjing University, Zhongsheng Zhan Nanjing University, Tian Tan Nanjing University, Yue Li Nanjing University DOI | ||
11:20 25mTalk | Miri: Practical Undefined Behavior Detection for Rust POPL Ralf Jung ETH Zurich, Benjamin Kimock Lansweeper NV, Christian Poveda Unaffiliated, Eduardo Sánchez Muñoz Unaffiliated, Oli Scherer Unaffiliated, Qian (Andy) Wang ETH Zurich and Imperial College London DOI | ||
11:45 25mTalk | Piecewise Analysis of Probabilistic Programs via k-Induction POPL Tengshun Yang Institute of Software at Chinese Academy of Sciences, Shenghua Feng Institute of Software at Chinese Academy of Sciences, Hongfei Fu Shanghai Jiao Tong University, Naijun Zhan Peking University; Zhongguancun Lab, Jingyu Ke Shanghai Jiao Tong University, Shiyang Wu Shanghai Jiao Tong University DOI | ||
10:30 - 12:10 | |||
10:30 25mTalk | Domain-Theoretic Semantics for Functional Logic Programming POPL Eddie Jones University of Bristol, Samson Main University of Bristol, Celia Mengyue Li University of Bristol, Jonathan Marriott University of Bristol, Alex Kavvos University of Bristol DOI | ||
10:55 25mTalk | Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks POPL Michael Lee University of Cambridge, UK, Ningning Xie University of Toronto, Oleg Kiselyov Tohoku University, Jeremy Yallop University of Cambridge DOI | ||
11:20 25mTalk | Hyperfunctions: Communicating Continuations POPL DOI Pre-print | ||
11:45 25mTalk | Lazy Linearity for a Core Functional Language POPL DOI Pre-print | ||
10:30 - 12:10 | |||
10:30 25mTalk | Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures POPL C. Aiswarya Chennai Mathematical Institute, Pascal Baumann MPI-SWS, Prakash Saivasan Institute of Mathematical Sciences, Lia Schütze MPI-SWS, Georg Zetzsche MPI-SWS DOI | ||
10:55 25mTalk | Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications POPL Aurèle Barrière EPFL, Victor Deng EPFL; École Normale Supérieure - PSL - CNRS, Clément Pit-Claudel EPFL DOI | ||
11:20 25mTalk | Network Change Validation with Relational NetKAT POPL Han Xu Princeton University, Zachary Kincaid Princeton University, Ratul Mahajan University of Washington, Intentionet, David Walker DOI | ||
11:45 25mTalk | Parameterized Verification of Quantum Circuits POPL Parosh Aziz Abdulla Uppsala University; Mälardalen University, Yu-Fang Chen Academia Sinica, Michal Hečko Brno University of Technology, Lukáš Holík Brno University of Technology; Aalborg University, Ondřej Lengál Brno University of Technology, Jyun-Ao Lin National Taipei University of Technology, Ramanathan S. Thinniyam Uppsala University DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | An Expressive Assertion Language for Quantum Programs POPL Bonan Su Tsinghua University, Yuan Feng Tsinghua University, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University, Li Zhou Institute of Software at Chinese Academy of Sciences DOI | ||
14:25 25mTalk | Hadamard-Pi: Equational Quantum Programming POPL Wang Fang University of Edinburgh, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark DOI | ||
14:50 25mTalk | Qudit Quantum Programming with Projective Cliffords POPL DOI | ||
15:15 25mTalk | RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing POPL Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University, Emanuele D'Osualdo University of Konstanz DOI Pre-print | ||
14:00 - 15:40 | |||
14:00 25mTalk | Extensible Data Types with Ad-Hoc Polymorphism POPL Matthew Toohey University of Toronto, Yanning Chen University of Toronto, Ara Jamalzadeh University of Toronto, Ningning Xie University of Toronto DOI | ||
14:25 25mTalk | Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems POPL Joseph Zullo Purdue University DOI | ||
14:50 25mTalk | Local Contextual Type Inference POPL Xu Xue University of Hong Kong, Chen Cui University of Hong Kong, Shengyi Jiang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
15:15 25mTalk | Typing Strictness POPL Daniel Sainati University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Stephanie Weirich University of Pennsylvania DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Characterizing Sets of Theories That Can Be Disjointly Combined POPL DOI | ||
16:35 25mTalk | Context-Free-Language Reachability for Almost-Commuting Transition Systems POPL Nikhil Pimpalkhare Princeton University, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison DOI | ||
17:00 25mTalk | Determination Problems for Orbit Closures and Matrix Groups POPL Rida Ait El Manssour University of Oxford, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS, Anton Varonka TU Wien, James Worrell University of Oxford DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages POPL Zhentao Ye Peking University, Ruyi Ji Peking University, Yingfei Xiong Peking University, Xin Zhang Peking University DOI | ||
16:35 25mTalk | Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling POPL Doyoon Lee Seoul National University, Woosuk Lee Hanyang University, Kwangkeun Yi Seoul National University DOI | ||
17:00 25mTalk | Oriented Metrics for Bottom-Up Enumerative Synthesis POPL DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models POPL Shaan Nagy University of California at San Diego, Timothy Zhou , Nadia Polikarpova University of California at San Diego, Loris D'Antoni University of California at San Diego DOI | ||
16:35 25mTalk | Compiling to Linear Neurons POPL Joey Velez-Ginorio , Nada Amin Harvard University, Konrad Kording University of Pennsylvania, Steve Zdancewic University of Pennsylvania DOI | ||
17:00 25mTalk | Fuzzing Guided by Bayesian Program Analysis POPL DOI | ||
Thu 15 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
10:20 - 12:00 | |||
10:20 25mTalk | (TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection POPL | ||
10:45 25mTalk | Verifying Almost-Sure Termination for Randomized Distributed Algorithms POPL Constantin Enea LIX, CNRS, Ecole Polytechnique, Rupak Majumdar MPI-SWS, Harshit Jitendra Motwani MPI-SWS, V.R. Sathiyanarayana MPI-SWS DOI | ||
11:10 25mTalk | Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic POPL DOI | ||
11:35 25mTalk | The Complexity of Testing Message-Passing Concurrency POPL Zheng Shi National University of Singapore, Lasse Møldrup Aarhus University, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University DOI Pre-print | ||
10:20 - 12:00 | |||
10:20 25mTalk | A Relational Separation Logic for Effect Handlers POPL Paulo Emílio de Vilhena Imperial College London, Simcha van Collem Radboud University Nijmegen, Ines Wright Aarhus University, Robbert Krebbers Radboud University Nijmegen DOI | ||
10:45 25mTalk | Bayesian Separation Logic POPL Shing Hin Ho Imperial College London, Nicolas Wu Imperial College London, Azalea Raad Imperial College London DOI Pre-print | ||
11:10 25mTalk | Cryptis: Cryptographic Reasoning in Separation Logic POPL Arthur Azevedo de Amorim Rochester Institute of Technology, Amal Ahmed Northeastern University, USA, Marco Gaboardi Boston University DOI | ||
11:35 25mTalk | Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions POPL Neta Elad Tel Aviv University, Adithya Murali University of Wisconsin, Sharon Shoham Tel Aviv University DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | Classical Notions of Computation and the Hasegawa-Thielecke Theorem POPL Éléonore Mangel Univ. Paris Cité - CNRS - Inria, Paul-André Melliès Univ. Paris Cité - CNRS - Inria, Guillaume Munch-Maccagnoni INRIA DOI | ||
14:25 25mTalk | From Semantics to Syntax: A Type Theory for Comprehension Categories POPL Niyousha Najmaei École Polytechnique, Niels van der Weide Radboud University, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University DOI | ||
14:50 25mTalk | Higher-Order Behavioural Conformances via Fibrations POPL Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg DOI | ||
15:15 25mTalk | What Is a Monoid? POPL DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | A Lazy, Concurrent Convertibility Checker POPL DOI | ||
14:25 25mTalk | Canonicity for Indexed Inductive-Recursive Types POPL András Kovács University of Gothenburg and Chalmers University of Technology DOI | ||
14:50 25mTalk | Coco: Corecursion with Compositional Heterogeneous Productivity POPL Jaewoo Kim Seoul National University, Yeonwoo Nam Seoul National University, Chung-Kil Hur Seoul National University DOI | ||
15:15 25mTalk | Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation POPL Marcus Rossel Barkhausen Institut; TU Darmstadt, Rudi Schneider TU Berlin, Thomas Koehler ICube Lab - CNRS - Université de Strasbourg, Michel Steuwer TU Berlin, Andrés Goens TU Darmstadt DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | A Logic for the Imprecision of Abstract Interpretations POPL Marco Campion Inria Paris - ENS - Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona, Caterina Urban Inria Paris - ENS - Université PSL DOI | ||
14:25 25mTalk | Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment POPL David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University, Runming Li Carnegie Mellon University DOI | ||
14:50 25mTalk | JAX Autodiff from a Linear Logic Perspective POPL DOI | ||
15:15 25mTalk | U-Turn: Enhancing Incorrectness Analysis by Reversing Direction POPL Flavio Ascari University of Konstanz, Roberto Bruni University of Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy, Azalea Raad Imperial College London DOI | ||
16:10 - 17:00 | |||
16:10 25mTalk | Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers POPL Xuanyu Peng University of California at San Diego, Dominic Kennedy University of Utah, Yuyou Fan University of Utah, Ben Greenman University of Utah, USA, John Regehr University of Utah, Loris D'Antoni University of California at San Diego DOI | ||
16:35 25mTalk | Parameterized Infinite-State Reactive Synthesis POPL DOI | ||
16:10 - 17:00 | |||
16:10 25mTalk | A Family of Sims with Diverging Interests POPL Nicolas Chappe CNRS - Verimag DOI | ||
16:35 25mTalk | Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation POPL Niklas Mück MPI-SWS, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Michael Sammler Institute of Science and Technology Austria DOI Pre-print | ||
16:10 - 17:00 | |||
16:10 25mTalk | Dependent Coeffects for Local Sensitivity Analysis POPL Victor Sannier Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL, Patrick Baillot Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL DOI | ||
16:35 25mTalk | Security Reasoning via Substructural Dependency Tracking POPL Hemant Gouni Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA, Jonathan Aldrich Carnegie Mellon University DOI Pre-print | ||
Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:00 | |||
09:00 60mKeynote | Hardware-Software Contracts for High Assurance with Applications to Side-Channel Security POPL Caroline Trippel Stanford University | ||
10:30 - 12:10 | |||
10:30 25mTalk | Abstraction Functions as Types POPL Harrison Grodin Carnegie Mellon University, Runming Li Carnegie Mellon University, Robert Harper Carnegie Mellon University DOI | ||
10:55 25mTalk | Foundational Multi-Modal Program Verifiers POPL Vladimir Gladshtein , George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore, Vitaly Kurin Neapolis University Pafos, Ilya Sergey National University of Singapore DOI | ||
11:20 25mTalk | Stateful Differential Operators for Incremental Computing POPL DOI | ||
11:45 25mTalk | The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs POPL Frank Schüssele University of Freiburg, Matthias Zumkeller University of Freiburg, Miriam Lagunes-Rochin University of Freiburg, Dominik Klumpp LIX - CNRS - École Polytechnique; University of Freiburg DOI | ||
10:30 - 12:10 | |||
10:30 25mTalk | Di- is for Directed: First-Order Directed Type Theory via Dinaturality POPL Andrea Laretto Tallinn University of Technology, Fosco Loregian Tallinn University of Technology, Niccolò Veltri IT University of Copenhagen DOI | ||
10:55 25mTalk | Quotient Polymorphism POPL DOI | ||
11:20 25mTalk | The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types POPL Chun Yin Chau HKUST (The Hong Kong University of Science and Technology), Lionel Parreaux Hong Kong University of Science and Technology DOI | ||
11:45 25mTalk | Welterweight Go: Boxing, Structural Subtyping, and Generics POPL Raymond Hu Queen Mary University of London, Julien Lange Royal Holloway University of London, Bernardo Toninho Instituto Superior Técnico - University of Lisbon, Philip Wadler University of Edinburgh, Robert Griesemer Google, Keith Randall Google DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories POPL Ohad Kammar University of Edinburgh, Jack Liell-Cock University of Oxford, Sam Lindley University of Edinburgh, Cristina Matache University of Edinburgh, Sam Staton University of Oxford DOI | ||
14:25 25mTalk | Handling Higher-Order Effectful Operations with Judgemental Monadic Laws POPL DOI | ||
14:50 25mTalk | Rows and Capabilities as Modal Effects POPL DOI | ||
15:15 25mTalk | The Relative Monadic Metalanguage POPL Jack Liell-Cock University of Oxford, Zev Shirazi University of Oxford, Sam Staton University of Oxford DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | AdapTT: Functoriality for Dependent Type Casts POPL Arthur Adjedj ENS Paris Saclay, Université Paris-Saclay, Meven Lennon-Bertrand Inria – Université Paris Cité, Thibaut Benjamin Université Paris-Saclay, CEA, List, Kenji Maillard Inria DOI | ||
14:25 25mTalk | Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach POPL DOI | ||
14:50 25mTalk | Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally POPL DOI | ||
15:15 25mTalk | Normalisation for First-Class Universe Levels POPL Nils Anders Danielsson University of Gothenburg, Naïm Camille Favier Chalmers University of Technology and University of Gothenburg, Ondřej Kubánek Chalmers University of Technology DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | A Complementary Approach to Incorrectness Typing POPL Celia Mengyue Li University of Bristol, Sophie Pull University of Bristol, Steven Ramsay University of Bristol DOI | ||
16:35 25mTalk | A Synthetic Reconstruction of Multiparty Session Types POPL David Castro-Perez University of Kent, Francisco Ferreira Royal Holloway, University of London, Sung-Shik Jongmans University of Groningen DOI | ||
17:00 25mTalk | Bounded Sort Polymorphism with Elimination Constraints POPL Johann Rosain ENS Lyon, Tomás Diaz University of Chile, Kenji Maillard Inria, Matthieu Sozeau Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile, Théo Winterhalter INRIA DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Counting and Sampling Traces in Regular Languages POPL Alexis de Colnet TU Wien, Kuldeep S. Meel University of Toronto, Umang Mathur National University of Singapore DOI Pre-print | ||
16:35 25mTalk | Parametrised Verification of Intel-x86 Programs POPL Parosh Aziz Abdulla Uppsala University; Mälardalen University, Mohamed Faouzi Atig Uppsala University, Ahmed Bouajjani Université Paris Cité, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan Institute of Mathematical Sciences DOI | ||
17:00 25mTalk | General Decidability Results for Systems with Continuous Counters POPL A. R. Balasubramanian Technical University of Munich, Matthew Hague Royal Holloway University of London, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Generating Compilers for Qubit Mapping and Routing POPL Abtin Molavi University of Wisconsin-Madison, Amanda Xu University of Wisconsin-Madison, Ethan Cecchetti University of Wisconsin-Madison, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison DOI | ||
16:35 25mTalk | On Circuit Description Languages, Indexed Monads, and Resource Analysis POPL Ken Sakayori University of Tokyo, Andrea Colledan University of Bologna; Centre Inria d’Université Côte d’Azur, Ugo Dal Lago University of Bologna; Centre Inria d’Université Côte d’Azur DOI | ||
17:00 25mTalk | Quantum Circuits Are Just a Phase POPL Chris Heunen University of Edinburgh, Louis Lemonnier University of Edinburgh, Christopher McNally Massachusetts Institute of Technology, Alex Rice University of Edinburgh DOI | ||