PriSC 2025
Dates to be announced Denver, Colorado, United States
co-located with 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.

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

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

11:00 - 12:30
Session 2CoqPL at Peek-A-Boo
11:00
70m
Panel
Session with the Coq Development Team
CoqPL
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
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
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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Peek-A-Boo

Tue 21 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Peek-A-Boo

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

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Peek-A-Boo

Sat 25 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Peek-A-Boo