Filter Program
Dates
Rooms
Tracks
Badges
Your Program
This program is tentative and subject to change.
Sun 11 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 12mDay opening | Day opening Dafny | ||
09:12 60mKeynote | Software Verification meets Real-World Cryptography Dafny Karthikeyan Bhargavan Cryspen, France | ||
10:12 18mTalk | The Design of an Interactive Proof Mode for Dafny Dafny Ștefan Ciobâcă Alexandru Ioan Cuza University of Iasi, K. Rustan M. Leino Amazon, Ștefan Mercaș Alexandru Ioan Cuza University, Iasi, Romania, Roxana-Mihaela Timon Alexandru Ioan Cuza University, Iasi, Romania | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Creusot: Formal verification of Rust programs Tutorials Li-yao Xia LMF, Inria, Université Paris-Saclay, Jacques-Henri Jourdan LMF, CNRS, Université Paris-Saclay, Arnaud Golfouse Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France, Vincent Lafeychine Université Paris-Saclay, CNRS, ENS Paris-Saclay, INRIA, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France. Media Attached | ||
09:00 - 10:30 | |||
09:00 90mTutorial | BINSEC: Adapting Symbolic Execution for Binary-level Security Tutorials Sébastien Bardin CEA LIST, University Paris-Saclay, Frédéric Recoules CEA, List, Yanis Sellami CEA, List, Univ. Grenoble Alpes | ||
09:00 - 10:00 | |||
09:00 5mDay opening | Day opening PriSC | ||
09:05 55mKeynote | The V8 Sandbox: From Compiler Correctness to Runtime Containment PriSC Samuel Groß Google | ||
10:00 - 10:30 | Information Flow ControlPriSC at Salle 19 Chair(s): David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break POPL Catering | ||
11:00 - 12:30 | |||
11:00 18mTalk | Diagnostics in Probabilistic Program Verification Dafny Philipp Schröer RWTH Aachen University, Darion Haase RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University | ||
11:18 18mTalk | Explicit Abstraction Barrier for Autoactive Verification Dafny Paul Patault Université Paris-Saclay - Laboratoire de Méthodes Formelles Pre-print | ||
11:36 18mTalk | Managing the Proof Context in SPARK Dafny File Attached | ||
11:54 18mTalk | Tunable Automation in Automated Program Verification Dafny Alexander Bai New York University, Chris Hawblitzel Microsoft Research, Andrea Lattuada VMware Research Pre-print | ||
12:12 18mTalk | Velvet: A Multi-Modal Verifier for Effectful Programs Dafny Vladimir Gladshtein , George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore, Vitaly Kurin Neapolis University Pafos, Ilya Sergey National University of Singapore Pre-print | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Creusot: Formal verification of Rust programs Tutorials Li-yao Xia LMF, Inria, Université Paris-Saclay, Jacques-Henri Jourdan LMF, CNRS, Université Paris-Saclay, Arnaud Golfouse Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France, Vincent Lafeychine Université Paris-Saclay, CNRS, ENS Paris-Saclay, INRIA, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France. Media Attached | ||
11:00 - 12:30 | |||
11:00 55mKeynote | A Welcome to Causal Probabilistic Programming LAFI | ||
11:56 10mTalk | Verifying Sampling Algorithms via Distributional Invariants LAFI Daniel Zilken , Tobias Winkler RWTH Aachen University, Kevin Batz RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University Media Attached File Attached | ||
12:08 10mTalk | Sequential Monte Carlo Program Synthesis with Refinement Proposals LAFI Maddy Bowers Massachusetts Institute of Technology, Mauricio Barba da Costa MIT, Xiaoyan Wang Massachusetts Institute of Technology, Joshua B. Tenenbaum Massachusetts Institute of Technology, Vikash Mansinghka Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology, Alexander K. Lew Yale University | ||
12:20 10mTalk | A Word Sampler for Well-Typed Functions LAFI Pre-print File Attached | ||
11:00 - 12:30 | |||
11:00 90mTutorial | BINSEC: Adapting Symbolic Execution for Binary-level Security Tutorials Sébastien Bardin CEA LIST, University Paris-Saclay, Frédéric Recoules CEA, List, Yanis Sellami CEA, List, Univ. Grenoble Alpes | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch POPL Catering | ||
14:00 - 15:30 | |||
14:00 18mTalk | Lessons from Building an Auto-Active Verifier in Lean Dafny George Pîrlea National University of Singapore, Vladimir Gladshtein , Qiyuan Zhao National University of Singapore, Ilya Sergey National University of Singapore Pre-print | ||
14:18 18mTalk | Formal Verification of Minimax Algorithms Dafny Wieger Wesselink Eindhoven University of Technology, Kees Huizing Eindhoven University of Technology, Huub van de Wetering Eindhoven University of Technology File Attached | ||
14:36 18mTalk | Teaching Automata Theory and Formal Languages with Dafny Dafny Ran Ettinger NVIDIA Pre-print | ||
14:54 18mTalk | Verification of E-Voting Algorithms in Dafny Dafny Robert Büttner University of Regensburg, Fabian Franz Dießl University of Regensburg, Patrick Janoschek University of Regensburg, Ivana Kostadinovic University of Regensburg, Henrik Oback University of Regensburg, Kilian Voß University of Regensburg, Franziska Alber University of Regensburg, Roland Herrmann University of Regensburg, Sibylle Möhle University of Regensburg, Philipp Rümmer University of Regensburg and Uppsala University Pre-print | ||
15:12 18mTalk | A Correct-by-Construction Checker for Validation of Railway Data Dafny Benoît Boyer Mitsubishi Electric R&D Centre Europe, Rennes, France, Noé Canva Inria Saclay & Université Paris-Saclay, Matteo Manighetti IRIF, Université Paris Cité, Claude Marché Inria Saclay & Université Paris-Saclay Link to publication | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Verifying Probabilistic Programs Using Separation Logic Tutorials Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen CISPA Helmholtz Center for Information Security, Philipp G. Haselwarter Aarhus University Link to publication | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Discrete and Continuous Models for Concurrent Systems: From Petri Nets to Directed Spaces Tutorials Uli Fahrenberg Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF | ||
14:00 - 15:30 | |||
14:00 18mTalk | Efficient Dependency Resolution in IFC-aware Decentralized Programming PriSC | ||
14:18 18mTalk | Tooling Design and Lessons Learned from Systematic Evaluations of the Preservation of Low-level Security Properties by Compilers with BinSec PriSC Yanis Sellami CEA, List, Univ. Grenoble Alpes, Frédéric Recoules CEA, List, Sébastien Bardin CEA LIST, University Paris-Saclay | ||
14:36 18mTalk | Decompiling for Constant-Time Analysis PriSC Sören van der Wall TU Braunschweig, 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, Youcef Bouzid , Zhiyuan Zhang | ||
14:54 18mTalk | Modular Verification of Probabilistic Constant-Time PriSC Xingyu Xie MPI-SP | ||
15:12 18mTalk | GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses PriSC Pierrick Philippe Univ Rennes, CNRS, IRISA, Mohamed Sabt Univ Rennes, CNRS, IRISA, Pierre-Alain Fouque Univ Rennes, CNRS, IRISA | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break POPL Catering | ||
16:00 - 18:00 | |||
16:00 18mTalk | ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis Dafny Mantas Bakšys University of Cambridge, Stefan Zetzsche Amazon Web Services, Olivier Bouissou Amazon Web Services, Soonho Kong Amazon Web Services, Remi Delmas Amazon Web Services Pre-print | ||
16:18 18mTalk | A benchmark for vericoding: formally verified program synthesis Dafny Sergiu Bursuc Beneficial AI Foundation, Theodore Ehrenborg Beneficial AI Foundation, Shaowei Lin Beneficial AI Foundation, Lăcrămioara Aștefănoaei Beneficial AI Foundation, Ionel Emilian Chiosa MIT, Jure Kukovec Beneficial AI Foundation, Alok Singh Beneficial AI Foundation, Oliver Butterley Beneficial AI Foundation, Adem Bizid MIT, Quinn Dougherty Beneficial AI Foundation, Miranda Zhao MIT, Max Tan MIT, Max Tegmark Massachusetts Institute of Technology Pre-print File Attached | ||
16:36 18mTalk | DafnyPro: LLM-Assisted Automated Verification for Dafny Programs Dafny | ||
16:54 18mTalk | MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification Dafny Mantas Bakšys University of Cambridge, Stefan Zetzsche Amazon Web Services, Olivier Bouissou Amazon Web Services Pre-print | ||
17:12 18mTalk | Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs Dafny Valentina Wu Faculdade de Engenharia, Universidade do Porto, Alexandra Mendes Faculty of Engineering, University of Porto & INESC TEC, Alexandre Abreu INESC TEC, Faculdade de Engenharia, Universidade do Porto | ||
17:30 18mTalk | Toward Automated, Contamination-free Dafny Benchmark Generation Dafny Changjie Wang KTH Royal Institute of Technology, Mariano Scazzariello RISE Research Institutes of Sweden, Dejan Kostic KTH Royal Institute of Technology, Marco Chiesa KTH Royal Institute of Technology Pre-print | ||
17:48 12mDay closing | Day closing Dafny | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Verifying Probabilistic Programs Using Separation Logic Tutorials Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen CISPA Helmholtz Center for Information Security, Philipp G. Haselwarter Aarhus University Link to publication | ||
16:00 - 18:00 | |||
16:00 10mTalk | Multi-Agent Systems for Traceable Bayesian Workflow LAFI Xianda Sun University of Cambridge, Andrew D. Gordon Cogna and University of Edinburgh, Hong Ge University of Cambridge File Attached | ||
16:12 10mTalk | Grammar-Constrained LLM Generation for Reliable and Efficient Probabilistic Program Synthesis LAFI Madhav Kanda University of Illinois Urbana-Champaign, Shubham Ugare Meta, Sasa Misailovic University of Illinois at Urbana-Champaign | ||
16:24 10mTalk | Language-Model Probabilistic Programming for Improving Autoformalization via Cycle Consistency and Incremental Type-Checking LAFI Mauricio Barba da Costa MIT, Fabian Zaiser MIT, Katherine Collins MIT, Romir Patel MIT, Timothy O'Donnell , Alexander K. Lew Yale University, Joshua B. Tenenbaum Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Cameron Freer Massachusetts Institute of Technology | ||
16:35 80mPoster | Poster Session LAFI | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Discrete and Continuous Models for Concurrent Systems: From Petri Nets to Directed Spaces Tutorials Uli Fahrenberg Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF | ||
17:30 - 18:00 | |||
17:30 25mTalk | Lightning Talks PriSC | ||
17:55 5mDay closing | Day closing PriSC | ||
18:00 - 22:00 | |||
19:00 3hDinner | PriSC Dinner @ Crêperie l'Épi de Blé Rennes PriSC | ||
Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 60mKeynote | How can Machine Learning Help Formal Proving ? CPP | ||
10:08 22mTalk | Higher order differential calculus in Mathlibdistinguished paper CPP Sebastien Gouezel CNRS and Rennes University | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Current State of the Industrial-Strength Infer Static Analysis Platform VMCAI David Pichardie Meta | ||
10:00 30mTalk | Try-Mopsa: Relational Static Analysis in Your Pocket VMCAI Raphaël Monat Inria and University of Lille Pre-print | ||
09:00 - 10:30 | |||
09:30 60mKeynote | Declarative Programming: Efficient and reliable programming with human intelligence (Invited Talk) PADL Michael Hanus Kiel University | ||
09:00 - 10:30 | |||
09:00 10mTalk | Opening AddressTalk PLanQC Vladimir Zamdzhiev Inria File Attached | ||
09:10 20mTalk | Traq: Estimating the Quantum Cost of Classical ProgramsTalk PLanQC Anurudh Peduri Ruhr University Bochum, Jam Kabeer Ali Khan Standard Chartered Bank; Max Planck Institute for Security and Privacy (MPI-SP), Gilles Barthe MPI-SP; IMDEA Software Institute, Michael Walter Ruhr-Universität Bochum File Attached | ||
09:30 20mTalk | Programming Abstractions for Quantum Linear AlgebraTalk PLanQC Charles Yuan University of Wisconsin–Madison File Attached | ||
09:50 20mTalk | Verifying Repeat-Until-Success Circuits with AutoQTalk PLanQC Jyun-Ao Lin National Taipei University of Technology, Yu-Fang Chen Academia Sinica, Jakub Havlík Brno University of Technology, Ondřej Lengál Brno University of Technology, Fang-Yi Lo Academia Sinica, Wei-Lun Tsai Academia Sinica File Attached | ||
10:10 20mTalk | VC-Qiskit: Automated–Interactive Verification of Qiskit Passes with Minimal IntrusionTalk PLanQC Xiaoquan Xu , Li Zhou Institute of Software at Chinese Academy of Sciences, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation Tutorials Sasa Misailovic University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Shubham Ugare Meta, Debangshu Banerjee UIUC, Tarun Suresh University of Illinois, Urbana-Champaign, Adharsh Kamath University of Illinois at Urbana-Champaign | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break POPL Catering | ||
11:00 - 12:50 | Formalized mathematicsCPP at Belvédère Chair(s): Marie Kerjean CNRS, Université Sorbonne Paris Nord, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio Inria, Université Jean Monnet Saint-Étienne | ||
11:00 22mTalk | Bar Inductive Predicates for Constructive Algebra in Rocq CPP Dominique Larchey-Wendling Université de Lorraine, CNRS, LORIA DOI Pre-print | ||
11:22 22mTalk | Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq CPP Holger Thies Kyoto University | ||
11:44 22mTalk | Cylindrical Algebraic Decomposition in Coq/Rocq CPP Quentin Vermande Université Côte d'Azur, Inria | ||
12:06 22mTalk | Adhesive Category Theory for Graph Rewriting in Rocq CPP | ||
12:28 22mTalk | Formalizing polynomial laws and the universal divided power algebra CPP | ||
11:00 - 12:30 | |||
11:00 30mTalk | Data Race Detection by Digest-Driven Abstract Interpretation VMCAI Pre-print | ||
11:30 30mTalk | Termination Resilience Static Analysis VMCAI Naïm Moussaoui Remil Inria & ENS | PSL, Paris, France, Caterina Urban Inria Paris - ENS - Université PSL | ||
12:00 30mTalk | Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification VMCAI Andreas Lindner Uppsala universitet, Karl Palmskog KTH Royal Institute of Technology, Scott Constable Intel Corporation, Mads Dam KTH, Roberto Guanciale KTH Royal Institute of Technology, Hamed Nemati KTH Royal Institute of Technology | ||
11:00 - 12:30 | |||
11:00 30mTalk | An efficient compiler for the IDP-Z3 knowledge base system PADL Wout Piessens KU Leuven, Belgium, Simon Vandevelde KU Leuven, Belgium, Joost Vennekens KU Leuven, Tom Schrijvers KU Leuven | ||
11:30 30mTalk | Multi-Configurable Search Rules in Prolog and Application to Testing PADL Daniela Ferreiro Technical University of Madrid and IMDEA Software Institute, José Morales IMDEA Software Institute, Pedro López-García IMDEA Software Institute, Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute | ||
12:00 30mTalk | Using Prolog to Translate Set Theory and B to SAT PADL Michael Leuschel HHU | ||
11:00 - 12:30 | |||
11:00 45mKeynote | Building the Cloud with Continuous Assurances using Static Analysis TPSA Subarno Banerjee Amazon Web Services | ||
11:45 22mTalk | Tracking Dynamically Bound Variable Dependencies TPSA | ||
12:07 23mTalk | Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach TPSA Rini Banerjee University of Cambridge, Zain K Aamer University of Pennsylvania, Hiroyuki Katsura University of Cambridge, David Kaloper-Meršinjak University of Cambridge, Dimitrios J. Economou University of Cambridge, Kayvan Memarian University of Cambridge, Dhruv Makwana University of Cambridge, Neel Krishnaswami University of Cambridge, Benjamin C. Pierce University of Pennsylvania, Christopher Pulte University of Cambridge, Peter Sewell University of Cambridge | ||
11:00 - 12:30 | |||
11:00 45mKeynote | Democratizing quantum formal verification: the path-sum wayKeynote PLanQC Christopĥe Chareton CEA, LIST, France | ||
11:45 20mTalk | One rig to control them allTalk PLanQC Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark, Louis Lemonnier University of Edinburgh File Attached | ||
12:05 20mTalk | Quantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic ApproachTalk PLanQC File Attached | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Syntactically and Semantically Constraining LLMs with Guarantees using Structured LLM Generation Tutorials Sasa Misailovic University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Shubham Ugare Meta, Debangshu Banerjee UIUC, Tarun Suresh University of Illinois, Urbana-Champaign, Adharsh Kamath University of Illinois at Urbana-Champaign | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch POPL Catering | ||
14:00 - 15:30 | Proof assistantsCPP at Belvédère Chair(s): Sophie Tourret Inria and Max Planck Institute for Informatics | ||
14:00 22mTalk | A Certifying Proof Assistant for Synthetic Mathematics in Lean CPP Wojciech Nawrocki Carnegie Mellon University, Joseph Hua Carnegie Mellon University, Mario Carneiro Chalmers University of Technology, Yiming Xu LMU Munich, Spencer Woolfson Carnegie Mellon University, Shuge Rong Carnegie Mellon University, Sina Hazratpour Johns Hopkins University, Steve Awodey Carnegie Mellon University | ||
14:22 22mTalk | Adding Sorts to an Isabelle Formalization of Superposition CPP Balazs Toth Ludwig-Maximilians-Universität München, Martin Desharnais Ludwig-Maximilians-Universität München, Jasmin Blanchette Ludwig-Maximilians-Universität München | ||
14:45 22mTalk | A Lambda-Superposition Tactic for Isabelle/HOL CPP Massin Guerdi Ludwig-Maximilians-Universität München | ||
15:07 22mTalk | Certifying the decidability of the word problem in monoids at large CPP Reinis Cirpons St Andrews University, Florent Hivert Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA, Assia Mahboubi INRIA, Guillaume Melquiond Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, James Mitchell St Andrews University, Finn Smith St Andrews University | ||
14:00 - 15:30 | |||
14:00 60mKeynote | Understanding Transformers through the Lens of Logic and Automata VMCAI Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS | ||
15:00 30mTalk | Proof Minimization in Neural Network Verification VMCAI Omri Isac The Hebrew University of Jerusalem, Idan Refaeli Hebrew University of Jerusalem, Haoze Wu Stanford University, Clark Barrett Stanford University, Guy Katz The Hebrew University of Jerusalem | ||
14:00 - 15:30 | |||
14:00 30mTalk | Property-Based Testing for Asynchronous Functional Reactive Programming Using Linear Temporal Logic PADL Christian Emil Nielsen IT University of Copenhagen, Mathias Faber Kristiansen IT University of Copenhagen, Patrick Bahr IT University of Copenhagen | ||
14:30 30mTalk | Graph Rewriting Language as a Platform for Quantum Diagrammatic Calculi PADL Kayo Tei Waseda University, Haruto Mishina Waseda University, Naoki Yamamoto Waseda University, Kazunori Ueda Waseda University | ||
15:00 30mTalk | Solving hard combinatorial optimization problems with PyQASP PADL Damiano Azzolini University of Ferrara, Nicola Leone University of Calabria, Italy, Giuseppe Mazzotta University of Calabria, Fracesco Ricca University of Calabria | ||
14:00 - 15:30 | |||
14:00 22mTalk | Soteria Rust: Efficient Symbolic Execution for Rust TPSA Opale Sjöstedt Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London | ||
14:22 22mTalk | Towards automatic functional correctness in the Mopsa static analyzer TPSA Milla Valnet Sorbonne Université, Raphaël Monat Inria and University of Lille, Antoine Miné Sorbonne Université | ||
14:45 22mTalk | An LLVM frontend for Infer for Swift analysis TPSA Dulma Churchill Meta | ||
15:07 22mTalk | Specialisation: Context-Dependent Reasoning in Incorrectness Separation Logic TPSA Raquel Fernandes da Silva Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London, David Pichardie Meta | ||
14:00 - 15:30 | |||
14:00 90mTutorial | A Guided Tour through Oxidized OCaml Tutorials Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Veil: Automated and Interactive Verification of Transition Systems Tutorials | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break POPL Catering | ||
16:00 - 17:30 | |||
16:00 22mTalk | Mechanized Dominator Tree Certificationdistinguished paper CPP Jean-Christophe Léchenet Université Côte d’Azur, Inria DOI Pre-print | ||
16:22 22mTalk | Brack: A Verified Compiler for Scheme via CakeML CPP Pascal Lasnier University of Cambridge, Jeremy Yallop University of Cambridge, Magnus O. Myreen Chalmers University of Technology | ||
16:45 22mTalk | Verified VCG and Verified Compiler for Dafny CPP Daniel Nezamabadi ETH Zurich, Magnus O. Myreen Chalmers University of Technology, Yong Kiam Tan Institute for Infocomm Research, A*STAR | ||
17:07 22mTalk | Foundational Verification of Running-Time Bounds for Interactive Programs CPP Thomas Carotti MIT, Andy Tockman Massachussetts Institute of Technology, Pratap Singh CMU, Andres Erbsen Google, Samuel Gruetter ETH Zurich, Adam Chlipala Massachusetts Institute of Technology | ||
16:00 - 17:30 | Models 1VMCAI at Horizons Chair(s): Mihaela Sighireanu University Paris-Saclay, ENS Paris-Saclay, CNRS, LMF | ||
16:00 30mTalk | Verification of Generic VHDL Designs and Their Translation to Rocq VMCAI Ocan Sankur University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Benoît Boyer Mitsubishi Electric R&D Centre Europe, Rennes, France, Florian Faissole Mitsubishi Electric R&D Centre Europe | ||
16:30 30mTalk | A Formal Executable Semantics of PROMELA VMCAI | ||
17:00 30mTalk | Efficient Discovery of Actual Causality in Stochastic Systems VMCAI Arshia Rafieioskouei Michigan State University, Kenneth Rogale Michigan State University, Borzoo Bonakdarpour Michigan State University | ||
16:00 - 17:30 | PADL M4PADL at Salle 12 Chair(s): Nada Amin Harvard University, Joaquín Arias Universidad Rey Juan Carlos | ||
16:00 30mTalk | Declarative Debugging for Modern Networks PADL | ||
16:30 30mTalk | Interpretable Configuration Optimization for Static Program Verification via Rule-Based and Counterfactual Reasoning PADL Jaeseong Lee The University of Texas at Dallas, Sopam Dasgupta The University of Texas at Dallas, Gopal Gupta The University of Texas at Dallas, Shiyi Wei University of Texas at Dallas | ||
17:00 30mTalk | REGAL: Extracting implicit rules in text using LLMs with logic program feedback PADL Abhiramon Rajasekharan The University of Texas at Dallas, Gopal Gupta The University of Texas at Dallas | ||
16:00 - 17:30 | |||
16:00 22mTalk | How to identify security vulnerabilities in Node.js packages? TPSA José Fragoso Santos INESC-ID; Instituto Superior Técnico - University of Lisbon, Filipe Marques INESC-ID; Instituto Superior Técnico - University of Lisbon, André Nascimento INESC-ID; Instituto Superior Técnico - University of Lisbon | ||
16:22 22mTalk | Modeling Incorrectness and Unknown Functions with Angelic and Demonic Nondeterminism TPSA Noam Zilberstein Cornell University | ||
16:45 22mTalk | A logic for all reasons TPSA Flavio Ascari University of Konstanz, Roberto Bruni University of Pisa, Lorenzo Gazzella Università di Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy | ||
17:07 22mTalk | AMPLE: Fine-grained File Access Policies for Server Applications TPSA | ||
16:00 - 17:30 | |||
16:00 30m | Poster SessionPoster PLanQC | ||
16:30 20mTalk | Compiling Quantum Lambda-Terms into Circuits via the Geometry of InteractionTalk PLanQC Kostia Chardonnet Université de Lorraine, CNRS, Inria, LORIA, Ugo Dal Lago University of Bologna; Centre Inria d’Université Côte d’Azur, Naohiko Hoshino Sojo University, Paolo Pistone Université Claude Bernard Lyon 1 File Attached | ||
16:50 20mTalk | Towards a Hierarchical Quantum Circuit LanguageTalk PLanQC File Attached | ||
17:10 20mTalk | Denotational semantics for stabiliser quantum programsTalk PLanQC File Attached | ||
16:00 - 17:30 | |||
16:00 90mTutorial | A Guided Tour through Oxidized OCaml Tutorials Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Veil: Automated and Interactive Verification of Transition Systems Tutorials | ||
Tue 13 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Tue 13 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 60mKeynote | Specification, Semantics, and Verification of Quantum Programs CPP Jennifer Paykin University of Vermont | ||
10:00 30mMeeting | Business Meeting CPP | ||
09:00 - 10:30 | |||
09:00 60mKeynote | TypedC: Spatial Memory Safety for Low Level Programs by Abstract Interpretation VMCAI Mihaela Sighireanu University Paris-Saclay, ENS Paris-Saclay, CNRS, LMF | ||
10:00 30mTalk | Input-based Three-Valued Abstraction Refinement VMCAI | ||
09:00 - 10:30 | |||
09:30 60mKeynote | A positive perspective on term representation (Invited Talk) PADL Dale Miller INRIA Saclay and LIX/Institut Polytechnique de Paris | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Welcome from the Organizers RTFM Amal Ahmed Northeastern University, USA, Derek Dreyer MPI-SWS, Ilya Sergey National University of Singapore | ||
09:10 40mTalk | On long-term research vision RTFM Peter Sewell University of Cambridge | ||
09:50 40mTalk | On transitioning from academia to industry RTFM David Pichardie Meta | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Analyzing Shell Scripts Tutorials Michael Greenberg Stevens Institute of Technology, Konstantinos Kallas University of California, Los Angeles, Nikos Vasilakis Brown University, Evangelos Lamprou Brown University, USA | ||
09:00 - 10:30 | |||
09:00 5mDay opening | Welcome PEPM | ||
09:05 30mResearch paper | Hole Refinements for Polymorphic Type-and-Example Driven Synthesis PEPM Niek Mulleners Utrecht University, Johan Jeuring Utrecht University, Wouter Swierstra Utrecht University, Netherlands DOI | ||
09:35 30mResearch paper | Inferring Typing Rules for Contextual Sugars PEPM Tailai Yu Peking University, Zhichao Guan Peking University, Di Wang Peking University, Zhenjiang Hu Peking University DOI | ||
10:05 15mShort-paper | S4 modal sequent calculus as intermediate logic and intermediate language (Short Paper) PEPM File Attached | ||
10:20 15mShort-paper | Epistemic Logic for Polyglots (Short Paper) PEPM File Attached | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Opening PLMW @ POPL Andrew K. Hirsch University at Buffalo, SUNY, Yannick Forster INRIA, Jenna DiVincenzo (Wise) Purdue University | ||
09:10 10mTalk | SIGPLAN CARES Introduction PLMW @ POPL Stephanie Weirich University of Pennsylvania | ||
09:20 20mTalk | The Art of Living Abroad (and Finding a Good Baguette in New York) PLMW @ POPL Alexandre Moine New York University | ||
09:40 50mOther | Icebreaker PLMW @ POPL | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break POPL Catering | ||
11:00 - 12:30 | |||
11:00 30mTalk | Multi-variable Quantification of BDDs in External Memory using Nested Sweeping VMCAI | ||
11:30 30mTalk | Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver VMCAI Bruno Andreotti Universidade Federal de Minas Gerais, Haniel Barbosa Universidade Federal de Minas Gerais | ||
12:00 30mTalk | SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation VMCAI Junjie Meng School of Computer Science and Technology, Tongji University, Jie An Institute of Software Chinese Academy of Sciences, Yong Li Institute of Software, Chinese Academy of Sciences, Andrea Turrini Institute of Software, Chinese Academy of Sciences, Miaomiao Zhang School of Computer Science and Technology, Tongji University | ||
11:00 - 12:30 | |||
11:00 30mTalk | A Functional Logic Perspective on Indentation-Sensitive Parsing (Short Paper) PADL Steven Libby University of Portland | ||
11:30 30mTalk | A One-Pass CPS Transform with Simulation on the Nose PADL Pascal Y. Lasnier , Jeremy Yallop University of Cambridge, Magnus O. Myreen Chalmers University of Technology | ||
12:00 30mTalk | Determinacy Checking for Elpi: an Higher-Order Logic Programming Language with Cut PADL | ||
11:00 - 12:30 | |||
11:00 30mTalk | On building a successful research group RTFM Stephanie Weirich University of Pennsylvania | ||
11:30 60mPanel | Panel: Promotion and tenure RTFM P: Amal Ahmed Northeastern University, USA, P: Lars Birkedal Aarhus University, P: Ilya Sergey National University of Singapore, P: Nicolas Wu Imperial College London, P: Steve Zdancewic University of Pennsylvania, M: Derek Dreyer MPI-SWS | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Analyzing Shell Scripts Tutorials Michael Greenberg Stevens Institute of Technology, Konstantinos Kallas University of California, Los Angeles, Nikos Vasilakis Brown University, Evangelos Lamprou Brown University, USA | ||
11:00 - 12:30 | |||
11:00 30mResearch paper | Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations PEPM DOI | ||
11:30 30mResearch paper | Towards Lightweight and Efficient Choreographic Cloud Services PEPM Alex Ionescu Chalmers University of Technology; University of Gothenburg, Alejandro Russo Chalmers University of Technology; University of Gothenburg DOI | ||
12:00 15mShort-paper | Incrementalizing Haskell implementation of Putback-based Bidirectional Transformation Language BiGUL (Short Paper) PEPM File Attached | ||
12:15 15mTalk | Partial Evaluation as a primitive in modern network troubleshooting (Talk Proposal) PEPM Anduo Wang Temple University, USA | ||
11:00 - 12:30 | |||
11:00 45mPanel | PLMW Panel PLMW @ POPL Alexandre Moine New York University, Simon Spies Jane Street, Umang Mathur National University of Singapore, Jennifer Paykin University of Vermont, Stephen Mell | ||
11:45 45mTalk | Weak Accept, or: How I Learned to Write Papers and Deal with Reviews PLMW @ POPL Alex Kavvos University of Bristol | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch POPL Catering | ||
14:00 - 15:30 | |||
14:00 22mTalk | Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis CPP | ||
14:22 22mTalk | Enhancing Symbolic Execution with Machine-Checked Safety Proofs CPP Pre-print | ||
14:45 22mTalk | Layers of Confluence for Actors CPP Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Einar Broch Johnsen University of Oslo, Åsmund Aqissiaq Arild Kløvstad University of Oslo (UiO), Violet Ka I Pun Western Norway University of Applied Sciences, Yannick Zakowski Inria | ||
15:07 22mTalk | Towards composable proofs of cache coherence protocols CPP | ||
14:00 - 15:30 | |||
14:00 30mTalk | Atomic Gliders and Cellular Automata as Language Generators VMCAI Dana Fisman Ben-Gurion University, Noa Izsak CISPA Helmholtz Center for Information Security, Germany | ||
14:30 30mTalk | Reachability in multi-agent transfer systems VMCAI Nathalie Bertrand INRIA Rennes, Loic Helouet INRIA, Engel Lefaucheux Université de Lorraine; CNRS; Inria; LORIA, Luca Paparazzo Inria, IRISA, Université de Rennes | ||
15:00 30mTalk | A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamical Models VMCAI Rui Guo Zhejiang Sci-Tech University, Yang Li Zhejiang Sci-Tech University, Xiuqing Cao Zhejiang Sci-Tech University, Wang Lin | ||
14:00 - 15:30 | |||
14:00 40mTalk | On grant writing RTFM Suresh Jagannathan Purdue University | ||
14:40 50mPanel | Panel: Visibility and Impact RTFM P: Derek Dreyer MPI-SWS, P: Xavier Leroy Collège de France - PSL University, P: Nikhil Swamy Microsoft Research, P: Stephanie Weirich University of Pennsylvania, M: Ilya Sergey National University of Singapore | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Is Program Synthesis Soluble in Large Language Models? Tutorials Nathanaël Fijalkow CNRS, LaBRI, University of Bordeaux | ||
14:00 - 15:30 | |||
14:00 90mKeynote | Revisiting the Evolution of Effects (Invited Talk)Keynote PEPM Nicolas Wu Imperial College London DOI | ||
14:00 - 15:30 | |||
14:00 45mTalk | An Invitation to Quantum Programming Languages PLMW @ POPL Robert Rand University of Chicago | ||
14:45 45mTalk | Industry Panel PLMW @ POPL Nathanaëlle Courant OCamlPro, Chris Casinghino Jane Street, Kiran Gopinathan University College London, Satnam Singh Harmonic | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break POPL Catering | ||
16:00 - 17:30 | |||
16:00 22mTalk | A Recipe for Modular Verification of Generic Tree Traversals CPP Laila Elbeheiry MPI-SWS, Michael Sammler Institute of Science and Technology Austria, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS | ||
16:22 22mTalk | Precise Reasoning about Container-Internal Pointers with Logical Pinningdistinguished paper CPP DOI Pre-print | ||
16:45 22mTalk | Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic CPP Virgil Marionneau ENS Rennes, Félix Sassus-Bourda ENS Paris Saclay, Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University | ||
17:07 22mTalk | Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust CPP Arnaud Golfouse Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France, Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Jacques-Henri Jourdan LMF, CNRS, Université Paris-Saclay | ||
16:00 - 17:30 | Quantum and Probabilistic VerificationVMCAI at Horizons Chair(s): Jyun-Ao Lin National Taipei University of Technology | ||
16:00 30mTalk | Efficiently Verifying Quantum Programs with Few T Gates VMCAI | ||
16:30 30mTalk | Finding Photonics Circuits via δ-weakening SMT VMCAI | ||
17:00 30mTalk | Probabilistic Verification for Modular Network-on-Chip Systems VMCAI Nick Waddoups nick.waddoups@usu.edu, Jonah Boe Hill Air Force Base, Utah, Arnd Hartmanns University of Twente, Prabal Basu Utah State University, Sanghamitra Roy Utah State University, Koushik Chakraborty Utah State University, Zhen Zhang Utah State University | ||
16:00 - 17:30 | |||
16:00 60mPanel | Panel: Work-life balance, service, and teaching RTFM P: Sebastian Erdweg KIT, P: Robbert Krebbers Radboud University Nijmegen, P: Azalea Raad Imperial College London, P: Sharon Shoham Tel Aviv University, M: Amal Ahmed Northeastern University, USA | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Is Program Synthesis Soluble in Large Language Models? Tutorials Nathanaël Fijalkow CNRS, LaBRI, University of Bordeaux | ||
16:00 - 17:30 | |||
16:00 30mResearch paper | Staging Effect Handlers for Modular Search PEPM DOI | ||
16:30 15mTalk | Holey: Staged Execution from Python to SMT (Talk Proposal) PEPM Nada Amin Harvard University | ||
16:45 15mShort-paper | Towards Cumulative Abstract Semantics via Handlers (Short Paper) PEPM Cade Lueker University of Colorado Boulder, Andrew Fox University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon File Attached | ||
17:00 15mShort-paper | Retargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper) PEPM Jay Lee Seoul National University, Joongwon Ahn Seoul National University, Kwangkeun Yi Seoul National University File Attached | ||
17:15 10mDay closing | Closing PEPM | ||
16:00 - 17:30 | |||
16:00 45mTalk | How to Write a Paper PLMW @ POPL Nate Foster Cornell University; Jane Street | ||
16:45 45mTalk | Effects and Call-by-Push-Value PLMW @ POPL Paul Blain Levy University of Birmingham | ||
17:30 - 21:30 | |||
17:30 4hSocial Event | Jane Street Game Night POPL Chris Casinghino Jane Street | ||
Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
08:50 - 09:00 | |||
08:50 10mDay opening | Welcome from the general chair POPL | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Medium-scale automation for proof assistants POPL Damien Pous CNRS | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Medium-scale automation for proof assistants POPL Damien Pous CNRS | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Medium-scale automation for proof assistants POPL Damien Pous CNRS | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break POPL Catering | ||
10:30 - 12:10 | Program AnalysisPOPL at Dortoirs Chair(s): Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University | ||
10:30 25mTalk | A Modular Static Cost Analysis for GPU Warp-Level Parallelism POPL Gregory Blike University of Massachusetts at Boston, Hannah Zicarelli University of Massachusetts at Boston, Udaya Sathiyamoorthy University of Massachusetts at Boston, Julien Lange Royal Holloway University of London, Tiago Cogumbreiro University of Massachusetts at Boston DOI | ||
10:55 25mTalk | ChiSA: Static Analysis for Lightweight Chisel Verification POPL Jiacai Cui Nanjing University, Qinlin Chen Nanjing University, Zhongsheng Zhan Nanjing University, Tian Tan Nanjing University, Yue Li Nanjing University DOI | ||
11:20 25mTalk | Miri: Practical Undefined Behavior Detection for Rust POPL Ralf Jung ETH Zurich, Benjamin Kimock Lansweeper NV, Christian Poveda Unaffiliated, Eduardo Sánchez Muñoz Unaffiliated, Oli Scherer Unaffiliated, Qian (Andy) Wang ETH Zurich and Imperial College London DOI | ||
11:45 25mTalk | Piecewise Analysis of Probabilistic Programs via k-Induction POPL Tengshun Yang Institute of Software at Chinese Academy of Sciences, Shenghua Feng Institute of Software at Chinese Academy of Sciences, Hongfei Fu Shanghai Jiao Tong University, Naijun Zhan Peking University; Zhongguancun Lab, Jingyu Ke Shanghai Jiao Tong University, Shiyang Wu Shanghai Jiao Tong University DOI | ||
10:30 - 12:10 | |||
10:30 25mTalk | Domain-Theoretic Semantics for Functional Logic Programming POPL Eddie Jones University of Bristol, Samson Main University of Bristol, Celia Mengyue Li University of Bristol, Jonathan Marriott University of Bristol, Alex Kavvos University of Bristol DOI | ||
10:55 25mTalk | Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks POPL Michael Lee University of Cambridge, UK, Ningning Xie University of Toronto, Oleg Kiselyov Tohoku University, Jeremy Yallop University of Cambridge DOI | ||
11:20 25mTalk | Hyperfunctions: Communicating Continuations POPL DOI Pre-print | ||
11:45 25mTalk | Lazy Linearity for a Core Functional Language POPL DOI Pre-print | ||
12:15 - 14:00 | |||
12:15 1h45mLunch | Lunch POPL Catering | ||
12:15 - 14:00 | |||
12:15 1h45mLunch | Mentoring Lunch POPL Catering | ||
12:15 - 14:00 | |||
12:15 1h45mMeeting | PLMW Steering Committee Meeting PLMW @ POPL | ||
14:00 - 15:40 | Quantum 1POPL at Dortoirs Chair(s): Ugo Dal Lago University of Bologna; Centre Inria d’Université Côte d’Azur | ||
14:00 25mTalk | An Expressive Assertion Language for Quantum Programs POPL Bonan Su Tsinghua University, Yuan Feng Tsinghua University, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University, Li Zhou Institute of Software at Chinese Academy of Sciences DOI | ||
14:25 25mTalk | Hadamard-Pi: Equational Quantum Programming POPL Wang Fang University of Edinburgh, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark DOI | ||
14:50 25mTalk | Qudit Quantum Programming with Projective Cliffords POPL DOI | ||
15:15 25mTalk | RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing POPL Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University, Emanuele D'Osualdo University of Konstanz DOI Pre-print | ||
14:00 - 15:40 | |||
14:00 25mTalk | Extensible Data Types with Ad-Hoc Polymorphism POPL Matthew Toohey University of Toronto, Yanning Chen University of Toronto, Ara Jamalzadeh University of Toronto, Ningning Xie University of Toronto DOI Pre-print | ||
14:25 25mTalk | Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems POPL Joseph Zullo Purdue University DOI | ||
14:50 25mTalk | Local Contextual Type Inference POPL Xu Xue University of Hong Kong, Chen Cui University of Hong Kong, Shengyi Jiang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
15:15 25mTalk | Typing Strictness POPL Daniel Sainati University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Stephanie Weirich University of Pennsylvania DOI | ||
15:40 - 16:10 | |||
15:40 30mCoffee break | Break POPL Catering | ||
16:10 - 17:25 | |||
16:10 25mTalk | Characterizing Sets of Theories That Can Be Disjointly Combined POPL DOI | ||
16:35 25mTalk | Context-Free-Language Reachability for Almost-Commuting Transition Systems POPL Nikhil Pimpalkhare Princeton University, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison DOI | ||
17:00 25mTalk | Determination Problems for Orbit Closures and Matrix Groups POPL Rida Ait El Manssour University of Oxford, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS, Anton Varonka TU Wien, James Worrell University of Oxford DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages POPL Zhentao Ye Peking University, Ruyi Ji Peking University, Yingfei Xiong Peking University, Xin Zhang Peking University DOI | ||
16:35 25mTalk | Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling POPL Doyoon Lee Seoul National University, Woosuk Lee Hanyang University, Kwangkeun Yi Seoul National University DOI | ||
17:00 25mTalk | Oriented Metrics for Bottom-Up Enumerative Synthesis POPL DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models POPL Shaan Nagy University of California at San Diego, Timothy Zhou University of California, San Diego, Nadia Polikarpova University of California at San Diego, Loris D'Antoni University of California at San Diego DOI | ||
16:35 25mTalk | Compiling to Linear Neurons POPL Joey Velez-Ginorio University of Pennsylvania, Nada Amin Harvard University, Konrad Kording University of Pennsylvania, Steve Zdancewic University of Pennsylvania DOI | ||
17:00 25mTalk | Fuzzing Guided by Bayesian Program Analysis POPL DOI Pre-print | ||
17:30 - 19:30 | |||
17:30 2hSocial Event | POPL networking reception POPL | ||
19:30 - 22:00 | |||
19:30 2h30mDinner | Women @ POPL Dinner POPL | ||
Thu 15 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:00 | |||
09:00 60mSocial Event | Tour of the Historic City Center POPL | ||
09:30 - 09:50 | |||
09:30 20mSocial Event | Jacobins Convent and its History POPL | ||
09:50 - 10:20 | |||
09:50 30mCoffee break | Break POPL Catering | ||
10:20 - 12:00 | |||
10:20 - 12:00 | Concurrency: Testing and VerificationPOPL at Nef Chair(s): Ramanathan S. Thinniyam Uppsala University | ||
10:20 25mTalk | (TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection POPL DOI | ||
10:45 25mTalk | Verifying Almost-Sure Termination for Randomized Distributed Algorithms POPL Constantin Enea LIX, CNRS, Ecole Polytechnique, Rupak Majumdar MPI-SWS, Harshit Jitendra Motwani MPI-SWS, V.R. Sathiyanarayana MPI-SWS DOI | ||
11:10 25mTalk | Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic POPL DOI | ||
11:35 25mTalk | The Complexity of Testing Message-Passing Concurrency POPL Zheng Shi National University of Singapore, Lasse Møldrup Aarhus University, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University DOI Pre-print | ||
10:20 - 12:00 | |||
10:20 25mTalk | A Relational Separation Logic for Effect Handlers POPL Paulo Emílio de Vilhena Imperial College London, Simcha van Collem Radboud University Nijmegen, Ines Wright Aarhus University, Robbert Krebbers Radboud University Nijmegen DOI | ||
10:45 25mTalk | Bayesian Separation Logic POPL Shing Hin Ho Imperial College London, Nicolas Wu Imperial College London, Azalea Raad Imperial College London DOI Pre-print | ||
11:10 25mTalk | Cryptis: Cryptographic Reasoning in Separation Logic POPL Arthur Azevedo de Amorim Rochester Institute of Technology, Amal Ahmed Northeastern University, USA, Marco Gaboardi Boston University DOI | ||
11:35 25mTalk | Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions POPL Neta Elad Tel Aviv University, Adithya Murali University of Wisconsin, Sharon Shoham Tel Aviv University DOI | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break POPL Catering | ||
12:00 - 14:00 | |||
12:00 2hLunch | Lunch POPL Catering | ||
12:00 - 14:00 | |||
12:00 2hMeeting | POPL steering committee meeting POPL | ||
12:30 - 14:00 | |||
12:30 90mLunch | LGBTQ+ Lunch POPL Catering | ||
14:00 - 15:40 | |||
14:00 25mTalk | Classical Notions of Computation and the Hasegawa-Thielecke Theorem POPL Éléonore Mangel Univ. Paris Cité - CNRS - Inria, Paul-André Melliès Univ. Paris Cité - CNRS - Inria, Guillaume Munch-Maccagnoni INRIA DOI | ||
14:25 25mTalk | From Semantics to Syntax: A Type Theory for Comprehension Categories POPL Niyousha Najmaei École Polytechnique, Niels van der Weide Radboud University, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University DOI | ||
14:50 25mTalk | Higher-Order Behavioural Conformances via Fibrations POPL Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg DOI | ||
15:15 25mTalk | What Is a Monoid? POPL DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | A Lazy, Concurrent Convertibility Checker POPL DOI | ||
14:25 25mTalk | Canonicity for Indexed Inductive-Recursive Types POPL András Kovács University of Gothenburg and Chalmers University of Technology DOI | ||
14:50 25mTalk | Coco: Corecursion with Compositional Heterogeneous Productivity POPL Jaewoo Kim Seoul National University, Yeonwoo Nam Seoul National University, Chung-Kil Hur Seoul National University DOI | ||
15:15 25mTalk | Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation POPL Marcus Rossel Barkhausen Institut; TU Darmstadt, Rudi Schneider TU Berlin, Thomas Koehler ICube Lab - CNRS - Université de Strasbourg, Michel Steuwer TU Berlin, Andrés Goens TU Darmstadt DOI Pre-print | ||
14:00 - 15:40 | |||
14:00 25mTalk | A Logic for the Imprecision of Abstract Interpretations POPL Marco Campion Inria Paris - ENS - Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona, Caterina Urban Inria Paris - ENS - Université PSL DOI | ||
14:25 25mTalk | Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment POPL David M. Kahn Denison University, Jan Hoffmann Carnegie Mellon University, Runming Li Carnegie Mellon University DOI | ||
14:50 25mTalk | JAX Autodiff from a Linear Logic Perspective POPL DOI | ||
15:15 25mTalk | U-Turn: Enhancing Incorrectness Analysis by Reversing Direction POPL Flavio Ascari University of Konstanz, Roberto Bruni University of Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy, Azalea Raad Imperial College London DOI | ||
15:40 - 16:10 | |||
15:40 30mCoffee break | Break POPL Catering | ||
16:10 - 17:00 | |||
16:10 25mTalk | Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers POPL Xuanyu Peng University of California at San Diego, Dominic Kennedy University of Utah, Yuyou Fan University of Utah, Ben Greenman University of Utah, USA, John Regehr University of Utah, Loris D'Antoni University of California at San Diego DOI | ||
16:35 25mTalk | Parameterized Infinite-State Reactive Synthesis POPL DOI | ||
16:10 - 17:00 | |||
16:10 25mTalk | A Family of Sims with Diverging Interests POPL Nicolas Chappe CNRS - Verimag DOI | ||
16:35 25mTalk | Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation POPL Niklas Mück MPI-SWS, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Michael Sammler Institute of Science and Technology Austria DOI Pre-print | ||
16:10 - 17:00 | |||
16:10 25mTalk | Dependent Coeffects for Local Sensitivity Analysis POPL Victor Sannier Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL, Patrick Baillot Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL DOI | ||
16:35 25mTalk | Security Reasoning via Substructural Dependency TrackingDistinguished Paper POPL Hemant Gouni Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA, Jonathan Aldrich Carnegie Mellon University DOI Pre-print | ||
17:00 - 18:30 | |||
17:00 90mMeeting | PC Chair's Report and Business Meeting POPL | ||
19:30 - 22:00 | |||
19:30 2h30mDinner | POPL PC and SC dinner POPL | ||
Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:00 | |||
09:00 60mKeynote | Hardware-Software Contracts for High Assurance with Applications to Side-Channel Security POPL Caroline Trippel Stanford University | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break POPL Catering | ||
10:30 - 12:10 | Specification and Verification MethodsPOPL at Dortoirs Chair(s): Ben Greenman University of Utah, USA | ||
10:30 25mTalk | Abstraction Functions as Types POPL Harrison Grodin Carnegie Mellon University, Runming Li Carnegie Mellon University, Robert Harper Carnegie Mellon University DOI | ||
10:55 25mTalk | Foundational Multi-Modal Program Verifiers POPL Vladimir Gladshtein , George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore, Vitaly Kurin Neapolis University Pafos, Ilya Sergey National University of Singapore DOI | ||
11:20 25mTalk | Stateful Differential Operators for Incremental Computing POPL DOI | ||
11:45 25mTalk | The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs POPL Frank Schüssele University of Freiburg, Matthias Zumkeller University of Freiburg, Miriam Lagunes-Rochin University of Freiburg, Dominik Klumpp LIX - CNRS - École Polytechnique; University of Freiburg DOI | ||
10:30 - 12:10 | |||
10:30 25mTalk | Di- is for Directed: First-Order Directed Type Theory via Dinaturality POPL Andrea Laretto Tallinn University of Technology, Fosco Loregian Tallinn University of Technology, Niccolò Veltri IT University of Copenhagen DOI | ||
10:55 25mTalk | Quotient PolymorphismDistinguished Paper POPL DOI | ||
11:20 25mTalk | The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types POPL Chun Yin Chau HKUST (The Hong Kong University of Science and Technology), Lionel Parreaux Hong Kong University of Science and Technology DOI | ||
11:45 25mTalk | Welterweight Go: Boxing, Structural Subtyping, and Generics POPL Raymond Hu Queen Mary University of London, Julien Lange Royal Holloway University of London, Bernardo Toninho Instituto Superior Técnico - University of Lisbon, Philip Wadler University of Edinburgh, Robert Griesemer Google, Keith Randall Google DOI | ||
12:15 - 14:00 | |||
12:15 1h45mLunch | Lunch POPL Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | URM Lunch POPL Catering | ||
14:00 - 15:40 | Monads and EffectsPOPL at Dortoirs Chair(s): Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg | ||
14:00 25mTalk | An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic TheoriesDistinguished Paper POPL Ohad Kammar University of Edinburgh, Jack Liell-Cock University of Oxford, Sam Lindley University of Edinburgh, Cristina Matache University of Edinburgh, Sam Staton University of Oxford DOI | ||
14:25 25mTalk | Handling Higher-Order Effectful Operations with Judgemental Monadic Laws POPL DOI | ||
14:50 25mTalk | Rows and Capabilities as Modal Effects POPL DOI | ||
15:15 25mTalk | The Relative Monadic Metalanguage POPL Jack Liell-Cock University of Oxford, Zev Shirazi University of Oxford, Sam Staton University of Oxford DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | AdapTT: Functoriality for Dependent Type Casts POPL Arthur Adjedj ENS Paris Saclay, Université Paris-Saclay, Meven Lennon-Bertrand Inria – Université Paris Cité, Thibaut Benjamin Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Kenji Maillard Inria DOI | ||
14:25 25mTalk | Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach POPL DOI | ||
14:50 25mTalk | Encode the Cake and Eat It Too: Controlling Computation in Type Theory, LocallyDistinguished Paper POPL DOI | ||
15:15 25mTalk | Normalisation for First-Class Universe LevelsDistinguished PaperRemote POPL Nils Anders Danielsson University of Gothenburg, Naïm Camille Favier Chalmers University of Technology and University of Gothenburg, Ondřej Kubánek Chalmers University of Technology DOI | ||
15:40 - 16:10 | |||
15:40 30mCoffee break | Break POPL Catering | ||
16:10 - 17:25 | |||
16:10 25mTalk | A Complementary Approach to Incorrectness Typing POPL Celia Mengyue Li University of Bristol, Sophie Pull University of Bristol, Steven Ramsay University of Bristol DOI | ||
16:35 25mTalk | A Synthetic Reconstruction of Multiparty Session Types POPL David Castro-Perez University of Kent, Francisco Ferreira Royal Holloway, University of London, Sung-Shik Jongmans University of Groningen DOI | ||
17:00 25mTalk | Bounded Sort Polymorphism with Elimination Constraints POPL Johann Rosain ENS Lyon, Tomás Diaz University of Chile, Kenji Maillard Inria, Matthieu Sozeau Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile, Théo Winterhalter INRIA DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Counting and Sampling Traces in Regular Languages POPL Alexis de Colnet TU Wien, Kuldeep S. Meel University of Toronto, Umang Mathur National University of Singapore DOI Pre-print | ||
16:35 25mTalk | Parametrised Verification of Intel-x86 Programs POPL Parosh Aziz Abdulla Uppsala University; Mälardalen University, Mohamed Faouzi Atig Uppsala University, Ahmed Bouajjani Université Paris Cité, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan Institute of Mathematical Sciences DOI | ||
17:00 25mTalk | General Decidability Results for Systems with Continuous Counters POPL A. R. Balasubramanian Technical University of Munich, Matthew Hague Royal Holloway University of London, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Generating Compilers for Qubit Mapping and Routing POPL Abtin Molavi University of Wisconsin-Madison, Amanda Xu University of Wisconsin-Madison, Ethan Cecchetti University of Wisconsin-Madison, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison DOI | ||
16:35 25mTalk | On Circuit Description Languages, Indexed Monads, and Resource Analysis POPL Ken Sakayori University of Tokyo, Andrea Colledan University of Bologna; Centre Inria d’Université Côte d’Azur, Ugo Dal Lago University of Bologna; Centre Inria d’Université Côte d’Azur DOI | ||
17:00 25mTalk | Quantum Circuits Are Just a Phase POPL Chris Heunen University of Edinburgh, Louis Lemonnier University of Edinburgh, Christopher McNally Massachusetts Institute of Technology, Alex Rice University of Edinburgh DOI | ||
Sat 17 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 60mKeynote | Lean4Lean: Mechanizing the Metatheory of Lean WITS Mario Carneiro Chalmers University of Technology | ||
10:00 22mTalk | Observing Definitional Equality WITS András Kovács University of Gothenburg and Chalmers University of Technology | ||
09:00 - 10:30 | |||
09:00 45mKeynote | Future-Proofing Numerical Accuracy with Formal Specifications RocqPL Ariel E. Kellison Cornell University | ||
09:45 15mTalk | Crane Lowers Rocq Safely into C++ RocqPL Pre-print File Attached | ||
10:00 15mTalk | Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic RocqPL | ||
10:15 15mTalk | The HOL-Light library of Multivariate real analysis in Rocq RocqPL | ||
09:00 - 10:30 | |||
09:10 10mTalk | Opening GiacoFest | ||
09:20 70mTalk | Keynote Speech GiacoFest | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break POPL Catering | ||
11:00 - 12:30 | |||
11:00 22mTalk | Decoupling Resolution from Type Inference WITS Lionel Parreaux Hong Kong University of Science and Technology | ||
11:22 22mTalk | First-Class Refinement Types in Scala WITS Matt Bovel EPFL | ||
11:45 22mTalk | Types as grammars WITS Gil Silva LASIGE, University of Lisbon, Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Diana Costa LASIGE, University of Lisbon, Andreia Mordido University of Lisbon, Diogo Poças Instituto de Telecomunicações, University of Lisbon, Vasco T. Vasconcelos LASIGE, University of Lisbon | ||
12:07 22mTalk | Omnidirectional type inference for ML WITS Alistair O'Brien University of Cambridge, Didier Rémy Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS | ||
11:00 - 12:30 | Rocq Developer Session and Mechanized Metatheory in RocqRocqPL at Salle 14 Chair(s): François Pottier Inria | ||
11:00 45mPanel | Session with the Rocq Development Team RocqPL | ||
11:45 15mTalk | Rocq CARVe-ing: A Library for Substructural Meta-Theory RocqPL Daniel Zackon McGill University, Ryan Kavanagh Université du Québec à Montréal, Alberto Momigliano Università degli Studi di Milano, Brigitte Pientka McGill University File Attached | ||
12:00 15mTalk | Scalable Type Inference for Intrinsically-Typed Binders RocqPL Max Kurze Barkhausen Institut, Clément Pit-Claudel EPFL, Sebastian Ertel Barkhausen Institute, Dresden | ||
12:15 15mTalk | Sulfur: Substitution Generation using a Logical Framework RocqPL Mathis Bouverot-Dupuis INRIA & École Normale Supérieure, Théo Winterhalter INRIA, Kenji Maillard Inria, Kathrin Stark Heriot-Watt University File Attached | ||
11:00 - 12:30 | Short TalksGiacoFest at Salle 19 Chair(s): Marco Campion Inria Paris - ENS - Université PSL, Michele Pasqua University of Verona | ||
11:00 90mTalk | Short Talks GiacoFest | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch POPL Catering | ||
14:00 - 15:30 | |||
14:00 22mTalk | A Dependent Language with Type-Safe Program Extraction WITS Greg Brown University of Edinburgh | ||
14:22 22mTalk | Code Generation via Meta-programming in Dependently Typed Proof Assistants WITS | ||
14:45 22mTalk | Garbage Collection for Higher Inductive Types WITS | ||
15:07 22mTalk | Type Inference Techniques: Implementation and Formalization, Better Together WITS | ||
14:00 - 15:30 | |||
14:00 15mTalk | A systematic approach to "Well-founded recursion done right" RocqPL Herman Geuvers Radboud University Nijmegen, Netherlands, Gijs Pennings Eindhoven University of Technology File Attached | ||
14:15 15mTalk | Implementing parametricity in Rocq-ELPI RocqPL | ||
14:30 15mTalk | Enhancing universe polymorphism for Rocq: Algebraic universes, consistency checking and variance inference RocqPL File Attached | ||
14:45 15mTalk | Nested Inductive Types for Rocq and Lean RocqPL Thomas Lamiaux Nantes Université, Inria, Yannick Forster INRIA, Matthieu Sozeau Inria, Nicolas Tabareau Inria | ||
15:00 15mTalk | Trocq parametricity translations for inductives RocqPL Tomas Vallejos Parada Inria File Attached | ||
15:15 15mTalk | Verifying Synchronous Dataflow Programs with SMTCoq RocqPL Basile Pesin Ecole Nationale de l'Aviation Civile (ENAC) File Attached | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break POPL Catering | ||
16:00 - 18:00 | |||
16:00 40mKeynote | Verifying Dependent Type-checkers WITS Meven Lennon-Bertrand Inria – Université Paris Cité | ||
17:00 22mTalk | Type Narrowing the Hard Way WITS | ||
17:23 2mOther | Closing WITS Niki Vazou IMDEA Software Institute | ||