Room 2 - CoqPL 2025

VenueCurtis Hotel Denver

Room nameRoom 2

Floor0

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	KeynoteDafny at Room 2

09:00 10m Day opening		Day opening Dafny Stefan Zetzsche Amazon Web Services
09:10 60m Keynote		Keynote Dafny Nada Amin Harvard University

11:00 - 12:30	Proof Stability and ApplicationsDafny at Room 2

11:00 18m Talk		Helping users to reduce Brittleness in their Dafny programs - a success story Dafny Remy Willems Amazon, Matthias Schlaipfer Amazon, Olivier Bouissou Amazon
11:18 18m Talk		Towards Proof Stability in SMT-based Program Verification Dafny Yi Zhou Carnegie Mellon University, Bryan Parno Carnegie Mellon University
11:36 18m Talk		Verifying the Fisher-Yates Shuffle Algorithm in Dafny Dafny Stefan Zetzsche Amazon Web Services, Tancrède Lepoint Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services, Mikael Mayer Automated Reasoning Group, Amazon Web Services
11:54 18m Talk		Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems Dafny Derek Leung MIT, Nickolai Zeldovich Massachusetts Institute of Technology, USA, M. Frans Kaashoek Massachusetts Institute of Technology, USA
12:12 18m Talk		Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny Dafny Stefan Zetzsche Amazon Web Services, Wojciech Różowski University College London

14:00 - 15:30	Backends and TeachingDafny at Room 2

14:00 18m Talk		Baking for Dafny: A CakeML Backend for Dafny Dafny Daniel Nezamabadi Chalmers University of Technology and University of Gothenburg, Magnus O. Myreen Chalmers University of Technology
14:18 18m Talk		Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean Dafny Wojciech Różowski University College London, Georges-Axel Jaloyan Amazon Web Services, Sean McLaughlin Amazon Web Services
14:36 18m Talk		Performant, Readable and Interoperable Rust from Dafny Dafny Mikael Mayer Automated Reasoning Group, Amazon Web Services, Shadaj Laddad University of California at Berkeley, Fabio Madge Automated Reasoning Group, Amazon Web Services, Siva Somayyajula Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services
14:54 18m Talk		Randomised Testing of the Dafny Compiler: Into the CI Dafny Karnbongkot Boonriong Imperial College London, Alastair F. Donaldson Imperial College London, Stefan Zetzsche Amazon Web Services
15:12 18m Talk		Teaching Types and Non-Interference in Dafny Dafny Bryan Parno Carnegie Mellon University

16:00 - 18:00	Verified Code SynthesisDafny at Room 2

16:00 18m Talk		Laurel: Unblocking Automated Verification with Large Language Models Dafny Eric Mugnier University of California San Diego, Emmanuel Anaya Gonzalez UCSD, Nadia Polikarpova University of California at San Diego, Ranjit Jhala University of California at San Diego, Zhou Yuanyuan UCSD
16:18 18m Talk		VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search Dafny David Brandfonbrener Harvard, Simon Henniger Technical University of Munich, Sibi Raja Harvard, Tarun Prasad Harvard, Chloe Loughridge Harvard University, Federico Cassano Northeastern University, Sabrina Ruixin Hu Harvard, Jianang Yang Million.js, William E. Byrd University of Alabama at Birmingham, USA, Robert Zinkov University of Oxford, Nada Amin Harvard University
16:36 18m Talk		dafny-annotator: AI-Assisted Verification of Dafny Programs Dafny Gabriel Poesia Stanford University, Chloe Loughridge Harvard University, Nada Amin Harvard University
16:54 18m Talk		Dafny as Verification-Aware Intermediate Language for Code Generation Dafny Yue Chen Li Massachusetts Institute of Technology, Stefan Zetzsche Amazon Web Services, Siva Somayyajula Amazon Web Services
17:12 18m Talk		DafnyBench: A Benchmark for Formal Software Verification Dafny Chloe Loughridge Harvard University, Qinyi Sun Massachusetts Institute of Technology, Seth Ahrenbach Beneficial AI Foundation, Federico Cassano Northeastern University, Chuyue Sun Stanford University, Ying Sheng Stanford University, Anish Mudide Massachusetts Institute of Technology, Md Rakib Hossain Misu University of California Irvine, Nada Amin Harvard University, Max Tegmark Massachusetts Institute of Technology
17:30 18m Talk		Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming Dafny Saikat Chakraborty Microsoft Research, Gabriel Ebner Microsoft Research, Siddharth Bhat University of Cambridge, Sarah Fakhoury Microsoft Research, Sakina Fatima University of Ottawa, Shuvendu K. Lahiri Microsoft Research, Nikhil Swamy Microsoft Research
17:48 12m Day closing		Day closing Dafny Stefan Zetzsche Amazon Web Services

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:30	Session 1PADL at Room 2

09:00 60m Keynote		Solvers, unite! A simple unified semantics for reasoning with assurance and agreement PADL Y. Annie Liu Stony Brook University
10:00 30m Talk		Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination PADL Kento Takyu Waseda University, Kazunori Ueda Waseda University

11:00 - 12:30	Session 2PADL at Room 2

11:00 30m Talk		Type-Checking Heterogeneous Sequences in a Simple Embeddable Type System PADL Jim Newton EPITA / LRDE https://www.lre.epita.fr
11:30 30m Talk		Haskell Based Spreadsheets PADL Ignacio Ballesteros IMDEA Software Institute and Universidad Politécnica de Madrid, Luis Eduardo Bueso de Barrio Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid
12:00 30m Talk		The Scenic Route to Deforestation PADL Steven Libby , Vincent Robinson University of Portland

14:00 - 15:30	Session 3PADL at Room 2

14:00 30m Talk		A practical approach to handling tabular data in logic PADL Robin De Vogelaere KU Leuven, Kylian Van Dessel Leuven.AI, Belgium, Joost Vennekens KU Leuven
14:30 30m Talk		C3G: Causally Constrained Counterfactual Generation PADL Sopam Dasgupta , Farhad Shakerin Microsoft, Joaquín Arias Universidad Rey Juan Carlos, Elmer Salazar The University of Texas at Dallas, Gopal Gupta
15:00 30m Talk		On Bridging Prolog and Python to Enhance an Inductive Logic Programming System PADL Vitor Santos Costa University of Porto, Portugal, Miguel Areias University of Porto, Portugal

16:00 - 17:30	Session 4PADL at Room 2

16:00 30m Talk		MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs PADL Felipe Gorostiaga IMDEA Software Institute, Martin Ceresa IMDEA Software Institute, César Sánchez IMDEA Software Institute
16:30 30m Talk		Checking Concurrency Coding Rules PADL Lars-Åke Fredlund Universidad Politécnica de Madrid, Ángel Herranz Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid

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

09:00 - 10:30	Session 5PADL at Room 2

09:00 60m Keynote		Bridging Safety and Performance PADL Umut A. Acar Carnegie Mellon University
10:00 30m Talk		SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic PADL Zachary Hansen University of Nebraska Omaha, Yuliya Lierler University of Nebraska

11:00 - 12:30	Session 6PADL at Room 2

11:00 30m Talk		ASP for Language Documentation and Reclamation: A Derivational Stemming Tool for Myaamia PADL Daniela Inclezan Miami University, USA, Hunter Lockwood Myaamia Center & Miami University, Anita Baral Miami University, Jitendra Sharma Miami University, Pratiksha Shrestha Miami University
11:30 30m Talk		A Weighted Bipolar Argumentation Framework and its ASP-based Implementation PADL Yan Yan Southeast University, Nanjing, Junru Li Southeast University, Nanjing, Fangzhou Liu Southeast University, Nanjing, Zerong Wang Southeast University, Nanjing, Zhizheng Zhang Southeast University, Nanjing
12:00 30m Talk		Automated Playing of Survival Video Games with Commonsense Reasoning (short paper) PADL Dan Nguyen University of Texas at Dallas, USA, Bryant Hargreaves University of Texas at Dallas, USA, Keegan Kimbrell University of Texas at Dallas, USA, Gopal Gupta

14:00 - 15:30	Session 7PADL at Room 2

14:00 30m Talk		Exploring Answer Set Programming for Provenance Graph-Based Cyber Threat Detection: A Novel Approach PADL Fang Li Oklahoma Christian University, Fei Zuo University of Central Oklahoma, Gopal Gupta
14:30 30m Talk		Leveraging LLM Reasoning with Dual Horn Programs PADL Paul Tarau University of North Texas
15:00 30m Talk		Enhancing network diagnosis with reflection in Prolog (extended abstract) PADL Anduo Wang Temple University, USA Pre-print

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

10:40 - 12:00	Program AnalysisPOPL at Room 2

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 Room 2

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 Room 2

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 Room 2

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 Room 2

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 Room 2

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 Room 2

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 Room 2

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 Room 2

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 Room 2

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 Room 2

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 Room 2

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 2025 at Room 2

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

11:00 - 12:30	Session 2CoqPL 2025 at Room 2

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

14:00 - 15:30	Session 3CoqPL 2025 at Room 2

14:00 22m Talk		Towards Verified Linear Algebra Programs Through Equivalence CoqPL 2025 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 2025 Runqing Xu , Sebastian Erdweg JGU Mainz
14:45 22m Talk		A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types CoqPL 2025 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 2025 Jan-Paul Ramos-Davila Cornell University

16:00 - 17:30	Session 4 (16:00 - 17:30)CoqPL 2025 at Room 2

16:00 22m Talk		Towards Automated Verification of LLM-Synthesized C Programs CoqPL 2025 Prasita Mukherjee , Benjamin Delaware Purdue University
16:22 22m Talk		Towards Mining Robust Coq Proof Patterns CoqPL 2025 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 2025 Marko Doko Heriot-Watt University, UK, Vedran Čačić
17:07 22m Talk		Formal Verification of Quantum Stabilizer Code CoqPL 2025 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
Room 2	Dafny Keynote																								Dafny Proof Stability and Applications																																				Dafny Backends and Teaching																								Dafny Verified Code Synthesis

Mon 20 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
Room 2	PADL Session 1																								PADL Session 2																																				PADL Session 3																								PADL Session 4

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
Room 2	PADL Session 5																								PADL Session 6																																				PADL Session 7																								PADL

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
Room 2									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
Room 2									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
Room 2									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
Room 2	CoqPL 2025 Session 1																								CoqPL 2025 Session 2																																				CoqPL 2025 Session 3																								CoqPL 2025 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
Room 2	Dafny Day opening 09:00 - 09:10		Dafny Keynote 09:10 - 10:10																						Dafny Helping users to reduce Brittleness in their Dafny programs - a success ... 11:00 - 11:18				Dafny Towards Proof Stability in SMT-based Program Verification 11:18 - 11:36			Dafny Verifying the Fisher-Yates Shuffle Algorithm in Dafny 11:36 - 11:54				Dafny Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fau ... 11:54 - 12:12			Dafny Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny 12:12 - 12:30																						Dafny Baking for Dafny: A CakeML Backend for Dafny 14:00 - 14:18				Dafny Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean 14:18 - 14:36			Dafny Performant, Readable and Interoperable Rust from Dafny 14:36 - 14:54				Dafny Randomised Testing of the Dafny Compiler: Into the CI 14:54 - 15:12			Dafny Teaching Types and Non-Interference in Dafny 15:12 - 15:30										Dafny Laurel: Unblocking Automated Verification with Large Language Models 16:00 - 16:18				Dafny VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Lan ... 16:18 - 16:36			Dafny dafny-annotator: AI-Assisted Verification of Dafny Programs 16:36 - 16:54				Dafny Dafny as Verification-Aware Intermediate Language for Code Generation 16:54 - 17:12			Dafny DafnyBench: A Benchmark for Formal Software Verification 17:12 - 17:30				Dafny Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming 17:30 - 17:48				Dafny Day closing 17:48 - 18:00

Mon 20 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
Room 2	PADL Solvers, unite! A simple unified semantics for reasoning with assurance ... 09:00 - 10:00												PADL Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Eli ... 10:00 - 10:30												PADL Type-Checking Heterogeneous Sequences in a Simple Embeddable Type System 11:00 - 11:30						PADL Haskell Based Spreadsheets 11:30 - 12:00						PADL The Scenic Route to Deforestation 12:00 - 12:30																								PADL A practical approach to handling tabular data in logic 14:00 - 14:30						PADL C3G: Causally Constrained Counterfactual Generation 14:30 - 15:00						PADL On Bridging Prolog and Python to Enhance an Inductive Logic Programming ... 15:00 - 15:30												PADL MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embe ... 16:00 - 16:30						PADL Checking Concurrency Coding Rules 16:30 - 17:00

Tue 21 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
Room 2	PADL Bridging Safety and Performance 09:00 - 10:00												PADL SM-based Semantics for Answer Set Programs Containing Conditional Liter ... 10:00 - 10:30												PADL ASP for Language Documentation and Reclamation: A Derivational Stemming ... 11:00 - 11:30						PADL A Weighted Bipolar Argumentation Framework and its ASP-based Implementation 11:30 - 12:00						PADL Automated Playing of Survival Video Games with Commonsense Reasoning (s ... 12:00 - 12:30																								PADL Exploring Answer Set Programming for Provenance Graph-Based Cyber Threa ... 14:00 - 14:30						PADL Leveraging LLM Reasoning with Dual Horn Programs 14:30 - 15:00						PADL Enhancing network diagnosis with reflection in Prolog (extended abstract) 15:00 - 15: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
Room 2									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
Room 2									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
Room 2									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
Room 2	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: Room 2

This program is tentative and subject to change.

Program Display Configuration

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

Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change

Tue 21 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

Dafny

Dafny

Dafny

Dafny

Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change

PADL

PADL

PADL

PADL

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

PADL

PADL

PADL

PADL

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 2025

CoqPL 2025

CoqPL 2025

CoqPL 2025

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

Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change

Tue 21 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

Mon 20 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

Mon 20 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

Mon 20 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