Filter Program
Dates
Rooms
Tracks
Badges
Your Program
This program is tentative and subject to change.
Sun 19 JanDisplayed time zone: Mountain Time (US & Canada) change
Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 10mDay opening | Day opening Dafny Stefan Zetzsche Amazon Web Services | ||
09:10 60mKeynote | Keynote Dafny Nada Amin Harvard University | ||
11:00 - 12:30 | |||
11:00 18mTalk | Helping users to reduce Brittleness in their Dafny programs - a success story Dafny | ||
11:18 18mTalk | Towards Proof Stability in SMT-based Program Verification Dafny | ||
11:36 18mTalk | 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 18mTalk | 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 18mTalk | Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny Dafny | ||
14:00 - 15:30 | |||
14:00 18mTalk | 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 18mTalk | 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 18mTalk | 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 18mTalk | 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 18mTalk | Teaching Types and Non-Interference in Dafny Dafny Bryan Parno Carnegie Mellon University | ||
16:00 - 18:00 | |||
16:00 18mTalk | 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 18mTalk | 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 18mTalk | dafny-annotator: AI-Assisted Verification of Dafny Programs Dafny Gabriel Poesia Stanford University, Chloe Loughridge Harvard University, Nada Amin Harvard University | ||
16:54 18mTalk | 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 18mTalk | 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 18mTalk | 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 12mDay closing | Day closing Dafny Stefan Zetzsche Amazon Web Services | ||
Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change
Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mKeynote | Prospects for Computer Formalization of Infinite-Dimensional Category Theory CPP Emily Riehl Johns Hopkins University | ||
10:00 30mTalk | Certifying rings of integers in number fields CPP Anne Baanen Vrije Universiteit Amsterdam, Alain Chavarri Villarello Vrije Universiteit Amsterdam, Sander R. Dahmen Vrije Universiteit Amsterdam | ||
09:00 - 10:30 | |||
09:00 4mDay opening | Opening Remarks PriSC | ||
09:05 59mKeynote | Keynote: Bringing Verified Cryptographic Protocols to Practice PriSC Bryan Parno Carnegie Mellon University | ||
10:05 25mTalk | A Semantic Approach to Robust Property Preservation PriSC Niklas Mück MPI-SWS, Michael Sammler Institute of Science and Technology Austria, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS | ||
11:00 - 12:30 | |||
11:00 30mTalk | Split Decisions: Explicit Contexts for Substructural Languages CPP Daniel Zackon McGill University, Chuta Sano McGill University, Alberto Momigliano Università degli Studi di Milano, Brigitte Pientka McGill University | ||
11:30 30mTalk | Machine Checked Proofs and Programs in Algebraic Combinatorics CPP Florent Hivert Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA | ||
12:00 30mTalk | Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IR CPP Nicolas Chappe Inria Lyon, LIP, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Yannick Zakowski Inria | ||
11:00 - 12:30 | |||
11:00 25mTalk | ILA: Correctness via Type Checking for Fully Homomorphic Encryption PriSC Tarakaram Gollamudi None, Anitha Gollamudi University of Massachusetts Lowell, Joshua Gancher Northeastern University | ||
11:25 24mTalk | Leveraging Duality for Programming with zkSNARKs PriSC | ||
11:50 24mTalk | Preservation of Speculative Constant-time by Compilation PriSC Santiago Arranz Olmos Max Planck Institute for Security and Privacy, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter Max Planck Institute for Security and Privacy, Benjamin Gregoire INRIA, Vincent Laporte Inria | ||
12:15 15mTalk | Lightning talks PriSC | ||
14:00 - 15:30 | |||
14:00 30mTalk | An Isabelle formalization of co-rewrite pairs for non-reachability in conditional rewriting CPP Dohan Kim University of Innsbruck, Teppei Saito Japan Advanced Institute of Science and Technology, Japan, René Thiemann University of Innsbruck, Akihisa Yamada National Institute of Informatics | ||
14:30 30mTalk | Intrinsically Correct Sorting in Cubical Agda CPP Cass Alexandru RPTU Kaiserslautern-Landau, Vikraman Choudhury Università di Bologna & Inria OLAS, Jurriaan Rot Radboud University Nijmegen, Niels van der Weide Radboud University | ||
15:00 30mTalk | Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems CPP | ||
14:00 - 15:30 | |||
14:00 24mTalk | Auditing Rust Crates Effectively PriSC Lydia Zoghbi University of California, San Diego, David Thien University of California, San Diego, Ranjit Jhala UCSD, Deian Stefan University of California at San Diego, Caleb Stanford University of California, Davis | ||
14:25 24mTalk | Automatic Inference of Enclave Placement in LLVM Compiler PriSC Wesley B Nuzzo University of Massachusetts, Lowell (UML), Mohamed Elwakil U.S. Coast Guard Academy, Anitha Gollamudi University of Massachusetts Lowell | ||
14:50 24mTalk | Counterexamples in Safe Rust PriSC | ||
15:15 15mTalk | Lightning talks PriSC | ||
16:00 - 17:30 | |||
16:00 30mTalk | Formalized Burrows-Wheeler Transform CPP Louis Cheung University of Melbourne, Alistair Moffat The University of Melbourne, Christine Rizkallah University of Melbourne | ||
16:30 30mTalk | Verified and Efficient Matching of Regular Expressions with Lookaround CPP Agnishom Chattopadhyay Rice University, Wu Angela Li Rice University, Konstantinos Mamouras Rice University | ||
17:00 30mTalk | Further Tackling Post Correspondence Problem and Proof Generation CPP Akihiro Omori Department of Mathematical and Computing Science, Tokyo Institute of Technology, Yasuhiko Minamide Tokyo Institute of Technology | ||
16:00 - 17:30 | |||
16:00 24mTalk | BeePL: Correct-by-compilation kernel extensions PriSC Swarn Priya Virginia Tech, Tim Steenvoorden Open Universiteit, Connor Sughrue Virginia Tech, Frédéric Besson Inria, Rennes, Freek Verbeek Open Universiteit & Virginia Tech | ||
16:25 24mTalk | Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations PriSC Julian Rosemann Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus, Deepak Garg MPI-SWS | ||
16:50 24mTalk | SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations PriSC | ||
17:15 15mDay closing | Closing Remarks PriSC | ||
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mKeynote | CRIS: The power of imagination in specification and verification CPP | ||
10:00 30mTalk | The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic CPP Simon Friis Vindum Aarhus University, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Lars Birkedal Aarhus University | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Welcome PEPM Y. Annie Liu Stony Brook University | ||
09:10 50mKeynote | The Missing Diagonal: High Level Languages for Low Level Systems (Invited Talk Abstract) PEPM Satnam Singh Groq | ||
10:00 30mResearch paper | A type safe calculus for generating syntax-directed editors PEPM Andreas Tor Mortensen Department of Computer Science, Aalborg University, Benjamin Bennetzen Department of Computer Science, Aalborg University, Nikolaj Rossander Kristensen Department of Computer Science, Aalborg University, Peter Buus Steffensen Department of Computer Science, Aalborg University, Hans Hüttel Department of Computer Science, Aalborg University, Sune Skaaning Engtorp Department of Computer Science, University of Copenhagen | ||
11:00 - 12:30 | |||
11:00 30mTalk | Leakage-Free Probabilistic Jasmin Programs CPP Denis Firsov Tallinn University of Technology, Tiago Oliveira SandboxAQ, José Bacelar Almeira University of Minho & INESC TEC, Dominique Unruh RWTH Aachen | ||
11:30 30mTalk | Formally verified hardening of C programs against hardware fault injection CPP Basile Pesin Ecole Nationale de l'Aviation Civile (ENAC), Sylvain Boulmé Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, David Monniaux CNRS, Marie-Laure Potet Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG Pre-print | ||
12:00 30mTalk | CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq CPP Wolfgang Meier Aarhus University, Martin Jensen Aarhus University, Jean Pichon-Pharabod Aarhus University, Bas Spitters Aarhus University | ||
11:00 - 12:30 | Language design, pedagogical tool, and staged interpreterPEPM at Room 6 Chair(s): Sam Lindley The University of Edinburgh | ||
11:00 45mKeynote | The Ethical Compiler: Addressing the Is-Ought Gap in Compilation (Invited Talk) PEPM William J. Bowman University of British Columbia DOI Pre-print | ||
11:45 30mResearch paper | Algebraic Stepper for Simple Modules PEPM | ||
12:15 15mShort-paper | Collapsing Towers for Side-Channel Security (Short Paper) PEPM Cameron Wong Harvard SEAS, Muhammad Abdullah MIT, Yuheng Yang MIT, Mengjia Yan MIT, Adam Chlipala Massachusetts Institute of Technology, Nada Amin Harvard University File Attached | ||
14:00 - 15:30 | |||
14:00 30mTalk | Nominal Matching Logic With Fixpoints CPP | ||
14:30 30mTalk | Tactic Script Optimisation for Aesop CPP Jannis Limperg University of Munich (LMU) | ||
15:00 30mTalk | An Isabelle/HOL Framework for Synthetic Completeness Proofs CPP Asta Halkjær From University of Copenhagen | ||
14:00 - 15:30 | |||
14:00 45mKeynote | A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract) PEPM Brigitte Pientka McGill University | ||
14:45 30mResearch paper | Typed Program Analysis Without Encodings PEPM | ||
15:15 15mShort-paper | A Fuelled Self-Reducer for System T (Short Paper) PEPM Greg Brown University of Edinburgh File Attached | ||
16:00 - 17:30 | |||
16:00 30mTalk | Formalization of Differential Privacy in Isabelle/HOL CPP | ||
16:30 30mTalk | A CHERI C Memory Model for Verified Temporal Safety CPP Vadim Zaliva University of Cambridge, UK, Kayvan Memarian University of Cambridge, Brian Campbell University of Edinburgh, Ricardo Almeida University of Edinburgh, Nathaniel Filardo University of Cambridge, Ian Stark The University of Edinburgh, Peter Sewell University of Cambridge | ||
17:00 30mTalk | Formalizing the One-way to Hiding Theorem CPP | ||
16:00 - 17:30 | |||
16:00 15mShort-paper | Type-Sensitive Algebraic Macros (Short Paper)Remote PEPM File Attached | ||
16:15 30mResearch paper | Characterizations of Partial Well-Behaved Lenses PEPM Keishi HASHIBA The University of Osaka, Keisuke Nakano Tohoku University, Kazuyuki Asada Tohoku University, Kentaro Kikuchi Tohoku University | ||
16:45 40mPanel | Semantics-based program manipulation in the age of LLMs PEPM William J. Bowman University of British Columbia, Brigitte Pientka McGill University, Satnam Singh Groq | ||
17:25 5mDay closing | Farewell PEPM Y. Annie Liu Stony Brook University | ||
Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change
Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change
10:40 - 12:00 | |||
10:40 20mTalk | Maximal Simplification of Polyhedral Reductions POPL Louis Narmour Colorado State University, Tomofumi Yuki , Sanjay Rajopadhye Colorado State University | ||
11:00 20mTalk | 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 20mTalk | The Best of Abstract Interpretations POPL Roberto Giacobazzi University of Arizona, Francesco Ranzato Dipartimento di Matematica, University of Padova, Italy | ||
11:40 20mTalk | 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 | |||
13:20 20mTalk | Linear and non-linear relational analyses for Quantum Program Optimization POPL | ||
13:40 20mTalk | Automating equational proofs in Dirac notation POPL Yingte Xu MPI-SP and Institute of Software, Chinese Academy of Sciences, Gilles Barthe MPI-SP; IMDEA Software Institute, Li Zhou Institute of Software, Chinese Academy of Sciences | ||
14:00 20mTalk | Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages POPL Andrea Colledan University of Bologna & INRIA Sophia Antipolis, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis | ||
13:20 - 14:20 | |||
13:20 20mTalk | Axe 'Em: Eliminating Spurious States with Induction Axioms POPL | ||
13:40 20mTalk | 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 20mTalk | 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 | |||
15:00 20mTalk | A quantitative probabilistic relational Hoare logic POPL Martin Avanzini Inria, Gilles Barthe MPI-SP; IMDEA Software Institute, Benjamin Gregoire INRIA, Davide Davoli Université Côte d’Azur, Inria | ||
15:20 20mTalk | Approximate Relational Reasoning for Higher-Order Probabilistic Programs POPL Philipp G. Haselwarter Aarhus University, Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University Pre-print | ||
15:40 20mTalk | Compositional imprecise probability: a solution from graded monads and Markov categories POPL | ||
16:00 20mTalk | Sound and Complete Proof Rules for Probabilistic Termination POPL | ||
15:00 - 16:20 | |||
15:00 20mTalk | 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 20mTalk | Finite-Choice Logic Programming POPL Pre-print | ||
15:40 20mTalk | 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 20mTalk | 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 | |||
17:00 20mTalk | 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 20mTalk | 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 20mTalk | 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 JanDisplayed time zone: Mountain Time (US & Canada) change
Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change
10:40 - 12:00 | |||
10:40 20mTalk | Inference Plans for Hybrid Particle Filtering POPL Ellie Y. Cheng MIT, Eric Atkinson , Guillaume Baudart Inria, Louis Mandel IBM Research, USA, Michael Carbin Massachusetts Institute of Technology | ||
11:00 20mTalk | Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops POPL Pre-print | ||
11:20 20mTalk | Modelling Recursion and Probabilistic Choice in Guarded Type Theory POPL Philipp Stassen Aarhus University, Rasmus Ejlers Møgelberg IT University of Copenhagen, Maaike Annebet Zwart IT University of Copenhagen, Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University | ||
11:40 20mTalk | Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning POPL Jialu Bao Cornell University, Emanuele D'Osualdo University of Konstanz, Azadeh Farzan University of Toronto | ||
10:40 - 12:00 | |||
10:40 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | Biparsers: Exact Printing for Data Synchronisation POPL | ||
13:20 - 14:20 | |||
13:20 20mTalk | The Decision Problem for Regular First Order Theories POPL Umang Mathur National University of Singapore, David Mestel Maastricht University, Mahesh Viswanathan University of Illinois at Urbana-Champaign | ||
13:40 20mTalk | A Primal-Dual Perspective on Program Verification Algorithms POPL Takeshi Tsukada Chiba University, Hiroshi Unno Tohoku University, Oded Padon Weizmann Institute of Science, Sharon Shoham Tel Aviv University | ||
14:00 20mTalk | Dis/Equality Graphs POPL George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Jahrim Gabriele Cesario University of St. Gallen, Guido Salvaneschi University of St. Gallen | ||
13:20 - 14:20 | |||
13:20 20mTalk | Program logics à la carte POPL Max Vistrup ETH Zurich, Michael Sammler Institute of Science and Technology Austria, Ralf Jung ETH Zurich | ||
13:40 20mTalk | 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 20mTalk | 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 | |||
15:00 20mTalk | A Dependent Type Theory for Meta-programming with Intensional Analysis POPL | ||
15:20 20mTalk | Avoiding signature avoidance in ML modules with zippers POPL | ||
15:40 20mTalk | Bidirectional Higher-Rank Polymorphism with Intersection and Union Types POPL | ||
16:00 20mTalk | Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs POPL | ||
15:00 - 16:20 | |||
15:00 20mTalk | 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 20mTalk | RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency POPL | ||
15:40 20mTalk | 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 20mTalk | Model Checking C/C++ with Mixed-Size Accesses POPL | ||
17:00 - 17:40 | |||
17:00 20mTalk | Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime POPL | ||
17:20 20mTalk | Verifying Quantum Circuits with Level-Synchronized Tree Automata POPL Parosh Aziz Abdulla Uppsala University, Sweden, Yo-Ga Chen Academia Sinica, Yu-Fang Chen Academia Sinica, Lukáš Holík Brno University of Technology, Ondřej Lengál Brno University of Technology, Jyun-Ao Lin National Taipei University of Technology, Fang-Yi Lo Academia Sinica, Wei-Lun Tsai Academia Sinica | ||
17:00 - 17:40 | |||
17:00 20mTalk | 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 20mTalk | Algebras for Deterministic Computation are Inherently Incomplete POPL | ||
Fri 24 JanDisplayed time zone: Mountain Time (US & Canada) change
Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change
10:40 - 12:00 | |||
10:40 20mTalk | MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age POPL Roland Leißa University of Mannheim, School of Business Informatics and Mathematics, Marcel Ullrich Saarland University, Joachim Meyer Compiler Design Lab; Saarland Informatics Campus; Saarland University, Sebastian Hack Saarland University, Saarland Informatics Campus | ||
11:00 20mTalk | Simple Linear Loops: Algebraic Invariants and Applications POPL Rida Ait El Manssour CNRS & IRIF, Paris, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS & IRIF, Paris, Anton Varonka TU Wien | ||
11:20 20mTalk | Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus POPL Yufan Cai National University of Singapore, Zhe Hou Griffith University, David Sanan Nanyang Technological University, Singapore, Xiaokun Luan Peking University, Yun Lin Shanghai Jiao Tong University, Jun Sun Singapore Management University, Jin Song Dong National University of Singapore | ||
11:40 20mTalk | Tail Modulo Cons, OCaml, and Relational Separation Logic POPL Clément Allain INRIA, Frédéric Bour Tarides, Basile Clément OCamlPro, François Pottier Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS | ||
10:40 - 12:00 | |||
10:40 20mPaper | Affect: An Affine Type and Effect System POPL Link to publication | ||
11:00 20mTalk | A modal deconstruction of Löb induction POPL Daniel Gratzer Aarhus University | ||
11:20 20mTalk | QuickSub: Efficient Iso-Recursive Subtyping POPL | ||
11:40 20mTalk | Generic Refinement Types POPL Nico Lehmann UCSD, Cole Kurashige UCSD, Nikhil Akiti UCSD, Niroop Krishnakumar UCSD, Ranjit Jhala UCSD | ||
13:20 - 14:20 | |||
13:20 20mTalk | Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting POPL Yonghyun Kim Seoul National University, South Korea, Minki Cho Seoul National University, Jaehyung Lee Seoul National University, Jinwoo Kim Seoul National University, Taeyoung Yoon Seoul National University, Youngju Song MPI-SWS, Chung-Kil Hur Seoul National University | ||
13:40 20mResearch paper | Formalising Graph Algorithms with Coinduction POPL Pre-print | ||
14:00 20mTalk | VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems POPL Yoonseung Kim Yale University, Sung-Hwan Lee Seoul National University, Yonghyun Kim Seoul National University, South Korea, Chung-Kil Hur Seoul National University | ||
13:20 - 14:20 | |||
13:20 20mTalk | BiSikkel: A Multimode Logical Framework in Agda POPL | ||
13:40 20mTalk | Calculational Design of Hyperlogics by Abstract Interpretation POPL | ||
14:00 20mTalk | 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 20mTalk | Flo: a Semantic Foundation for Progressive Stream Processing POPL Shadaj Laddad University of California at Berkeley, Alvin Cheung University of California at Berkeley, Joseph M. Hellerstein UC Berkeley, Mae Milano Princeton University Pre-print | ||
15:20 20mTalk | Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types POPL | ||
15:40 20mTalk | Semantic Logical Relations for Timed Message-Passing Protocols POPL Yue Yao Carnegie Mellon University, Grant Iraci University at Buffalo, Cheng-En Chuang University at Buffalo, Stephanie Balzer Carnegie Mellon University, Lukasz Ziarek University at Buffalo | ||
16:00 20mTalk | Reachability Analysis of the Domain Name System POPL | ||
15:00 - 16:20 | |||
15:00 20mTalk | The Duality of λ-Abstraction POPL | ||
15:20 20mTalk | On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus POPL Naoki Kobayashi University of Tokyo | ||
15:40 20mTalk | 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 20mTalk | 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 | |||
17:00 20mTalk | Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks POPL Xaver Fabian CISPA, Marco Patrignani University of Trento, Marco Guarnieri IMDEA Software Institute, Michael Backes Cispa Helmholtz Center for Information Security | ||
17:20 20mTalk | Preservation of speculative constant-time by compilation POPL Santiago Arranz Olmos Max Planck Institute for Security and Privacy, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter Max Planck Institute for Security and Privacy, Benjamin Gregoire INRIA, Vincent Laporte Inria | ||
17:40 20mTalk | SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations POPL | ||
17:00 - 18:00 | |||
17:00 20mTalk | 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 20mTalk | 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 20mTalk | 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 JanDisplayed time zone: Mountain Time (US & Canada) change
Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 50mKeynote | Elpi: rule-based meta-languge for Rocq CoqPL Enrico Tassi INRIA | ||
09:50 20mTalk | Implementing OCaml APIs in Coq CoqPL Joshua M. Cohen Princeton University | ||
10:10 20mTalk | Towards general white-box automation: a typeclass-guided context cleaner CoqPL Thibaut Pérami University of Cambridge | ||
11:00 - 12:30 | |||
11:00 70mPanel | Session with the Coq Development Team CoqPL | ||
12:10 20mTalk | Vellvm: Formalizing the Informal CoqPL Calvin Beck University of Pennsylvania, USA, Hanxi Chen , Steve Zdancewic University of Pennsylvania | ||
14:00 - 15:30 | |||
14:00 22mTalk | 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 22mTalk | A Framework of Differential Operators CoqPL | ||
14:45 22mTalk | 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 22mTalk | Formal Verification of a Software Defined Delay-Tolerant Network CoqPL Jan-Paul Ramos-Davila Cornell University | ||
16:00 - 17:30 | |||
16:00 22mTalk | Towards Automated Verification of LLM-Synthesized C Programs CoqPL | ||
16:22 22mTalk | 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 22mTalk | CoqNFU: Towards Formalizing NFU in Coq CoqPL | ||
17:07 22mTalk | Formal Verification of Quantum Stabilizer Code CoqPL | ||