Peek-A-Boo - POPL 2025

VenueCurtis Hotel Denver

Room namePeek-A-Boo

Floor2

Capacity300

Room InformationNo extra information available

Program

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT-07:00) Mountain Time (US & Canada).

Use conference time zone: (GMT-07:00) Mountain Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

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

Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:30	First sessionLAFI at Peek-A-Boo

09:00 5m Talk		Welcome LAFI Matthijs Vákár Utrecht University, Atılım Güneş Baydin University of Oxford
09:06 20m Industry talk		Industry Talk: Basis AI LAFI
09:27 15m Talk		Towards Symbolic Execution for Probability and Non-determinism LAFI Jack Czenszak Northeastern University, John Li Northeastern University, Steven Holtzen Northeastern University
09:43 15m Talk		Lazy Knowledge Compilation for Discrete PPLs LAFI Maddy Bowers Massachusetts Institute of Technology, Alexander K. Lew Massachusetts Institute of Technology, Joshua B. Tenenbaum Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology
09:59 15m Talk		Reasoning About Sampling Without Sampling: Atomic Machines for Contextual Equivalence in Probabilistic Programs LAFI Anthony D'Arienzo University of Illinois and Sandia National Laboratories, Jon Aytac Sandia National Laboratories
10:15 15m Talk		Exact Inference for Nested Discrete Probabilistic Programs LAFI Francesco Pontiggia TU Wien, Ezio Bartocci TU Wien, Michele Chiari TU Wien

11:00 - 12:30	Second sessionLAFI at Peek-A-Boo

11:00 40m Talk		Invited talk: A Fast and Differentiable Tokamak Transport Simulator in JAX LAFI Jonathan Citrin Google Deepmind
11:41 15m Talk		Data-Parallel Differentiation by Optic Composition LAFI Paul Wilson University of Southampton, Fabio Zanasi University College London
11:57 15m Talk		A Domain-Specific PPL for Reasoning about Reasoning (or: a memo on memo) LAFI Kartik Chandra MIT, Tony Chen MIT, Joshua B. Tenenbaum Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology
12:13 15m Talk		Data-oriented Design for Differentiable, Probabilistic Programming LAFI Owen Lynch University of Oxford, Maria-Nicoleta Craciun University of Oxford, Younesse Kaddar University of Oxford, Sam Staton University of Oxford

14:00 - 15:30	Third sessionLAFI at Peek-A-Boo

14:00 40m Talk		Invited talk: Modern Bayesian experimental design LAFI Desi R. Ivavona University of Oxford
14:41 15m Talk		Partially Evaluating Higher-Order Probabilistic Programs without Stochastic Recursion to Graphical Models LAFI Christian Weilbach University of British Columbia, Frank Wood University of Oxford
14:57 15m Talk		NP-NUTS: A Nonparametric No-U-Turn Sampler LAFI Maria-Nicoleta Craciun University of Oxford, C.-H. Luke Ong NTU, Sam Staton University of Oxford, Matthijs Vákár Utrecht University
15:13 15m Talk		Sandwood: Runtime Adaptable Probabilistic Programming for Java LAFI Daniel Goodman Oracle Labs, Adam Pocock Oracle Labs, Natalia Kosilova Oracle Labs

16:00 - 17:30	Fourth sessionLAFI at Peek-A-Boo

16:00 15m Talk		Semantics of the memo Probabilistic Programming Language LAFI Kartik Chandra MIT, Nada Amin Harvard University, Yizhou Zhang University of Waterloo
16:16 15m Talk		State Space Model Programming in Turing.jl LAFI Tim Hargreaves Department of Engineering, University of Cambridge, Qing Li Department of Engineering, University of Cambridge, Charles Knipp Federal Reserve Board of Governors, USA, Frederic Wantiez , Simon J. Godsill Department of Engineering, University of Cambridge, Hong Ge University of Cambridge
16:32 58m Other		Poster session LAFI

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:00	Program AnalysisPOPL at Peek-A-Boo

10:40 20m Talk		Maximal Simplification of Polyhedral Reductions POPL Louis Narmour Colorado State University, Tomofumi Yuki , Sanjay Rajopadhye Colorado State University
11:00 20m Talk		Program Analysis via Multiple Context Free Language Reachability POPL Giovanna Kobus Conrado Hong Kong University of Science and Technology, Adam Husted Kjelstrøm Aarhus University, Jaco van de Pol Aarhus University, Andreas Pavlogiannis Aarhus University
11:20 20m Talk		The Best of Abstract Interpretations POPL Roberto Giacobazzi University of Arizona, Francesco Ranzato Dipartimento di Matematica, University of Padova, Italy
11:40 20m Talk		An Incremental Algorithm for Algebraic Program Analysis POPL Chenyu Zhou University of Southern California, Yuzhou Fang University of Southern California, Jingbo Wang Purdue University, Chao Wang University of Southern California

13:20 - 14:20	Verification 1POPL at Peek-A-Boo

13:20 20m Talk		Axe 'Em: Eliminating Spurious States with Induction Axioms POPL Neta Elad Tel Aviv University, Sharon Shoham Tel Aviv University
13:40 20m Talk		A Verified Foreign Function Interface Between Coq and C POPL Joomy Korkut Bloomberg LP, Kathrin Stark Heriot-Watt University, Andrew W. Appel Princeton University
14:00 20m Talk		TensorRight: Automated Verification of Tensor Graph Rewrites POPL Jai Arora University of Illinois at Urbana-Champaign, Sirui Lu University of Washington, Devansh Jain University of Illinois at Urbana-Champaign, Tianfan Xu University of Illinois at Urbana-Champaign, Farzin Houshmand Google, Phitchaya Mangpo Phothilimthana Google, Mohsen Lesani University of California at Santa Cruz, Praveen Narayanan Google, Karthik Srinivasa Murthy Google, Rastislav Bodík Google Research, Brain Team, Amit Sabne Google, Charith Mendis University of Illinois at Urbana-Champaign

15:00 - 16:20	Semantic modelsPOPL at Peek-A-Boo

15:00 20m Talk		Consistency of a Dependent Calculus of Indistinguishability POPL Yiyun Liu University of Pennsylvania, Jonathan Chan University of Pennsylvania, Stephanie Weirich University of Pennsylvania
15:20 20m Talk		Finite-Choice Logic Programming POPL Chris Martens Northeastern University, Robert Simmons Independent, Michael Arntzenius None Pre-print
15:40 20m Talk		Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory POPL Eric Giovannini University of Michigan, Tingting Ding University of Michigan, Max S. New University of Michigan
16:00 20m Talk		Abstract Operational Methods for Call-by-Push-Value POPL Sergey Goncharov University of Birmingham, School of Comp. Sci., Stelios Tsampas FAU Erlangen-Nuremberg, INF 8, Henning Urbat FAU Erlangen-Nuremberg, INF 8

17:00 - 18:00	Separation LogicPOPL at Peek-A-Boo

17:00 20m Talk		Formal Foundations for Translational Separation Logic Verifiers POPL Thibault Dardinier ETH Zurich, Michael Sammler Institute of Science and Technology Austria, Gaurav Parthasarathy ETH Zurich, Alexander J. Summers University of British Columbia, Peter Müller ETH Zurich
17:20 20m Talk		Fulminate: Testing CN Separation-Logic Specifications in C POPL Rini Banerjee University of Cambridge, Kayvan Memarian University of Cambridge, Dhruv Makwana University of Cambridge, Christopher Pulte University of Cambridge, Neel Krishnaswami University of Cambridge, Peter Sewell University of Cambridge
17:40 20m Talk		Generically Automating Separation Logic by Functors, Homomorphisms, and Modules POPL Qiyuan Xu Nanyang Technological University, David Sanan Singapore Institute of Technology, Zhe Hou Griffith University, Xiaokun Luan Peking University, Conrad Watt Nanyang Technological University, Yang Liu Nanyang Technological University

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:00	Syntax and EditingPOPL at Peek-A-Boo

10:40 20m Talk		RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds POPL Ian Erik Varatalu Tallinn University of Technology, Estonia, Margus Veanes Microsoft Research, Juhan Ernits Tallinn University of Technology
11:00 20m Talk		Pantograph: A Fluid and Typed Structure Editor POPL Jacob Prinz University of Maryland, College Park, Henry Blanchette , Leonidas Lampropoulos University of Maryland, College Park
11:20 20m Talk		Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus POPL Michael D. Adams National University of Singapore, Eric Griffis University of Michigan, Thomas J. Porter University of Michigan, Sundara Vishnu Satish University of Michigan - Ann Arbor, Eric Zhao Brown University, Cyrus Omar University of Michigan
11:40 20m Talk		Biparsers: Exact Printing for Data Synchronisation POPL Ruifeng Xie Peking University, Tom Schrijvers KU Leuven, Zhenjiang Hu Peking University

13:20 - 14:20	Program Logics 1POPL at Peek-A-Boo

13:20 20m Talk		Program logics à la carte POPL Max Vistrup ETH Zurich, Michael Sammler Institute of Science and Technology Austria, Ralf Jung ETH Zurich
13:40 20m Talk		On Extending Incorrectness Logic with Backwards Reasoning POPL Freek Verbeek Open Universiteit & Virginia Tech, Md Syadus Sefat Virginia Tech, Zhoulai Fu State University of New York, Korea, Binoy Ravindran Virginia Tech
14:00 20m Talk		A Demonic Outcome Logic for Randomized Nondeterminism POPL Noam Zilberstein Cornell University, Dexter Kozen Cornell University, Alexandra Silva Cornell University, Joseph Tassarotti New York University

15:00 - 16:20	ConcurrencyPOPL at Peek-A-Boo

15:00 20m Talk		Data Race Freedom à la Mode POPL Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Benjamin Peters MPI-SWS, Laila Elbeheiry MPI-SWS, Leo White Jane Street, Stephen Dolan Jane Street, Richard A. Eisenberg Jane Street, Chris Casinghino Jane Street, François Pottier Inria, Derek Dreyer MPI-SWS
15:20 20m Talk		RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency POPL Pavel Golovin MPI-SWS, Michalis Kokologiannakis ETH Zurich, Viktor Vafeiadis MPI-SWS
15:40 20m Talk		Relaxed Memory Concurrency Re-executed POPL Evgenii Moiseenko JetBrains Research, Matteo Meluzzi TU Delft, the Netherlands, Innokentii Meleshchenko JetBrains Research, Neapolis University Pafos, Cyprus, Ivan Kabashnyi JetBrains Research, Constructor University Bremen, Germany, Anton Podkopaev JetBrains Research, Constructor University, Soham Chakraborty TU Delft
16:00 20m Talk		Model Checking C/C++ with Mixed-Size Accesses POPL Iason Marmanis MPI-SWS, Michalis Kokologiannakis ETH Zurich, Viktor Vafeiadis MPI-SWS

17:00 - 17:40	Kleene Algebra with TestsPOPL at Peek-A-Boo

17:00 20m Talk		CF-GKAT: Efficient Validation of Control-Flow Transformations POPL Cheng Zhang University College London (UCL), Tobias Kappé LIACS, Leiden University, David E. Narváez Virginia Tech, Nico Naus Open University of The Netherlands & Virginia Tech
17:20 20m Talk		Algebras for Deterministic Computation are Inherently Incomplete POPL Balder ten Cate ILLC, University of Amsterdam, Tobias Kappé LIACS, Leiden University

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:00	Types 2POPL at Peek-A-Boo

10:40 20m Paper		Affect: An Affine Type and Effect System POPL Orpheas van Rooij University of Edinburgh, Robbert Krebbers Radboud University Nijmegen Link to publication
11:00 20m Talk		A modal deconstruction of Löb induction POPL Daniel Gratzer Aarhus University
11:20 20m Talk		QuickSub: Efficient Iso-Recursive Subtyping POPL Litao Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
11:40 20m Talk		Generic Refinement Types POPL Nico Lehmann UCSD, Cole Kurashige UCSD, Nikhil Akiti UCSD, Niroop Krishnakumar UCSD, Ranjit Jhala UCSD

13:20 - 14:20	Program Logics 2POPL at Peek-A-Boo

13:20 20m Talk		BiSikkel: A Multimode Logical Framework in Agda POPL Joris Ceulemans KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese KU Leuven
13:40 20m Talk		Calculational Design of Hyperlogics by Abstract Interpretation POPL Patrick Cousot , Jeffery Wang CIMS, New York University
14:00 20m Talk		A Taxonomy of Hoare-Like Logics POPL Lena Verscht RWTH Aachen University; Saarland University, Benjamin Lucien Kaminski Saarland University; University College London

15:00 - 16:20	TheoryPOPL at Peek-A-Boo

15:00 20m Talk		The Duality of λ-Abstraction POPL Vikraman Choudhury Università di Bologna & Inria OLAS, Simon J. Gay University of Glasgow, UK
15:20 20m Talk		On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus POPL Naoki Kobayashi University of Tokyo
15:40 20m Talk		Interaction Equivalence POPL Beniamino Accattoli Inria & Ecole Polytechnique, Adrienne Lancelot Inria, LIX Ecole Polytechnique, IRIF Université Paris Cité, Giulio Manzonetto Université Paris Cité, Gabriele Vanoni IRIF, Université Paris Cité
16:00 20m Talk		Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings POPL Jan van Brügge Heriot-Watt University, James McKinna Heriot-Watt University, Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen

17:00 - 18:00	Proof AssistantsPOPL at Peek-A-Boo

17:00 20m Talk		Progressful Interpreters for Efficient WebAssembly Mechanisation POPL Xiaojia Rao Imperial College London, Stefan Radziuk Imperial College London, Conrad Watt Nanyang Technological University, Philippa Gardner Imperial College London
17:20 20m Talk		Unifying compositional verification and certified compilation with a three-dimensional refinement algebra POPL Yu Zhang , Jérémie Koenig Yale University, Zhong Shao Yale University, Yuting Wang Shanghai Jiao Tong University
17:40 20m Talk		All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants POPL Josselin Poiret Nantes Université, Inria, Gaetan Gilbert , Kenji Maillard Inria, Pierre-Marie Pédrot INRIA, Matthieu Sozeau Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:30	Session 1CoqPL at Peek-A-Boo

09:00 50m Keynote		Elpi: rule-based meta-languge for Rocq CoqPL Enrico Tassi INRIA
09:50 20m Talk		Implementing OCaml APIs in Coq CoqPL Joshua M. Cohen Princeton University
10:10 20m Talk		Towards general white-box automation: a typeclass-guided context cleaner CoqPL Thibaut Pérami University of Cambridge

11:00 - 12:30	Session 2CoqPL at Peek-A-Boo

11:00 70m Panel		Session with the Coq Development Team CoqPL Matthieu Sozeau Inria, Nicolas Tabareau Inria, Enrico Tassi INRIA, Yves Bertot INRIA
12:10 20m Talk		Vellvm: Formalizing the Informal CoqPL Calvin Beck University of Pennsylvania, USA, Hanxi Chen , Steve Zdancewic University of Pennsylvania

14:00 - 15:30	Session 3CoqPL at Peek-A-Boo

14:00 22m Talk		Towards Verified Linear Algebra Programs Through Equivalence CoqPL Yihan Yang Harvey Mudd College, Mohit Tekriwal Lawrence Livermore National Laboratory, John Sarracino Lawrence Livermore National Laboratory, Matthew Sottile Lawrence Livermore National Laboratory, Ignacio Laguna Lawrence Livermore National Laboratory
14:22 22m Talk		A Framework of Differential Operators CoqPL Runqing Xu , Sebastian Erdweg JGU Mainz
14:45 22m Talk		A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types CoqPL Tarakaram Gollamudi None, Jules Jacobs Cornell University, Yue Yao Carnegie Mellon University, Stephanie Balzer Carnegie Mellon University
15:07 22m Talk		Formal Verification of a Software Defined Delay-Tolerant Network CoqPL Jan-Paul Ramos-Davila Cornell University

16:00 - 17:30	Session 4 (16:00 - 17:30)CoqPL at Peek-A-Boo

16:00 22m Talk		Towards Automated Verification of LLM-Synthesized C Programs CoqPL Prasita Mukherjee , Benjamin Delaware Purdue University
16:22 22m Talk		Towards Mining Robust Coq Proof Patterns CoqPL Cezary Kaliszyk University of Melbourne, Xuan-Bach D. Le University of Melbourne, Christine Rizkallah University of Melbourne
16:45 22m Talk		CoqNFU: Towards Formalizing NFU in Coq CoqPL Marko Doko Heriot-Watt University, UK, Vedran Čačić
17:07 22m Talk		Formal Verification of Quantum Stabilizer Code CoqPL Qiuyi Feng , Udaya Parampalli , Christine Rizkallah University of Melbourne

Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Peek-A-Boo	LAFI First session																								LAFI Second session																																				LAFI Third session																								LAFI Fourth session

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Peek-A-Boo	PLMW @ POPL																								PLMW @ POPL																																				PLMW @ POPL																								PLMW @ POPL

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Peek-A-Boo									POPL Program Analysis																																POPL Verification 1																				POPL Semantic models																								POPL Separation Logic

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Peek-A-Boo									POPL Syntax and Editing																																POPL Program Logics 1																				POPL Concurrency																								POPL Kleene Algebra with Tests

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Peek-A-Boo									POPL Types 2																																POPL Program Logics 2																				POPL Theory																								POPL Proof Assistants

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Peek-A-Boo	CoqPL Session 1																								CoqPL Session 2																																				CoqPL Session 3																								CoqPL Session 4 (16:00 - 17:30)

Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Peek-A-Boo	LAFI Welcome 09:00 - 09:05	LAFI Industry Talk: Basis AI 09:06 - 09:26				LAFI Towards Symbolic Execution for Probability and Non-determinism 09:27 - 09:42				LAFI Lazy Knowledge Compilation for Discrete PPLs 09:43 - 09:58			LAFI Reasoning About Sampling Without Sampling: Atomic Machines for Contextu ... 09:59 - 10:14			LAFI Exact Inference for Nested Discrete Probabilistic Programs 10:15 - 10:30									LAFI Invited talk: A Fast and Differentiable Tokamak Transport Simulator in JAX 11:00 - 11:40								LAFI Data-Parallel Differentiation by Optic Composition 11:41 - 11:56			LAFI A Domain-Specific PPL for Reasoning about Reasoning (or: a memo on memo) 11:57 - 12:12				LAFI Data-oriented Design for Differentiable, Probabilistic Programming 12:13 - 12:28																					LAFI Invited talk: Modern Bayesian experimental design 14:00 - 14:40								LAFI Partially Evaluating Higher-Order Probabilistic Programs without Stocha ... 14:41 - 14:56			LAFI NP-NUTS: A Nonparametric No-U-Turn Sampler 14:57 - 15:12				LAFI Sandwood: Runtime Adaptable Probabilistic Programming for Java 15:13 - 15:28									LAFI Semantics of the memo Probabilistic Programming Language 16:00 - 16:15			LAFI State Space Model Programming in Turing.jl 16:16 - 16:31			LAFI Poster session 16:32 - 17:30

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Peek-A-Boo									POPL Maximal Simplification of Polyhedral Reductions 10:40 - 11:00				POPL Program Analysis via Multiple Context Free Language Reachability 11:00 - 11:20				POPL The Best of Abstract Interpretations 11:20 - 11:40				POPL An Incremental Algorithm for Algebraic Program Analysis 11:40 - 12:00																				POPL Axe 'Em: Eliminating Spurious States with Induction Axioms 13:20 - 13:40				POPL A Verified Foreign Function Interface Between Coq and C 13:40 - 14:00				POPL TensorRight: Automated Verification of Tensor Graph Rewrites 14:00 - 14:20												POPL Consistency of a Dependent Calculus of Indistinguishability 15:00 - 15:20				POPL Finite-Choice Logic Programming 15:20 - 15:40				POPL Denotational Semantics of Gradual Typing using Synthetic Guarded Domain ... 15:40 - 16:00				POPL Abstract Operational Methods for Call-by-Push-Value 16:00 - 16:20												POPL Formal Foundations for Translational Separation Logic Verifiers 17:00 - 17:20				POPL Fulminate: Testing CN Separation-Logic Specifications in C 17:20 - 17:40				POPL Generically Automating Separation Logic by Functors, Homomorphisms, and ... 17:40 - 18:00

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Peek-A-Boo									POPL RE#: High Performance Derivative-Based Regex Matching with Intersection ... 10:40 - 11:00				POPL Pantograph: A Fluid and Typed Structure Editor 11:00 - 11:20				POPL Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus 11:20 - 11:40				POPL Biparsers: Exact Printing for Data Synchronisation 11:40 - 12:00																				POPL Program logics à la carte 13:20 - 13:40				POPL On Extending Incorrectness Logic with Backwards Reasoning 13:40 - 14:00				POPL A Demonic Outcome Logic for Randomized Nondeterminism 14:00 - 14:20												POPL Data Race Freedom à la Mode 15:00 - 15:20				POPL RELINCHE: Automatically Checking Linearizability under Relaxed Memory C ... 15:20 - 15:40				POPL Relaxed Memory Concurrency Re-executed 15:40 - 16:00				POPL Model Checking C/C++ with Mixed-Size Accesses 16:00 - 16:20												POPL CF-GKAT: Efficient Validation of Control-Flow Transformations 17:00 - 17:20				POPL Algebras for Deterministic Computation are Inherently Incomplete 17:20 - 17:40

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Peek-A-Boo									POPL Affect: An Affine Type and Effect System 10:40 - 11:00				POPL A modal deconstruction of Löb induction 11:00 - 11:20				POPL QuickSub: Efficient Iso-Recursive Subtyping 11:20 - 11:40				POPL Generic Refinement Types 11:40 - 12:00																				POPL BiSikkel: A Multimode Logical Framework in Agda 13:20 - 13:40				POPL Calculational Design of Hyperlogics by Abstract Interpretation 13:40 - 14:00				POPL A Taxonomy of Hoare-Like Logics 14:00 - 14:20												POPL The Duality of λ-Abstraction 15:00 - 15:20				POPL On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus 15:20 - 15:40				POPL Interaction Equivalence 15:40 - 16:00				POPL Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for ... 16:00 - 16:20												POPL Progressful Interpreters for Efficient WebAssembly Mechanisation 17:00 - 17:20				POPL Unifying compositional verification and certified compilation with a th ... 17:20 - 17:40				POPL All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants 17:40 - 18:00

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Peek-A-Boo	CoqPL Elpi: rule-based meta-languge for Rocq 09:00 - 09:50										CoqPL Implementing OCaml APIs in Coq 09:50 - 10:10				CoqPL Towards general white-box automation: a typeclass-guided context cleaner 10:10 - 10:30										CoqPL Session with the Coq Development Team 11:00 - 12:10														CoqPL Vellvm: Formalizing the Informal 12:10 - 12:30																						CoqPL Towards Verified Linear Algebra Programs Through Equivalence 14:00 - 14:22				CoqPL A Framework of Differential Operators 14:22 - 14:45					CoqPL A Semantic Logical Relation for Termination of Intuitionistic Linear Lo ... 14:45 - 15:07				CoqPL Formal Verification of a Software Defined Delay-Tolerant Network 15:07 - 15:30											CoqPL Towards Automated Verification of LLM-Synthesized C Programs 16:00 - 16:22				CoqPL Towards Mining Robust Coq Proof Patterns 16:22 - 16:45					CoqPL CoqNFU: Towards Formalizing NFU in Coq 16:45 - 17:07				CoqPL Formal Verification of Quantum Stabilizer Code 17:07 - 17:30

Room information: Peek-A-Boo

This program is tentative and subject to change.

Program Display Configuration

Sun 19 JanDisplayed time zone: Mountain Time (US & Canada) change

Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change

Thu 23 JanDisplayed time zone: Mountain Time (US & Canada) change

Fri 24 JanDisplayed time zone: Mountain Time (US & Canada) change

Sat 25 JanDisplayed time zone: Mountain Time (US & Canada) change

Sun 19 JanDisplayed time zone: Mountain Time (US & Canada) change

LAFI

LAFI

LAFI

LAFI

Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change

PLMW @ POPL

PLMW @ POPL

PLMW @ POPL

PLMW @ POPL

Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change

POPL

POPL

POPL

POPL

Thu 23 JanDisplayed time zone: Mountain Time (US & Canada) change

POPL

POPL

POPL

POPL

Fri 24 JanDisplayed time zone: Mountain Time (US & Canada) change

POPL

POPL

POPL

POPL

Sat 25 JanDisplayed time zone: Mountain Time (US & Canada) change

CoqPL

CoqPL

CoqPL

CoqPL

Sun 19 JanDisplayed time zone: Mountain Time (US & Canada) change

Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change

Thu 23 JanDisplayed time zone: Mountain Time (US & Canada) change

Fri 24 JanDisplayed time zone: Mountain Time (US & Canada) change

Sat 25 JanDisplayed time zone: Mountain Time (US & Canada) change

Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change

Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change

Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change