POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

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.

Dates
Tracks

This program is tentative and subject to change.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Wed 14 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:00 - 10:00
KeynotePOPL at Nef
09:00
60m
Keynote
Medium-scale automation for proof assistants
POPL
10:30 - 12:10
Program AnalysisPOPL at Dortoirs
10:30
25m
Talk
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
25m
Talk
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
25m
Talk
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
25m
Talk
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
Functional Programming POPL at Nef
10:30
25m
Talk
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
25m
Talk
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
25m
Talk
Hyperfunctions: Communicating Continuations
POPL
Donnacha Oisín Kidney Imperial College London, Nicolas Wu Imperial College London
DOI Pre-print
11:45
25m
Talk
Lazy Linearity for a Core Functional Language
POPL
Rodrigo Mesquita Well-Typed LLP, Bernardo Toninho Instituto Superior Técnico - University of Lisbon
DOI Pre-print
10:30 - 12:10
Automata 1POPL at Réfectoire
10:30
25m
Talk
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
25m
Talk
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
25m
Talk
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
25m
Talk
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
Quantum 1POPL at Dortoirs
14:00
25m
Talk
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
25m
Talk
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
25m
Talk
Qudit Quantum Programming with Projective Cliffords
POPL
Jennifer Paykin University of Vermont, Sam Winnick Simon Fraser University; University of Waterloo
DOI
15:15
25m
Talk
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
Types 1POPL at Nef
14:00
25m
Talk
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
25m
Talk
Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems
POPL
Joseph Zullo Purdue University
DOI
14:50
25m
Talk
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
25m
Talk
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
14:00 - 15:40
Concurrency: ModelsPOPL at Réfectoire
14:00
25m
Talk
Arbitration-Free Consistency Is Available (and Vice Versa)
POPL
Hagit Attiya Technion - Israel Institute of Technology, Constantin Enea LIX, CNRS, Ecole Polytechnique, Enrique Román-Calvo University of Freiburg
DOI
14:25
25m
Talk
ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
POPL
Thibaut Pérami University of Cambridge, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Zongyuan Liu Aarhus University, Nils Lauermann University of Cambridge, Alasdair Armstrong University of Cambridge, Peter Sewell University of Cambridge
DOI
14:50
25m
Talk
Consistent Updates for Scalable Microservices
POPL
Devora Chait-Roth New York University, Kedar Namjoshi Nokia Bell Labs, Thomas Wies New York University
DOI
15:15
25m
Talk
Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
POPL
Thomas Haas TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León Huawei Dresden Research Center, Andrés Lomelí Garduño Huawei Dresden Research Center
DOI
16:10 - 17:25
Decision ProceduresPOPL at Dortoirs
16:10
25m
Talk
Characterizing Sets of Theories That Can Be Disjointly Combined
POPL
Benjamin Przybocki Carnegie Mellon University, Guilherme V. Toledo Bar-Ilan University, Yoni Zohar
DOI
16:35
25m
Talk
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
25m
Talk
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
Synthesis 1POPL at Nef
16:10
25m
Talk
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
25m
Talk
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
25m
Talk
Oriented Metrics for Bottom-Up Enumerative Synthesis
POPL
Roland Meyer TU Braunschweig, Jakob Tepe TU Braunschweig
DOI
16:10 - 17:25
Machine LearningPOPL at Réfectoire
16:10
25m
Talk
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
25m
Talk
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
25m
Talk
Fuzzing Guided by Bayesian Program Analysis
POPL
Yifan Zhang Peking University, Xin Zhang Peking University
DOI

Thu 15 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

10:20 - 12:00
SRC TalksPOPL at Dortoirs
10:20 - 12:00
Concurrency: Testing and VerificationPOPL at Nef
10:20
25m
Talk
(TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection
POPL
Alexandre Moine New York University, Arthur Charguéraud Inria, François Pottier Inria
10:45
25m
Talk
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
25m
Talk
Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic
POPL
Clément Allain INRIA, Gabriel Scherer Université Paris Cité - Inria - CNRS
DOI
11:35
25m
Talk
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
Separation LogicPOPL at Réfectoire
10:20
25m
Talk
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
25m
Talk
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
25m
Talk
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
25m
Talk
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
Category TheoryPOPL at Dortoirs
14:00
25m
Talk
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
25m
Talk
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
25m
Talk
Higher-Order Behavioural Conformances via Fibrations
POPL
Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg
DOI
15:15
25m
Talk
What Is a Monoid?
POPL
Paul Blain Levy University of Birmingham, Morgan Rogers University Sorbonne Paris 13
DOI
14:00 - 15:40
Proof AssistantsPOPL at Nef
14:00
25m
Talk
A Lazy, Concurrent Convertibility Checker
POPL
Nathanaëlle Courant OCamlPro, Xavier Leroy Collège de France - PSL University
DOI
14:25
25m
Talk
Canonicity for Indexed Inductive-Recursive Types
POPL
András Kovács University of Gothenburg and Chalmers University of Technology
DOI
14:50
25m
Talk
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
25m
Talk
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
Program Logics and Semantic FrameworksPOPL at Réfectoire
14:00
25m
Talk
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
25m
Talk
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
25m
Talk
JAX Autodiff from a Linear Logic Perspective
POPL
Giulia Giusti ENS Lyon, Michele Pagani ENS Lyon
DOI
15:15
25m
Talk
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
Synthesis 2POPL at Dortoirs
16:10
25m
Talk
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
25m
Talk
Parameterized Infinite-State Reactive Synthesis
POPL
Benedikt Maderbacher Graz University of Technology, Roderick Bloem Graz University of Technology
DOI
16:10 - 17:00
Verified CompilationPOPL at Nef
16:10
25m
Talk
A Family of Sims with Diverging Interests
POPL
Nicolas Chappe CNRS - Verimag
DOI
16:35
25m
Talk
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
Security and PrivacyPOPL at Réfectoire
16:10
25m
Talk
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
25m
Talk
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 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

10:30 - 12:10
Specification and Verification MethodsPOPL at Dortoirs
10:30
25m
Talk
Abstraction Functions as Types
POPL
Harrison Grodin Carnegie Mellon University, Runming Li Carnegie Mellon University, Robert Harper Carnegie Mellon University
DOI
10:55
25m
Talk
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
25m
Talk
Stateful Differential Operators for Incremental Computing
POPL
DOI
11:45
25m
Talk
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
Concurrency: Types, Logics, and LibrariesPOPL at Nef
10:30
25m
Talk
All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
POPL
Alexandre Moine New York University, Sam Westrick New York University, Joseph Tassarotti New York University
DOI
10:55
25m
Talk
A Verified High-Performance Composable Object Library for Remote Direct Memory Access
POPL
Guillaume Ambal , George Hodgkins University of Colorado, Mark Madler University of Colorado, Gregory Chockler University of Surrey, Brijesh Dongol University of Surrey, Joe Izraelevitz University of Colorodo Boulder, Azalea Raad Imperial College London, Viktor Vafeiadis MPI-SWS
DOI
11:20
25m
Talk
DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
POPL
Aleksandr Fedchin Tufts University, Antero Mejr Tufts University, Hari Sundar Tufts University, Jeffrey S. Foster Tufts University
DOI
11:45
25m
Talk
TypeDis: A Type System for Disentanglement
POPL
Alexandre Moine New York University, Stephanie Balzer Carnegie Mellon University, Alex Xu Carnegie Mellon University, Sam Westrick New York University
DOI
10:30 - 12:10
Types 2POPL at Réfectoire
10:30
25m
Talk
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
25m
Talk
Quotient Polymorphism
POPL
Brandon Hewer , Graham Hutton University of Nottingham
DOI
11:20
25m
Talk
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
25m
Talk
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
Monads and EffectsPOPL at Dortoirs
14:00
25m
Talk
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
25m
Talk
Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
POPL
Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London
DOI
14:50
25m
Talk
Rows and Capabilities as Modal Effects
POPL
Wenhao Tang The University of Edinburgh, Sam Lindley University of Edinburgh
DOI
15:15
25m
Talk
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
Probabilistic ProgrammingPOPL at Nef
14:00
25m
Talk
Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
POPL
Sangho Lim KAIST, Hyoungjin Lim KAIST, Wonyeol Lee POSTECH, Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University, Hongseok Yang KAIST
DOI
14:25
25m
Talk
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
POPL
Noam Zilberstein Cornell University, Alexandra Silva Cornell University, Joseph Tassarotti New York University
DOI
14:50
25m
Talk
Probabilistic Programming with Vectorized Programmable Inference
POPL
McCoy Reynolds Becker MIT, Mathieu Huot MIT, George Matheos Massachusetts Institute of Technology, Xiaoyan Wang Massachusetts Institute of Technology, Karen Chung Massachusetts Institute of Technology, Colin Smith Massachusetts Institute of Technology, Sam Ritchie Massachusetts Institute of Technology, Rif A. Saurous Google, Alexander K. Lew Yale University, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology
DOI
15:15
25m
Talk
Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
POPL
Davide Barbarossa University of Bath, Paolo Pistone Université Claude Bernard Lyon 1
DOI
14:00 - 15:40
Proof Assistants 2POPL at Réfectoire
14:00
25m
Talk
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
25m
Talk
Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach
POPL
Yiyun Liu University of Pennsylvania, Stephanie Weirich University of Pennsylvania
DOI
14:50
25m
Talk
Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally
POPL
Yann Leray Nantes Université; Inria, Théo Winterhalter INRIA
DOI
15:15
25m
Talk
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
Types 3POPL at Dortoirs
16:10
25m
Talk
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
25m
Talk
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
25m
Talk
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
Automata 2POPL at Nef
16:10
25m
Talk
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
25m
Talk
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
25m
Talk
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
Quantum 2POPL at Réfectoire
16:10
25m
Talk
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
25m
Talk
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
25m
Talk
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