PriSC 2025
Dates to be announced
Denver, Colorado, United States
co-located with
POPL 2025
Toggle navigation
Attending
Venue: Curtis Hotel Denver
Program
PriSC Program
Your Program
Wed 31 Dec
Track/Call
Organization
PriSC 2025 Committees
Track Committees
Program Committee
Steering Committee
Contributors
People Index
Search
Series
Series
PriSC 2025
PriSC 2024
PriSC 2023
PriSC 2022
PriSC 2021
PriSC 2020
PriSC 2019
PriSC 2018
Sign in
Sign up
POPL 2025
(
series
) /
PriSC 2025 (
series
) /
Curtis Hotel Denver
/
Room information: Peek-A-Boo
Venue
Curtis Hotel Denver
Room name
Peek-A-Boo
Floor
2
Capacity
300
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
This program is tentative and subject to change.
Program Display Configuration
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
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
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 program
Specify 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
Wed 22 Jan
Displayed time zone:
Mountain Time (US & Canada)
change
10:40 - 12:00
Program Analysis
POPL
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 1
POPL
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 models
POPL
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 Logic
POPL
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 Editing
POPL
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 1
POPL
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
Concurrency
POPL
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 Tests
POPL
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 2
POPL
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 2
POPL
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
Theory
POPL
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 Assistants
POPL
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 1
CoqPL
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 2
CoqPL
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 3
CoqPL
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
LAFI
LAFI
LAFI
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)
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
x
Sat 21 Dec 19:22