ICFP/SPLASH 2025 (series) /
ICFP/SPLASH 2025 Program
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
This program is tentative and subject to change.
Sun 12 OctDisplayed time zone: Perth change
Sun 12 Oct
Displayed time zone: Perth change
09:00 - 10:30 | |||
09:00 20mTalk | PLMW Welcome PLMW @ ICFP/SPLASH Lucas Bang Harvey Mudd College, Milijana Surbatovich University of Maryland, Conrad Watt Nanyang Technological University, Ningning Xie University of Toronto | ||
09:20 40mOther | Ice Breaker PLMW @ ICFP/SPLASH | ||
10:00 15mOther | SIGPLAN-M Introduction PLMW @ ICFP/SPLASH | ||
10:15 15mLive Q&A | Open Q & A PLMW @ ICFP/SPLASH | ||
09:00 - 10:30 | |||
09:00 90mTalk | WebAssembly Research Tools Tutorial Tutorials | ||
09:00 - 10:30 | |||
09:00 90mTalk | TBA TyDe Liang-Ting Chen Academia Sinica | ||
09:00 - 10:30 | |||
09:00 90mKeynote | Smart Handlers: Handling the selection monad HOPE Ningning Xie University of Toronto | ||
09:00 - 10:30 | |||
09:00 90mTalk | Testing concurrent code on JVM with Lincheck Tutorials | ||
09:00 - 10:30 | |||
09:00 90mTalk | Compiling Quantum Circuits Tutorials Amanda Xu University of Wisconsin-Madison, Abtin Molavi University of Wisconsin-Madison, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison | ||
09:00 - 10:30 | |||
09:00 15mDay opening | Welcome to Erlang’25 Erlang Kiko Fernandez-Reyes Ericsson, Sweden, Adriana Laura Voinea University of Glasgow, UK, Ákos Hajdu Meta | ||
09:15 75mKeynote | (Keynote) PyErlang -- a stepping stone towards behaviour-oriented concurrency in Python Erlang Tobias Wrigstad Uppsala University | ||
09:00 - 10:30 | |||
09:00 45mTalk | A Layered Certifying Compiler Architecture FUNARCH Jacco Krijnen Utrecht University, Wouter Swierstra Utrecht University, Netherlands, Manuel Chakravarty Tweag & IOG, Joris Dral Well-Typed, Gabriele Keller Utrecht University | ||
09:45 45mTalk | Evolution of Functional UI Paradigms FUNARCH | ||
09:00 - 10:30 | |||
09:00 90mTalk | Metaprogramming in Rhombus Tutorials Matthew Flatt University of Utah | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:30 | |||
11:00 90mTalk | How to Write Papers and Give Talks that People Can Follow PLMW @ ICFP/SPLASH Derek Dreyer MPI-SWS | ||
11:00 - 12:30 | |||
11:00 90mTalk | WebAssembly Research Tools Tutorial Tutorials | ||
11:00 - 12:30 | |||
11:00 30mTalk | Representing Data Structures with Invariants in Haskell: the cases of BST and AVL TyDe Nicolas Rodriguez Instituto de Computación, Universidad de la República, Alberto Pardo Universidad de la Republica, Uruguay, Marcos Viera University of the Republic, Uruguay | ||
11:30 30mTalk | Generating a corpus of Hazel programs from ill-typed OCaml programs (Extended Abstract) TyDe | ||
12:00 30mTalk | Constrained generation of well-typed programs (Extended Abstract) TyDe | ||
11:00 - 12:30 | |||
11:00 30mTalk | Contractions Are Abstractions - Towards Effective Memory Management in ReML HOPE Martin Elsman University of Copenhagen | ||
11:30 30mTalk | Finite functional programming via graded effects and relevance types HOPE Michael Arntzenius None | ||
11:00 - 12:30 | |||
11:00 90mTalk | Testing concurrent code on JVM with Lincheck Tutorials | ||
11:00 - 12:30 | |||
11:00 90mTalk | Compiling Quantum Circuits Tutorials Amanda Xu University of Wisconsin-Madison, Abtin Molavi University of Wisconsin-Madison, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison | ||
11:00 - 12:30 | |||
11:00 38mTalk | Mechanised Proofs of Atom Exhaustion in Erlang Erlang Arsenii Fomin Eötvös Loránd University, Péter Bereczky Eötvös Loránd University, Dániel Horpácsi Eötvös Loránd University, Gergő Lajos Turán Eötvös Loránd University | ||
11:38 37mTalk | Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang Erlang Gergő Lajos Turán Eötvös Loránd University, Arsenii Fomin Eötvös Loránd University, Péter Bereczky Eötvös Loránd University, Dániel Horpácsi Eötvös Loránd University, Simon Thompson University of Kent (UK) | ||
12:15 15mTalk | (Lightning Talk) The State of The Unions: challenges for type-checking unions and generics at WhatsApp Erlang Maxwell Heiber Meta | ||
11:00 - 12:30 | |||
11:00 45mTalk | Six Years of FUNAR: Functional Training for Software Architects FUNARCH Michael Sperber Active Group GmbH | ||
11:45 45mTalk | Lightning Talks #1 FUNARCH | ||
11:00 - 12:30 | |||
11:00 90mTalk | Metaprogramming in Rhombus Tutorials Matthew Flatt University of Utah | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 40mPanel | Career Panel PLMW @ ICFP/SPLASH | ||
14:45 45mTalk | Research Talk PLMW @ ICFP/SPLASH Philippa Gardner Imperial College London | ||
14:00 - 15:30 | |||
14:00 90mTalk | A guided tour through Oxidized OCaml Tutorials Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Richard A. Eisenberg Jane Street, Chris Casinghino Jane Street | ||
14:00 - 15:30 | |||
14:00 30mTalk | Gradual Metaprogramming TyDe Tianyu Chen Indiana University, Darshal Shetty Indiana University, Jeremy G. Siek Indiana University, USA, Chao-Hong Chen Indiana University, Weixi Ma Meta, Arnaud Venet Meta, Rocky Liu Meta Link to publication DOI Pre-print | ||
14:30 30mTalk | The conatural numbers form an exponential commutative semiring TyDe Pre-print | ||
15:00 30mTalk | Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search TyDe Satoshi Takimoto Institute of Science Tokyo, Sosuke Moriguchi Institute of Science Tokyo, Takuo Watanabe Institute of Science Tokyo | ||
14:00 - 15:30 | |||
14:00 30mTalk | Compositions for Free: Reasoning about Effectful Lenses HOPE | ||
14:30 30mTalk | Sound and Complete Refinement for SSA with Substructural Effects HOPE | ||
15:00 30mTalk | Substructural Weakest Preconditions in Fibrations HOPE John Li Northeastern University, Pedro H. Azevedo de Amorim University of Oxford, Ryan Doenges Northeastern University | ||
14:00 - 15:30 | |||
14:00 90mTalk | Concurrent Algorithms under the hood of Kotlin Coroutines Tutorials Nikita Koval JetBrains | ||
14:00 - 15:30 | |||
14:00 90mTalk | End-to-End Compiler Infrastructure for Emerging Tensor Accelerators Tutorials Devansh Jain University of Illinois at Urbana-Champaign, Akash Pardeshi University of Illinois at Urbana-Champaign, Marco Frigo University of Illinois at Urbana-Champaign, Kaustubh Khulbe University of Illinois at Urbana-Champaign, Charith Mendis University of Illinois at Urbana-Champaign | ||
14:00 - 15:30 | |||
14:00 38mTalk | A stop-the-world debugger for Erlang (and the BEAM) Erlang | ||
14:38 37mTalk | Evaluating AtomVM for fault-tolerant systems Erlang Daniel Ferenczi Eötvös Loránd University, Gergely Ruda evosoft Hungary Kft., Melinda Tóth Eötvös Loránd University | ||
15:15 15mTalk | (Lightning Talk) Mailboxer: Static Detection of Erlang Communication Errors Erlang Adriana Laura Voinea University of Glasgow, UK | ||
14:00 - 15:30 | |||
14:00 90mTalk | How to secure a distributed database such as OpenRiak with open-source tools Tutorials | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | |||
16:00 45mPanel | Graduate Student Panel PLMW @ ICFP/SPLASH | ||
16:45 30mTalk | How to Get the Most Out of a Conference PLMW @ ICFP/SPLASH Paulette Koronkevich University of British Columbia | ||
17:15 15mOther | Closing Remarks PLMW @ ICFP/SPLASH | ||
16:00 - 17:30 | |||
16:00 90mTalk | A guided tour through Oxidized OCaml Tutorials Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Richard A. Eisenberg Jane Street, Chris Casinghino Jane Street | ||
16:00 - 17:30 | |||
16:00 30mTalk | A Formalization of Opaque Definitions for a Dependent Type Theory TyDe Nils Anders Danielsson University of Gothenburg, Eve Geng Chalmers University of Technology, Gothenburg, Sweden | ||
16:30 30mTalk | Towards a Performance Comparison of Syntax and Type-Directed NbE (Extended Abstract) TyDe | ||
17:00 30mTalk | Type-Driven Prompt Programming: From Typed Interfaces to a Calculus of Constraints (Extended Abstract) TyDe Abhijit Paul Samsung R&D Institute, Bangladesh | ||
16:00 - 17:30 | |||
16:00 60mTalk | Rows and Capabilities as Modal Effects (Extended Abstract) HOPE | ||
16:00 - 17:30 | |||
16:00 90mTalk | Concurrent Algorithms under the hood of Kotlin Coroutines Tutorials Nikita Koval JetBrains | ||
16:00 - 17:30 | |||
16:00 90mTalk | End-to-End Compiler Infrastructure for Emerging Tensor Accelerators Tutorials Devansh Jain University of Illinois at Urbana-Champaign, Akash Pardeshi University of Illinois at Urbana-Champaign, Marco Frigo University of Illinois at Urbana-Champaign, Kaustubh Khulbe University of Illinois at Urbana-Champaign, Charith Mendis University of Illinois at Urbana-Champaign | ||
16:00 - 17:30 | |||
16:00 38mTalk | Moving Objects and Behavior Safely in Ad hoc Networks Erlang Juan Camilo Bonet Universidad de los Andes, Mateo Sanabria Universidad de los Andes, Nicolás Cardozo Universidad de los Andes | ||
16:38 15mTalk | (Lightning talk) DDMon: a Monitoring Tool for Distributed Deadlock Detection Erlang Radosław Jan Rowicki Technical University of Denmark | ||
16:53 15mTalk | (Lightning Talk) TBD Erlang | ||
17:15 15mDay closing | Closing Remarks Erlang Ákos Hajdu Meta, Kiko Fernandez-Reyes Ericsson, Sweden, Adriana Laura Voinea University of Glasgow, UK | ||
16:00 - 17:30 | |||
16:00 90mTalk | How to secure a distributed database such as OpenRiak with open-source tools Tutorials | ||
19:00 - 21:00 | |||
19:00 2hSocial Event | Concert: Mitosis SPLASH FARM Kerry Hagan University of Illinois, Urbana-Champaign | ||
19:00 2hSocial Event | Concert: The River Oycus SPLASH FARM | ||
19:00 2hSocial Event | Concert: False Awakening on a Mediterranean Island SPLASH FARM | ||
19:00 2hSocial Event | Concert: RocqNRoll SPLASH FARM | ||
19:00 2hSocial Event | Concert: Girard’s Paradox SPLASH FARM | ||
19:00 2hSocial Event | Concert: Mirages SPLASH FARM | ||
Mon 13 OctDisplayed time zone: Perth change
Mon 13 Oct
Displayed time zone: Perth change
09:00 - 10:10 | |||
09:00 5mTalk | JFP Announcement ICFP Papers Derek Dreyer MPI-SWS | ||
09:05 65mKeynote | Functional Programming for Hardware Design ICFP Keynotes Satnam Singh Independent | ||
10:10 - 10:50 | |||
10:10 40mCoffee break | Break Catering | ||
10:50 - 12:05 | |||
10:50 10mDay opening | Opening SAS | ||
11:05 60mKeynote | On a simple problem due to Yves Bertot SAS Olivier Danvy Yale-NUS College and School of Computing, Singapore | ||
10:50 - 12:05 | |||
10:50 25mTalk | 2-Functoriality of Initial Semantics, and Applications ICFP Papers Benedikt Ahrens Delft University of Technology, Ambroise Lafont Inria, France, Thomas Lamiaux University of Paris-Saclay, Ens Paris-Saclay DOI | ||
11:15 25mTalk | Bialgebraic Reasoning on Stateful Languages ICFP Papers Sergey Goncharov University of Birmingham, Stefan Milius Friedrich-Alexander University Erlangen-Nürnberg, Lutz Schröder Friedrich-Alexander University Erlangen-Nürnberg, Stelios Tsampas University of Southern Denmark, Henning Urbat Friedrich-Alexander University Erlangen-Nürnberg DOI | ||
11:40 25mTalk | Frex: Dependently Typed Algebraic Simplification ICFP Papers Guillaume Allais University of Strathclyde, Edwin Brady University of St. Andrews, Nathan Corbyn University of Oxford, Ohad Kammar University of Edinburgh, Jeremy Yallop University of Cambridge DOI Pre-print | ||
10:50 - 12:05 | |||
10:50 25mTalk | Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages ICFP Papers J. Carr University of Chicago, Benjamin Quiring University of Maryland at College Park, John Reppy University of Chicago, Olin Shivers Northeastern University, Skye Soss University of Chicago, Byron Zhong University of Chicago DOI | ||
11:15 25mTalk | Multiple Resumptions and Local Mutable State, Directly ICFP Papers Serkan Muhcu Technische Universität Berlin, Philipp Schuster University of Tübingen, Michel Steuwer Technische Universität Berlin, Jonathan Immanuel Brachthäuser University of Tübingen DOI | ||
11:40 25mPaper | OCaml Blockly ICFP JFP First Papers Kenichi Asai Ochanomizu University DOI | ||
10:50 - 12:05 | MorningThe Scala Workshop at Peony West Chair(s): Oliver Bračevac EPFL, LAMP, Hamza Remmal EPFL, LAMP | ||
10:50 10mDay opening | Welcome to Scala'25 The Scala Workshop | ||
11:00 45mKeynote | Simpler Scala Builds with Functional and Object-Oriented Programming The Scala Workshop | ||
11:45 20mTalk | Taking away Mutation The Scala Workshop Edward Lee University of Waterloo; University of Toronto Scarborough, James You University of Waterloo, Dimi Racordon EPFL, LAMP, Ondřej Lhoták University of Waterloo | ||
12:10 - 13:40 | |||
12:10 90mLunch | Lunch Catering | ||
13:40 - 15:20 | VerificationSAS at Orchid East Chair(s): Olivier Danvy Yale-NUS College and School of Computing, Singapore | ||
13:40 60mKeynote | Multi-Modal Verification of Distributed Systems in Lean SAS Ilya Sergey National University of Singapore | ||
14:40 20mTalk | Verifying Neural Networks with PyRAT SAS Tristan Le Gall CEA LIST, Augustin Lemesle CEA, LIST, France, Julien Lehmann CEA, LIST, France, Zakaria Chihani CEA, LIST, France | ||
15:00 20mTalk | Enhancing Neural Network Robustness via Synthesis of Repair Programs SAS | ||
13:40 - 15:20 | |||
13:40 25mTalk | Call-Guarded Abstract Definitional InterpretersDistinguished Paper ICFP Papers Kimball Germane Brigham Young University DOI | ||
14:05 25mTalk | Effectful Lenses: There and Back with Different MonadsDistinguished Paper ICFP Papers DOI | ||
14:30 25mTalk | First-Order LazinessDistinguished Paper ICFP Papers Anton Lorenzen University of Edinburgh, Daan Leijen Microsoft Research, Wouter Swierstra Utrecht University, Netherlands, Sam Lindley The University of Edinburgh DOI Pre-print | ||
14:55 25mTalk | Multi-stage Programming with Splice VariablesDistinguished Paper ICFP Papers DOI | ||
13:40 - 15:20 | |||
13:40 20mTalk | The Quest for Mutable Value Semantics in Scala The Scala Workshop Dimi Racordon EPFL, LAMP File Attached | ||
14:00 20mTalk | How Functional is Direct-Style? The Scala Workshop Adam Warski SoftwareMill File Attached | ||
14:20 20mTalk | ScalaF: Functional Refactoring Suggestions for Scala The Scala Workshop Shiv Kiran Bagathi Indian Institute of Technology Bombay, Shrikha Mahanty Indian Institute of Technology Mandi, Dasari Gnana Heemmanshuu Indian Institute of Technology Bombay, Manas Thakur IIT Bombay File Attached | ||
14:40 20mTalk | Debugging for Scala Control Flow DSLs The Scala Workshop | ||
15:00 20mTalk | Migrating Large-scale Scala Projects to Explicit-nulls with the Help from LLMs The Scala Workshop Yaoyu Zhao EPFL, LAMP File Attached | ||
15:20 - 16:00 | |||
15:20 40mCoffee break | Break Catering | ||
16:00 - 17:40 | |||
16:00 20mTalk | Relating Distances and Abstractions: An Abstract Interpretation Perspective SAS Marco Campion INRIA & ENS Paris | Université PSL, Isabella Mastroeni University of Verona, Caterina Urban Inria & ENS | PSL | ||
16:20 20mTalk | Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty SAS Zixin Huang University of Illinois at Urbana-Champaign, USA, Jacob Laurel Georgia Institute of Technology, Saikat Dutta University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign | ||
16:40 20mTalk | Specifying and Verifying Future Conditions SAS Yahui Song Standard Chartered Bank, Darius Foo National University of Singapore, Wei-Ngan Chin National University of Singapore | ||
17:00 20mTalk | Contextual Equality Saturation SAS | ||
17:20 20mTalk | Abstracting Concolic Execution for Soft Contract Verification SAS Bram Vandenbogaerde , Quentin Stiévenart Université du Québec à Montréal, Coen De Roover Vrije Universiteit Brussel Pre-print | ||
16:00 - 17:40 | |||
16:00 25mTalk | Pushing the Information-Theoretic Limits of Random Access Lists ICFP Papers Edward Peters , Yong Qi Foo National University of Singapore, Michael D. Adams National University of Singapore DOI | ||
16:25 25mTalk | Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl) ICFP Papers DOI | ||
16:50 25mPaper | Bottom-up computation using trees of sublists ICFP JFP First Papers Shin-Cheng Mu Academia Sinica, Taiwan DOI | ||
17:15 25mPaper | You could have invented Fenwick treesRemote ICFP JFP First Papers Brent Yorgey Hendrix College DOI | ||
16:00 - 17:40 | |||
16:00 25mPaper | A contextual formalization of structural coinduction ICFP JFP First Papers DOI | ||
16:25 25mPaper | A practical formalization of monadic equational reasoning in dependent-type theory ICFP JFP First Papers Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan, Jacques Garrigue , Takafumi Saikawa Nagoya University DOI | ||
16:50 25mTalk | Almost Fair Simulations ICFP Papers Arthur Correnson CISPA Helmholtz Center for Information Security, Iona Kuhn Saarland University, Bernd Finkbeiner CISPA Helmholtz Center for Information Security DOI | ||
17:15 25mTalk | Big Steps in Higher-Order Mathematical Operational Semantics ICFP Papers Sergey Goncharov University of Birmingham, Pouya Partow Birmingham University, Stelios Tsampas University of Southern Denmark DOI | ||
16:00 - 17:40 | |||
16:00 15mTalk | Challenges in Practice: Building a Usable Library for Planetary-Scale Embeddings PROPL Sadiq Jaffer University of Cambridge, Frank Feng University of Cambridge, Robin Young University of Cambridge, Srinivasan Keshav University of Cambridge, Anil Madhavapeddy University of Cambridge, UK, Robin Young University of Cambridge | ||
16:15 15mPaper | STACD: STAC Extension with DAGs for Geospatial Data and Algorithm Management PROPL Saharsh Laud Indian Institute Of Technology Delhi, Saurabh Joshi Indian Institute Of Technology Delhi, Tarun Mangla Indian Institute Of Technology Delhi, Abhilash Jindal IIT Delhi, India, Aaditeshwar Seth Indian Institute Of Technology Delhi | ||
16:30 15mTalk | Spatial Programming for Environmental Monitoring PROPL Josh Millar Imperial College London, Ryan Gibb University of Cambridge, Roy Ang University of Cambridge, Hamed Haddadi Imperial College London, Anil Madhavapeddy University of Cambridge, UK | ||
16:45 15mPaper | Yirgacheffe: a declarative approach to geospatial data PROPL Michael Dales University of Cambridge, UK, Alison Eyres University of Cambridge, Patrick Ferris University of Cambridge, UK, Anil Madhavapeddy University of Cambridge, UK, Francesca A. Ridley Newcastle University, Simon Tarr IUCN | ||
17:00 15mTalk | Large Language Models for computational climate analysis PROPL Jay Torry University of Cambridge | ||
17:15 15mTalk | Scaling the Urban Forest: An Integrated Framework for Managing Cities by Fusing Raster and Vector Data PROPL Andrés C. Zúñiga-González University of Cambridge, Anil Madhavapeddy University of Cambridge, UK, Ronita Bardhan University of Cambridge | ||
17:30 10mDay closing | Closing thoughts from the chairs PROPL Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Dominic Orchard University of Cambridge; University of Kent | ||
18:00 - 20:00 | |||
18:00 2hSocial Event | ICFP SRC Poster Session ICFP Student Research Competition | ||
Tue 14 OctDisplayed time zone: Perth change
Tue 14 Oct
Displayed time zone: Perth change
09:00 - 10:10 | |||
09:00 70mKeynote | The Rational Programmer, A Method for Investigating Programming Language Pragmatics ICFP Keynotes Christos Dimoulas Northwestern University | ||
10:10 - 10:50 | |||
10:10 40mCoffee break | Break Catering | ||
10:50 - 12:05 | |||
10:50 55mKeynote | From Within: Compiler Testing and Validation via Compilers SAS Qirun Zhang Georgia Institute of Technology | ||
11:45 20mTalk | Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and Data-Flow Analysis SAS | ||
10:50 - 12:05 | |||
10:50 25mTalk | Robust Dynamic Embedding for Gradual Typing ICFP Papers Koen Jacobs Inria, Matías Toro University of Chile, Nicolas Tabareau Inria, Éric Tanter University of Chile DOI | ||
11:15 25mPaper | A simple blame calculus for explicit nulls ICFP JFP First Papers DOI | ||
11:40 25mTalk | SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F* ICFP Papers Cezar-Constantin Andrici MPI-SP, Danel Ahman University of Ljubljana, Cătălin Hriţcu MPI-SP, Ruxandra Icleanu University of Edinburgh, Guido Martínez Microsoft Research, Exequiel Rivas Tallinn University of Technology; Ahrefs, Théo Winterhalter INRIA DOI | ||
10:50 - 12:05 | |||
10:50 25mTalk | Usability Barriers for Liquid Types (Summary of Published Work) HATRA Catarina Gamboa Carnegie Mellon University and University of Lisbon, Abigail Elena Reese Carnegie Mellon University, Alcides Fonseca LASIGE; University of Lisbon, Jonathan Aldrich Carnegie Mellon University | ||
11:15 25mTalk | Imperative Syntax for Dependent Types HATRA | ||
11:40 25mTalk | Decomposable Type Highlighting for Bidirectional Type and Cast Systems HATRA Max Carroll University of Cambridge, Patrick Ferris University of Cambridge, UK, Anil Madhavapeddy University of Cambridge, UK | ||
10:50 - 12:05 | |||
10:50 25mTalk | Compiling with Generating Functions ICFP Papers DOI | ||
11:15 25mTalk | Correctness Meets Performance: From Agda to Futhark ICFP Papers DOI | ||
11:40 25mPaper | Domain-specific tensor languages ICFP JFP First Papers Jean-Philippe Bernardy University of Gothenburg, Sweden, Patrik Jansson Chalmers University of Technology and University of Gothenbrug DOI | ||
10:50 - 12:05 | Capabilities and ownership in ScalaThe Scala Workshop at Peony NE Chair(s): Oliver Bračevac EPFL, LAMP, Hamza Remmal EPFL, LAMP Joint session with IWACO on Tuesday October 14 | ||
10:50 35mKeynote | Where Are We With Scala's Capabilities? The Scala Workshop | ||
11:25 20mTalk | System Capybara: Capture Tracking for Ownership and Borrowing The Scala Workshop File Attached | ||
11:45 20mTalk | Capability-Safe Erasure in ScalaRemote The Scala Workshop File Attached | ||
10:50 - 12:05 | |||
10:50 25mTalk | Bringing Together Cross-ISA Checkpoint/Restoration and AOT Compilation of WebAssembly Programs MPLR Raiki Tamura Kyoto University, Daisuke Kotani Kyoto University, Kazuyuki Shudo Kyoto University, Yasuo Okabe Kyoto University | ||
11:15 25mTalk | A Snapshot of the Performance of Wasm Backends for Managed Languages MPLR | ||
11:40 25mTalk | JASMaint: Portable Multi-language Taint Analysis for the Web MPLR Abel Stuker Vrije Universiteit Brussel, Aäron Munsters Vrije Universiteit Brussel, Angel Luis Scull Pupo Vrije Universiteit Brussel, Laurent Christophe Vrije Universiteit Brussel, Elisa Gonzalez Boix Vrije Universiteit Brussel | ||
10:50 - 12:05 | |||
10:50 5mDay opening | Opening OlivierFest Julia Lawall Inria, Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital, Jens Palsberg University of California, Los Angeles (UCLA), Ilya Sergey National University of Singapore | ||
10:55 20mTalk | Continuations in Musicfestschrift OlivierFest Youyou Cong Institute of Science Tokyo | ||
11:15 25mTalk | Exotic Uses of Continuations OlivierFest Michael D. Adams National University of Singapore | ||
11:40 25mTalk | Invertible Syntax without the Tuples (Functional Pearl)festschrift OlivierFest | ||
12:10 - 13:40 | |||
12:10 90mLunch | Lunch Catering | ||
12:10 - 13:40 | |||
13:40 - 15:20 | |||
13:40 60mKeynote | Towards static analyses and abstract domains for hyperproperties SAS Xavier Rival Inria; ENS; CNRS; PSL University | ||
14:40 20mTalk | Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis SAS Matan Shachnai , Harishankar Vishwanathan , Srinivas Narayana Rutgers University, Santosh Nagarakatte Rutgers University | ||
15:00 20mTalk | A Programming Language for Feasible Solutions SAS Weijun Chen Shanghai Jiao Tong University, China, Yuxi Fu Shanghai Jiao Tong University, China, Huan Long Shanghai Jiao Tong University | ||
13:40 - 15:20 | |||
13:40 25mTalk | Fulls Seldom Differ ICFP Papers Mark Koch Quantinuum, Alan Lawrence Quantinuum, Conor McBride University of Strathclyde, Craig Roy Quantinuum DOI | ||
14:05 25mTalk | Normalization by Evaluation for Non-cumulativity ICFP Papers Shengyi Jiang The University of Hong Kong, Jason Z. S. Hu Amazon, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
14:30 25mTalk | Type Theory in Type Theory using a Strictified Syntax ICFP Papers DOI Pre-print | ||
14:55 25mTalk | Type Universes as Kripke Worlds ICFP Papers Paulette Koronkevich University of British Columbia, William J. Bowman University of British Columbia DOI Pre-print | ||
13:40 - 15:20 | |||
13:40 25mTalk | Negative Bounds for Avoiding Conflicts in Implementing Traits in Rust HATRA | ||
14:05 25mTalk | P4-SpecTec: A Language Mechanization Framework for P4 HATRA | ||
14:30 25mTalk | Types as a Specification Language for Creativity HATRA Youyou Cong Institute of Science Tokyo | ||
14:55 25mTalk | Actema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestural Interaction HATRA | ||
13:40 - 15:25 | |||
13:40 25mTalk | A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware ICFP Papers Liyi Li Iowa State University, David Young University of Kansas, USA, James Bryan Graves Indiana University, Chandeepa Dissanayake Iowa State University, Amr Sabry Indiana University DOI | ||
14:05 25mTalk | Functional Networking for Millions of Docker Desktops (Experience Report) ICFP Papers Anil Madhavapeddy University of Cambridge, UK, David J. Scott Docker, Inc., Patrick Ferris University of Cambridge, UK, Ryan Gibb University of Cambridge, Thomas Gazagnaire Tarides DOI | ||
14:30 25mTalk | Polynomial-Time Program Equivalence for Machine Knitting ICFP Papers Nathan Hurtig University of Washington, Jenny Han Lin University of Utah, Thomas S. Price Carnegie Mellon University, Adriana Schulz University of Washington, James McCann Carnegie Mellon University, Gilbert Bernstein University of Washington DOI | ||
14:55 30mTalk | SRC Talks ICFP Student Research Competition | ||
13:40 - 15:20 | |||
13:40 30mTalk | A Verified Thread-Safe Array in Rust IWACO Sasha Pak The Australian National University, Fabian Muehlboeck Australian National University, Alex Potanin Australian National University | ||
14:10 30mTalk | Unfolding Expressions for Gradual Verification IWACO Hazel Torek Clemson University, Long Tien Nguyen Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University | ||
14:40 30mTalk | Gradual Verification: Assuring Software Incrementally IWACO Jonathan Aldrich Carnegie Mellon University | ||
13:40 - 15:25 | |||
13:40 40mKeynote | Joy of Meta-Tracing Just-in-Time Compilation: More Than Just a VM GeneratorMPLR Keynote MPLR Hidehiko Masuhara Institute of Science Tokyo | ||
14:20 25mTalk | A Control-Flow Graph Approach to Language-Agnostic Debugging for Microcontrollers MPLR Carlos Rojas Castillo Vrije Universiteit Brussel, Matteo Marra Nokia Bell Labs, Belgium, Elisa Gonzalez Boix Vrije Universiteit Brussel | ||
14:45 25mTalk | Co-operative JIT Compilation for Resource-Constrained Low-Power Coprocessors MPLR Go Suzuki Institute of Science Tokyo, Takuo Watanabe Institute of Science Tokyo, Sosuke Moriguchi Institute of Science Tokyo | ||
15:10 15mTalk | SmartSweep: Efficient Space Reclamation in Tiered Managed HeapsWIP Research MPLR Iacovos Kolokasis University of Crete, Konstantinos Delis University of Crete and FORTH-ICS, Shoaib Akram Australian National University, Foivos S. Zakkak Red Hat, Polyvios Pratikakis University of Crete, Angelos Bilas University of Crete and FORTH, Greece | ||
13:40 - 15:20 | |||
13:40 25mTalk | Defining Algebraic Effects and Handlers via Trails and Metacontinuationsfestschrift OlivierFest | ||
14:05 25mTalk | A Compositional Semantics for eval in Schemefestschrift OlivierFest Peter D. Mosses Swansea University and Delft University of Technology | ||
14:30 25mTalk | Generic Reduction-Based Interpretersfestschrift OlivierFest Casper Bach University of Southern Denmark | ||
14:55 25mTalk | Safe-for-Space Linked Environmentsfestschrift OlivierFest | ||
15:20 - 16:00 | |||
15:20 40mCoffee break | Break Catering | ||
16:00 - 17:40 | |||
16:00 20mTalk | Bounded-Exhaustive Subspace Diversification for SMT Solver Testing SAS | ||
16:20 20mTalk | Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell SAS Bram Vandenbogaerde , Sarah Verbelen Vrije Universiteit Brussel, Belgium, Noah Van Es Sofware Languages Lab, Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel | ||
16:40 20mTalk | Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters SAS Noah Van Es Sofware Languages Lab, Vrije Universiteit Brussel, Bram Vandenbogaerde , Coen De Roover Vrije Universiteit Brussel | ||
17:00 20mTalk | Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types SAS Hiroyuki Katsura , Naoki Kobayashi University of Tokyo, Ken Sakayori University of Tokyo, Ryosuke Sato Tokyo University of Agriculture and Technology | ||
17:20 20mTalk | Formal Analysis of Networked PLC Controllers Interacting with Physical Environments SAS | ||
16:00 - 18:00 | |||
16:00 30mTalk | ICFP Contest Report ICFP Papers | ||
16:30 15mAwards | Award Ceremony ICFP Papers | ||
16:45 5mAwards | SRC Awards ICFP Student Research Competition | ||
16:50 15mMeeting | PC Chair Report ICFP Papers | ||
17:05 10mTalk | General Chair Report ICFP Papers | ||
17:15 10mTalk | ICFP 2026 Announcement ICFP Papers Sam Tobin-Hochstadt Indiana University | ||
16:00 - 17:40 | |||
16:00 1h40mMeeting | Discussion HATRA Michael Coblenz University of California, San Diego, Jonathan Aldrich Carnegie Mellon University, Will Crichton Brown University | ||
16:00 - 17:40 | |||
16:00 30mTalk | Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning IWACO | ||
16:30 30mTalk | Type Universes as Kripke Worlds: Memory Management Edition IWACO Paulette Koronkevich University of British Columbia | ||
17:00 30mTalk | TBD IWACO Mae Milano Princeton University | ||
16:00 - 17:45 | |||
16:00 25mTalk | On the structure of abstract interpretersfestschrift OlivierFest Wonyeol Lee POSTECH, Matthieu Lemerre Université Paris-Saclay - CEA LIST, Xavier Rival Inria; ENS; CNRS; PSL University, Hongseok Yang KAIST | ||
16:25 25mTalk | Understanding Linux-Kernel Code Through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_corefestschrift OlivierFest | ||
16:50 25mTalk | Simple Closure Analysis Revisitedfestschrift OlivierFest Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital | ||
17:15 15mTalk | Mixing transformation and symbolic execution with continuation for WebAssembly OlivierFest Guannan Wei Tufts University | ||
17:30 15mTalk | Data-Centric Functional Programming with First-Class Finite Maps and Tabulated Abstractions OlivierFest Tiark Rompf Purdue University | ||
Wed 15 OctDisplayed time zone: Perth change
Wed 15 Oct
Displayed time zone: Perth change
09:00 - 10:10 | |||
09:00 70mKeynote | Proof-Carrying Neuro-Symbolic Code ICFP Keynotes Ekaterina Komendantskaya Heriot-Watt University and Southampton University | ||
10:10 - 10:50 | |||
10:10 40mCoffee break | Break Catering | ||
10:50 - 12:05 | |||
10:50 75mKeynote | AI Safety through Programming? LMPL Jun Sun Singapore Management University | ||
10:50 - 12:05 | |||
10:50 25mTalk | A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free ICFP Papers Cyril Cohen Inria - CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668, Kazuhiko Sakaguchi CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668 DOI Pre-print | ||
11:15 25mTalk | CRDT Emulation, Simulation, and Representation Independence ICFP Papers Nathan Liittschwager University of California, Santa Cruz, Jonathan Castello University of California, Santa Cruz, Stelios Tsampas University of Southern Denmark, Lindsey Kuper University of California, Santa Cruz DOI Pre-print | ||
11:40 25mPaper | How much is in a square? Calculating functional programs with squares ICFP JFP First Papers Jose Nuno Oliveira University of Minho; INESC TEC DOI | ||
10:50 - 12:05 | |||
10:50 25mTalk | Fusing Session-Typed Concurrent Programming into Functional Programming ICFP Papers Chuta Sano McGill University, Deepak Garg MPI-SWS, Ryan Kavanagh Université du Québec à Montréal, Brigitte Pientka McGill University, Bernardo Toninho Instituto Superior Técnico - University of Lisbon DOI | ||
11:15 25mTalk | Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs ICFP Papers Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Philipp G. Haselwarter Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University DOI Pre-print | ||
11:40 25mTalk | Relax! The Semilenient Core of Choreographic Programming (Functional Pearl) ICFP Papers Dan Plyukhin University of Southern Denmark, Xueying Qin University of Southern Denmark, Fabrizio Montesi University of Southern Denmark DOI Pre-print | ||
10:50 - 12:05 | |||
10:50 5mDay opening | Welcome VMIL | ||
10:55 25mResearch paper | Copy-and-Patch Just-in-Time Compiler for R VMIL Matěj Kocourek Charles University, Filip Křikava Czech Technical University in Prague, Jan Vitek Northeastern University DOI | ||
11:25 25mResearch paper | ASTro: An AST-based Reusable Optimization Framework VMIL Koich Sasada Stores, Inc. | ||
11:50 15mShort-paper | Evaluating Candidate Instructions for Reliable Program Slowdown at the Compiler Level - Towards Supporting Fine-grained Slowdown for Advanced Developer Tooling VMIL DOI Pre-print | ||
10:50 - 12:05 | |||
10:50 25mTalk | Controlling Copatterns: There and Back Againfestschrift OlivierFest Paul Downen University of Massachusetts at Lowell | ||
11:15 25mTalk | Deforestation through refunctionalization OlivierFest Lionel Parreaux HKUST (The Hong Kong University of Science and Technology) | ||
11:40 25mTalk | Encoding Product Typesfestschrift OlivierFest Sam Lindley The University of Edinburgh | ||
12:10 - 13:40 | |||
12:10 90mLunch | Lunch Catering | ||
12:10 - 13:40 | |||
13:40 - 15:20 | LLMs for Program Analysis and Verification ILMPL at Orchid East Chair(s): Guannan Wei Tufts University | ||
13:40 15mTalk | Function Renaming in Reverse Engineering of Embedded Device Firmware with ChatGPT LMPL Puzhuo Liu Ant Group & Tsinghua University, Peng Di Ant Group & UNSW Sydney, Yu Jiang Tsinghua University | ||
13:55 15mTalk | Enhancing Semantic Understanding in Pointer Analysis Using Large Language Models LMPL Baijun Cheng Peking University, Kailong Wang Huazhong University of Science and Technology, Ling Shi Nanyang Technological University, Haoyu Wang Huazhong University of Science and Technology, Yao Guo Peking University, Ding Li Peking University, Xiangqun Chen Peking University | ||
14:10 15mTalk | Improving SAST Detection Capability with LLMs and Enhanced DFA LMPL Yuan Luo Tencent Security Yunding Lab, Zhaojun Chen Tencent Security Yunding Lab, Yuxin Dong Peking University, Haiquan Zhang Tencent Security Yunding Lab, Yi Sun Tencent Security Yunding Lab, Fei Xie Tencent Security Yunding Lab, Zhiqiang Dong Tencent Security Yunding Lab | ||
14:25 15mTalk | ClearAgent: Agentic Binary Analysis for Effective Vulnerability Detection LMPL Xiang Chen The Hong Kong University of Science and Technology, Anshunkang Zhou The Hong Kong University of Science and Technology, Chengfeng Ye The Hong Kong University of Science and Technology, Charles Zhang The Hong Kong University of Science and Technology | ||
14:40 15mTalk | CG-Bench: Can Language Models Assist Call Graph Construction in the Real World? LMPL Ting Yuan , Wenrui Zhang Huawei Technologies Co., Ltd, Dong Chen Huawei, Jie Wang Huawei Technologies Co., Ltd Pre-print | ||
14:55 20mTalk | Beyond Static Pattern Matching? Rethinking Automatic Cryptographic API Misuse Detection in the Era of LLMs LMPL | ||
13:40 - 15:20 | |||
13:40 25mTalk | Formal Semantics and Program Logics for a Fragment of OCaml ICFP Papers DOI | ||
14:05 25mTalk | Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language ICFP Papers DOI Pre-print | ||
14:30 25mTalk | Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach ICFP Papers Marcos Grandury IMDEA Software Institute; Universidad Politécnica de Madrid, Aleksandar Nanevski IMDEA Software Institute, Alexander Gryzlov IMDEA Software Institute DOI | ||
14:55 25mTalk | Reasoning about Weak Isolation Levels in Separation Logic ICFP Papers Anders Alnor Mathiasen Aarhus University, Léon Gondelman Aalborg University, Léon Ducruet Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus University DOI | ||
13:40 - 15:20 | |||
13:40 25mTalk | McTT: A Verified Kernel for a Proof Assistant ICFP Papers Junyoung Jang McGill University, Antoine Gaulin McGill University, Jason Z. S. Hu Amazon, Brigitte Pientka McGill University DOI Media Attached | ||
14:05 25mTalk | Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl) ICFP Papers Maximilian Doré University of Oxford DOI Pre-print | ||
14:30 25mPaper | Binary search—think positive ICFP JFP First Papers DOI | ||
14:55 25mTalk | Teaching Software Specification (Experience Report) ICFP Papers DOI | ||
13:40 - 15:20 | |||
13:40 70mTalk | [Invited Talk] Notational Freedom via Self-Raising Diagrams PAINT Joel Jakubovic Charles University in Prague | ||
14:50 30mTalk | Block-based Editing in a Textual World PAINT Tom Beckmann Hasso Plattner Institute, Lukas Böhme Hasso Plattner Institute, University of Potsdam, Potsdam, Germany, Marcel Taeumel University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld Hasso Plattner Institute; University of Potsdam | ||
13:40 - 15:20 | |||
13:40 60mKeynote | The Wild West of post-POSIX IO Interfaces VMIL Anil Madhavapeddy University of Cambridge, UK | ||
14:40 15mShort-paper | Heterogeneous translation of Scala-like function types in Java-TX VMIL Julian Schmidt Baden-Wuerttemberg Cooperative State University, Daniel Holle Baden-Wuerttemberg Cooperative State University, Martin Plümicke DHBW Stuttgart, Campus Horb, Germany | ||
14:55 15mTalk | TEAL: a Total Expressive Assembly Language VMIL | ||
13:40 - 15:25 | |||
13:40 25mTalk | What I Always Wanted to Know About Second Class Valuesfestschrift OlivierFest Peter Thiemann University of Freiburg, Germany | ||
14:05 25mTalk | A Tale of two Zippersfestschrift OlivierFest | ||
14:30 25mTalk | Verified Nanopasses for Compiling Conditionalsfestschrift OlivierFest Jeremy G. Siek Indiana University, USA | ||
14:55 15mTalk | Verifying Effectful Programs via Answer-Type Modification OlivierFest Taro Sekiyama National Institute of Informatics | ||
15:10 15mTalk | From Delimited Continuations to Staged Logics OlivierFest Wei-Ngan Chin National University of Singapore, Darius Foo National University of Singapore, Yahui Song Standard Chartered Bank | ||
15:20 - 16:00 | |||
15:20 40mCoffee break | Break Catering | ||
16:00 - 17:40 | LLMs for Program Analysis and Verification IILMPL at Orchid East Chair(s): Zhuo Zhang Columbia University | ||
16:00 15mTalk | Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis LMPL | ||
16:15 20mTalk | Toward Repository-Level Program Verification with Large Language Models LMPL DOI | ||
16:35 15mTalk | Preguss: It Analyzes, It Specifies, It Verifies LMPL Zhongyi Wang Zhejiang University, China, Tengjie Lin Zhejiang University, Mingshuai Chen Zhejiang University, Mingqi Yang Zhejiang University, Haokun Li Peking University, Xiao Yi The Chinese University of Hong Kong, Shengchao Qin Xidian University, Jianwei Yin Zhejiang University | ||
16:50 20mTalk | A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants LMPL Barış Bayazıt University of Toronto, Yao Li Portland State University, Xujie Si University of Toronto Pre-print | ||
17:10 20mTalk | Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters LMPL Jacqueline Mitchell University of Southern California, Brian Hyeongseok Kim University of Southern California, Chenyu Zhou University of Southern California, Chao Wang University of Southern California | ||
16:00 - 17:40 | |||
16:00 15mTalk | Vibe Coding Needs Vibe Reasoning – Improving Vibe Coding with Formal Verification LMPL | ||
16:15 15mTalk | Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better LMPL Aaron Bembenek The University of Melbourne Pre-print | ||
16:30 15mTalk | Composable Effect Handling for Programming LLM-integrated Scripts LMPL Di Wang Peking University Pre-print | ||
16:45 15mTalk | The LLM Era Demands Natural-Language-Aligned Theorem Provers for Mathematics LMPL Qinxiang Cao Shanghai Jiao Tong University, Lihan Xie Shanghai Jiao Tong University, Junchi Yan Shanghai Jiao Tong University | ||
17:00 15mTalk | Programming Large Language Models with Algebraic Effect Handlers and the Selection Monad LMPL Shangyin Tan University of California, Berkeley, Guannan Wei Tufts University, Koushik Sen University of California at Berkeley, Matei Zaharia UC Berkeley | ||
16:00 - 17:40 | |||
16:00 30mTalk | TIDE: An Educational Live Programming Environment to Compose Graphics with PyTamaro PAINT Joey Bevilacqua Università della Svizzera italiana, Nathan Coquerel Rennes University, Luca Chiodini USI Lugano, Igor Moreno Santos USI Lugano, Matthias Hauswirth USI Lugano DOI | ||
16:30 30mTalk | The MNL: A Block-based Functional Programming Language with Reactive Blocks PAINT Steven Lolong University of Tübingen | ||
17:00 30mTalk | Toward Bridging the Tool Gap: Equipping Large Language Models with Tools to Answer Programmers’ Questions PAINT Lukas Böhme Hasso Plattner Institute, University of Potsdam, Potsdam, Germany, Christoph Thiede Hasso Plattner Institute, University of Potsdam, Germany, Toni Mattis University of Potsdam; Hasso Plattner Institute, Tom Beckmann Hasso Plattner Institute, Jens Lincke Hasso Plattner Institute; University of Potsdam, Robert Hirschfeld Hasso Plattner Institute; University of Potsdam | ||
17:30 10mDay closing | Closing PAINT | ||
16:00 - 17:40 | |||
16:00 25mResearch paper | MaTSa: Race Detection in Java VMIL Alexandros Emmanouil Antonakakis ICS-FORTH & University of Crete, Polyvios Pratikakis University of Crete, Angelos Bilas University of Crete and FORTH, Greece, Foivos S. Zakkak Red Hat, Iacovos Kolokasis University of Crete | ||
16:25 25mResearch paper | Memory Tiering in Python Virtual Machine VMIL Yuze Li Virginia Tech, Shunyu Yao Virginia Tech, Jaiaid Mobin Rochester Institute of Technology, Tianyu Zhan Virginia Tech, M. Mustafa Rafique Rochester Institute of Technology, Dimitrios Nikolopoulos Virginia Tech, Kirshanthan Sundararajah Virginia Tech, Ali R. Butt Virginia Tech | ||
16:50 15mShort-paper | RuntimeSave: A Graph Database of Runtime Values VMIL Matúš Sulír Technical University of Košice, Antonia Bertolino Gran Sasso Science Institute, Guglielmo De Angelis CNR-IASI Pre-print | ||
17:05 5mDay closing | Closing VMIL | ||
16:00 - 17:40 | |||
16:00 50mTalk | More than a Colleague: Celebrating Olivier’s Impact OlivierFest Charles Consel Bordeaux-INP, Andrzej Filinski DIKU, University of Copenhagen, Zhenjiang Hu Peking University, David Schmidt , Torben Amtoft Kansas State University, Jens Palsberg University of California, Los Angeles (UCLA), Jacob Johannsen Independent, Chantal Keller Université Paris-Saclay, CNRS, LMF | ||
16:50 50mTalk | TBA OlivierFest Olivier Danvy Yale-NUS College and School of Computing, Singapore | ||
19:00 - 21:00 | |||
Thu 16 OctDisplayed time zone: Perth change
Thu 16 Oct
Displayed time zone: Perth change
09:00 - 10:00 | |||
09:00 60mKeynote | Automating maintenance of the Linux kernel: a perspective over 20 years SPLASH Keynotes | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:15 | |||
10:30 15mTalk | Unveiling Heisenbugs with Diversified Execution SPLASH OOPSLA Arjun Ramesh Carnegie Mellon University, Tianshu Huang Carnegie Mellon University, Jaspreet Riar Carnegie Mellon University, Ben L. Titzer Carnegie Mellon University, Anthony Rowe Carnegie Mellon University | ||
10:45 15mTalk | TailTracer: Continuous Tail Tracing for Production Use SPLASH OOPSLA Tianyi Liu Nanjing University, Yi Li Nanyang Technological University, Yiyu Zhang Nanjing University, Zhuangda Wang Xiamen University, Rongxin Wu Xiamen University, Xuandong Li Nanjing University, Zhiqiang Zuo Nanjing University | ||
11:00 15mTalk | Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees SPLASH OOPSLA Matteo Basso Università della Svizzera italiana (USI), Aleksandar Prokopec Oracle Labs, Andrea Rosà USI Lugano, Walter Binder USI Lugano | ||
11:15 15mTalk | Float Self-Tagging SPLASH OOPSLA Olivier Melançon Université de Montréal, Manuel Serrano Inria; Université Côte d’Azur, Marc Feeley Université de Montréal Pre-print | ||
11:30 15mTalk | HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines SPLASH OOPSLA Vladyslav Nekriach University Of Toronto, Sidi Mohamed Beillahi University of Toronto, Chenxing Li Shanghai Tree-Graph Blockchain Research Institute, Peilun Li Shanghai Tree-Graph Blockchain Research Institute, Ming Wu Shanghai Tree-Graph Blockchain Research Institute, Andreas Veneris University of Toronto, Fan Long University of Toronto | ||
11:45 15mTalk | Advancing Performance via a Systematic Application of Research and Industrial Best Practice SPLASH OOPSLA Wenyu Zhao Australian National University, Stephen M. Blackburn Google; Australian National University, Kathryn S McKinley Google, Man Cao Google, Sara S. Hamouda Canva | ||
10:30 - 12:15 | |||
10:30 15mTalk | ABC: Towards a Universal Code Styler through Model Merging SPLASH OOPSLA Yitong Chen School of Computer Science and Engineering, College of Software Engineering, School of Artificial Intelligence, Southeast University, Zhiqiang Gao School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University, Chuanqi Shi School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University, Baixuan Li School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University, Miao Gao School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University | ||
10:45 15mTalk | Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation SPLASH OOPSLA | ||
11:00 15mTalk | Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations SPLASH OOPSLA Zhenyang Xu University of Waterloo, Yongqiang Tian Monash University, Mengxiao Zhang , Chengnian Sun University of Waterloo | ||
11:15 15mTalk | Code Style Sheets: CSS for Code SPLASH OOPSLA | ||
11:30 15mTalk | Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection SPLASH OOPSLA | ||
11:45 15mTalk | PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns SPLASH OOPSLA | ||
12:00 15mTalk | Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes SPLASH OOPSLA Mingyi Li , Junmin Xiao , Siyan Chen Institute of Computing Technology, Chinese Academy of Sciences, Hui Ma Institute of Computing Technology, Chinese Academy of Sciences, Xi Chen Institute of Computing Technology, Chinese Academy of Sciences, Peihua Bao University of Chinese Academy of Sciences, Liang Yuan Chinese Academy of Sciences, Guangming Tan Chinese Academy of Sciences(CAS) | ||
10:30 - 12:15 | |||
10:30 5mDay opening | Welcome ML Family Workshop Sam Westrick New York University | ||
10:35 30mTalk | MsML: A Proposal for a successor MLRemote ML Family Workshop David MacQueen University of Chicago (Emeritus) | ||
11:05 30mTalk | Range-Analysis-Based Optimization for SML/NJ ML Family Workshop | ||
11:35 30mTalk | LunarML: From Standard ML to Scripting Languages ML Family Workshop Mizuki Arata None | ||
10:30 - 12:15 | Implementation, Application, and TypesScheme at Peony NW Chair(s): Paul Downen University of Massachusetts at Lowell | ||
10:30 5mDay opening | Welcome Scheme | ||
10:35 25mTalk | Stak Scheme: The tiny R7RS-small implementation Scheme File Attached | ||
11:00 25mTalk | Gouki Scheme: An Embedded Scheme Implementation for Async Rust Scheme Matthew Plant OneChronos File Attached | ||
11:25 25mTalk | Automatic Invariant Testing for Finite-State Machines Scheme Marco Morazan pc, Sophia Turano Seton Hall University, Andrés M. Garced Seton Hall University, David Anthony K. Fields Seton Hall University | ||
11:50 20mTalk | Sound Default-Typed Scheme (Position Paper) Scheme Jan-Paul Ramos-Davila Boston University File Attached | ||
10:30 - 12:15 | |||
10:30 10mTalk | Opening SPLASH Onward! Papers | ||
10:40 30mTalk | Sharing is Scaring: Linking Cloud File-Sharing to Programming Language Semantics SPLASH Onward! Papers Skyler Austen Brown University, Shriram Krishnamurthi Brown University, Kathi Fisler Brown University | ||
11:10 30mTalk | On Collective Control over User Interfaces in the Face of Network Effects SPLASH Onward! Papers | ||
11:40 30mTalk | Foundational Design Principles and Patterns for Building Robust & Adaptive GenAI-Native Systems SPLASH Onward! Papers Frederik Vandeputte Nokia Bell Labs Pre-print | ||
10:30 - 12:15 | |||
10:30 5mTalk | Welcome Haskell | ||
10:35 30mResearch paper | Freer Arrows and Why You Need Them in Haskell Haskell Grant VanDomelen Portland State University, USA, Gan Shen University of California at Santa Cruz, Lindsey Kuper University of California, Santa Cruz, Yao Li Portland State University Pre-print | ||
11:05 30mResearch paper | Lightweight Testing of Persistent Amortized Time Complexity in the Credit Monad Haskell Anton Lorenzen University of Edinburgh | ||
11:35 30mResearch paper | The Calculated Typer (Functional Pearl) Haskell Zac Garby University of Nottingham, Patrick Bahr IT University of Copenhagen, Graham Hutton University of Nottingham | ||
12:15 - 13:45 | |||
12:15 90mLunch | Lunch Catering | ||
13:45 - 15:30 | |||
13:45 15mTalk | A Unifying Approach to Product Constructions for Quantitative Temporal Inference SPLASH OOPSLA Kazuki Watanabe National Institute of Informatics; SOKENDAI, Sebastian Junges Radboud University, Jurriaan Rot Radboud University Nijmegen, Ichiro Hasuo National Institute of Informatics, Japan | ||
14:00 15mTalk | Contract System Metatheories à la Carte: A Transition-System View of Contracts SPLASH OOPSLA Shu-Hung You Northwestern University, USA, Christos Dimoulas Northwestern University, Robert Bruce Findler Northwestern University | ||
14:15 15mTalk | Incremental Bidirectional Typing via Order Maintenance SPLASH OOPSLA Thomas J. Porter University of Michigan, Marisa Kirisame University of Utah, Ivan Wei University of Michigan, Pavel Panchekha University of Utah, Cyrus Omar University of Michigan | ||
14:30 15mTalk | Integrating Resource Analyses via Resource Decomposition SPLASH OOPSLA Long Pham Carnegie Mellon University, Yue Niu National Institute of Informatics, Nathan Glover Carnegie Mellon University, Feras Saad Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University | ||
14:45 15mTalk | Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles SPLASH OOPSLA Zhineng Zhong Key Laboratory of High-Confidence Software Technologies (MOE), School of Computer Science, Peking University, Ziqi Zhang University of Illinois Urbana-Champaign, Hanqin Guan Peking University, Ding Li Peking University | ||
15:00 15mTalk | Software Model Checking via Summary-Guided Search SPLASH OOPSLA Ruijie Fang University of Texas at Austin, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison DOI Pre-print | ||
15:15 15mTalk | The Power of Regular Constraint Propagation SPLASH OOPSLA Matthew Hague Royal Holloway University of London, Artur Jez University of Wroclaw, Anthony Widjaja Lin RPTU Kaiserslautern-Landau and Max-Planck Institute for Software Systems, Oliver Markgraf RPTU Kaiserslautern-Landau, Philipp Ruemmer University of Regensburg and Uppsala University | ||
13:45 - 15:30 | |||
13:45 30mTalk | Freezing Bidirectional Typing (Extended Abstract) ML Family Workshop Wenhao Tang The University of Edinburgh, Shengyi Jiang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Sam Lindley The University of Edinburgh | ||
14:15 30mTalk | A typed approach to ontology manipulation (experience report) ML Family Workshop Davide Camino University of Torino, Italy, Andrea Zito University of Torino, Italy, Viviana Bono University of Torino, Lorenzo Bafunno University of Torino, Italy, Lorenzo Pasini University of Torino, Italy, Emanuele Rovaretto University of Torino, Italy | ||
14:45 45mTalk | From CakeML to Proof Checking, and Back AgainInvited Talk ML Family Workshop Yong Kiam Tan Institute for Infocomm Research, A*STAR | ||
13:45 - 15:30 | Macros and Denotational SemanticsScheme at Peony NW Chair(s): Paulette Koronkevich University of British Columbia | ||
13:45 25mTalk | Rewriting Macros on the Fly: A Modular Approach to Administrative Reduction During Expansion Scheme Paul Downen University of Massachusetts at Lowell | ||
14:10 25mTalk | Fast and Extensible Hybrid Embeddings with Micros Scheme | ||
14:35 20mTalk | Hygienic Macros via Staged Environment Machines (Position Paper) Scheme Yuito Murase Kyoto University, Japan | ||
14:55 25mTalk | Checking a Denotational Semantics of Scheme in Agda Scheme Peter D. Mosses Swansea University and Delft University of Technology | ||
13:45 - 15:30 | |||
13:45 40mShort-paper | The Proof Must Go On: Formal Methods in the Theater of Secure Software Development of the Future SPLASH Onward! Essays Charles Averill University of Texas at Dallas DOI Pre-print | ||
14:25 40mTalk | The Unix Executable as a Smalltalk Method SPLASH Onward! Essays Joel Jakubovic Charles University in Prague | ||
13:45 - 15:30 | |||
13:45 70mKeynote | Join points in practiceKeynote Haskell Simon Peyton Jones Epic Games | ||
15:00 30mResearch paper | Automatic C bindings generation for Haskell Haskell Travis Cardwell Well-Typed LLP, Sam Derbyshire Well-Typed LLP, Edsko de Vries Well-Typed LLP, Dominik Schrempf Well-Typed LLP | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | |||
16:00 15mTalk | An Empirical Study of Bugs in the rustc Compiler SPLASH OOPSLA Zixi Liu Nanjing University, Yang Feng Nanjing University, Yunbo Ni The Chinese University of Hong Kong, Shaohua Li The Chinese University of Hong Kong, Xizhe Yin Nanjing University, Qingkai Shi Nanjing University, Baowen Xu Nanjing University, Zhendong Su ETH Zurich | ||
16:15 15mTalk | DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure SPLASH OOPSLA Chenyao Suo Tianjin University, Jianrong Wang Tianjin University, Yongjia Wang College of Intelligence and Computing, Tianjin University, Jiajun Jiang Tianjin University, Qingchao Shen Tianjin University, Junjie Chen Tianjin University | ||
16:30 15mTalk | GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler SPLASH OOPSLA Damitha Lenadora University of Illinois at Urbana-Champaign, Nikhil Jayakumar University of Texas at Austin, Chamika Sudusinghe University of Illinois at Urbana-Champaign, Charith Mendis University of Illinois at Urbana-Champaign | ||
16:45 15mTalk | Non-interference Preserving Optimising Compilation SPLASH OOPSLA Julian Rosemann Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus, Deepak Garg MPI-SWS | ||
17:00 15mTalk | Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations SPLASH OOPSLA Yi Zhang Nanjing University, Yu Wang Nanjing University, Linzhang Wang Nanjing University, Ke Wang Peking University | ||
17:15 15mTalk | Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits SPLASH OOPSLA Junrui Liu University of California, Santa Barbara, Jiaxin Song University of Illinois at Urbana-Champaign, Yanning Chen University of Toronto, Hanzhi Liu University of California, Santa Barbara & Riema Labs, Hongbo Wen University of California, Santa Barbara & Riema Labs, Luke Pearson Polychain Capital, Yanju Chen University of California, San Diego, Yu Feng University of California at Santa Barbara | ||
16:00 - 17:30 | |||
16:00 15mTalk | Compressed and Parallelized Structured Tensor Algebra SPLASH OOPSLA Mahdi Ghorbani University of Edinburgh, Emilien Bauer , Tobias Grosser University of Cambridge, Amir Shaikhha University of Edinburgh | ||
16:15 15mTalk | Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern SPLASH OOPSLA Patrick Redmond University of California, Santa Cruz, Jonathan Castello University of California, Santa Cruz, Jose Calderon Galois, Inc., Lindsey Kuper University of California, Santa Cruz Pre-print | ||
16:30 15mTalk | HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition SPLASH OOPSLA | ||
16:45 15mTalk | Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness SPLASH OOPSLA Dongjae Lee Massachusetts Institute of Technology, Janggun Lee KAIST, Taeyoung Yoon Seoul National University, Minki Cho Seoul National University, Jeehoon Kang FuriosaAI, Chung-Kil Hur Seoul National University | ||
17:00 15mTalk | Opportunistically Parallel Lambda Calculus SPLASH OOPSLA Stephen Mell University of Pennsylvania, Konstantinos Kallas University of California, Los Angeles, Steve Zdancewic University of Pennsylvania, Osbert Bastani University of Pennsylvania | ||
17:15 15mTalk | Soundness of Predictive Concurrency Analyses SPLASH OOPSLA Shuyang Liu , Doug Lea State University of New York (SUNY) Oswego, Jens Palsberg University of California, Los Angeles (UCLA) | ||
16:00 - 17:30 | |||
16:00 30mTalk | Implicit modules, a middle step towards modular implicitsRemote ML Family Workshop | ||
16:30 30mTalk | A Core Language for Extended Pattern Matching and Binding Boolean Expressions ML Family Workshop | ||
17:00 30mTalk | Compositional Deep Argument Flattening ML Family Workshop Martin Elsman University of Copenhagen Pre-print | ||
16:00 - 17:30 | Report, Lightning Talks, and KeynoteScheme at Peony NW Chair(s): Youyou Cong Institute of Science Tokyo, Olivier Danvy Yale-NUS College and School of Computing, Singapore | ||
16:00 20mTalk | Scheme Reports at Fifty: Where do we go from here?Remote Scheme | ||
16:20 10mTalk | Brack: A Verified Compiler for Scheme via CakeML (Lightning Talk) Scheme Pascal Lasnier University of Cambridge, Jeremy Yallop University of Cambridge, Magnus O. Myreen Chalmers University of Technology File Attached | ||
16:30 10mTalk | miniDusa: An Extensible Finite-Choice Logic Programming Language (Lightning Talk) Scheme File Attached | ||
16:40 50mKeynote | Scheme and New Frontiers for Language Design Scheme Michael D. Adams National University of Singapore | ||
16:00 - 17:30 | |||
16:00 30mTalk | Semantics-preserving Transformation of Context-free Grammars into LL(1) Form SPLASH Onward! Papers | ||
16:30 30mTalk | An Argument for the Practicality of Entity Component Systems as the Primary Data Structure for an Interpreter or Compiler SPLASH Onward! Papers | ||
17:00 30mTalk | TideScript: A Domain Specific Language for Peptide Chemistry SPLASH Onward! Papers Nicholas Morris University of Glasgow, Blair Archibald University of Glasgow, S Hessam M Mehr University of Glasgow | ||
16:00 - 17:30 | |||
16:00 30mResearch paper | A Clash Course in Solving Sudoku (Functional Pearl) Haskell Gergő Érdi Standard Chartered Bank Pre-print | ||
16:30 30mResearch paper | Staging Automatic Differentiation with Fusion Haskell | ||
17:00 30mTalk | Talk I Haskell | ||
18:00 - 20:00 | |||
18:00 2hSocial Event | SPLASH SRC Poster Session SPLASH Student Research Competition | ||
18:00 - 20:00 | |||
18:00 2hPoster | Toward Automated Verification of Static Analysis Results of Android Applications SPLASH Posters | ||
18:00 2hPoster | Existentialize your Generics SPLASH Posters | ||
18:00 2hPoster | View Types in Rust SPLASH Posters Sasha Pak The Australian National University, Richard Willie National University of Singapore, Umang Mathur National University of Singapore, Singapore, Fabian Muehlboeck Australian National University, Alex Potanin Australian National University | ||
18:00 2hPoster | Simplifying Lifter-generated Emulation Style LLVM IR for Analysis Suitability SPLASH Posters | ||
18:00 2hPoster | Verifying Extract Method Refactoring in Rust SPLASH Posters Matthew Britton The Australian National University, Alex Potanin Australian National University, Sasha Pak The Australian National University | ||
18:00 2hPoster | Reproducibility Debt in Scientific Software SPLASH Posters Zara Hassan Australian National University, Christoph Treude Singapore Management University, Graham Williams Australian National University, Michael Norrish Australian National University, Alex Potanin Australian National University | ||
18:00 2hPoster | Lemma Discovery for Inductive Equational Proofs via Recursive Function Synthesis SPLASH Posters | ||
18:00 2hPoster | Logically Qualified Types for Scala SPLASH Posters | ||
18:00 2hPoster | Incremental and Unbounded Loop Analysis SPLASH Posters | ||
18:00 2hPoster | Type Checking for Python Using Intersection Types SPLASH Posters | ||
18:00 2hPoster | Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can do Better SPLASH Posters Aaron Bembenek The University of Melbourne | ||
Fri 17 OctDisplayed time zone: Perth change
Fri 17 Oct
Displayed time zone: Perth change
09:00 - 10:00 | |||
09:00 60mKeynote | The Quest Toward that Perfect Compiler SPLASH Keynotes | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:15 | |||
10:30 15mTalk | Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis SPLASH OOPSLA Yuchen Ji ShanghaiTech University, Ting Dai IBM Research, Zhichao Zhou School of Information Science and Technology, ShanghaiTech University, Yutian Tang University of Glasgow, United Kingdom, Jingzhu He ShanghaiTech University | ||
10:45 15mTalk | A Sound Static Analysis Approach to I/O API Migration SPLASH OOPSLA Shangyu Li The Hong Kong University of Science and Technology, Zhaoyang Zhang The Hong Kong University of Science and Technology, Sizhe Zhong The Hong Kong University of Science and Technology, Diyu Zhou Peking University, Jiasi Shen The Hong Kong University of Science and Technology | ||
11:00 15mTalk | Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials SPLASH OOPSLA Pre-print | ||
11:15 15mTalk | Denotational Foundations for Expected Cost Analysis SPLASH OOPSLA Pedro Henrique Azevedo de Amorim Cornell University | ||
11:30 15mTalk | IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis SPLASH OOPSLA | ||
11:45 15mTalk | Revealing Sources of (Memory) Errors via Backward Analysis SPLASH OOPSLA Flavio Ascari University of Pisa, Roberto Bruni University of Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy, Francesco Logozzo Meta | ||
12:00 15mTalk | Two Approaches to Fast Bytecode Frontend for Static Analysis SPLASH OOPSLA Chenxi Li Nanjing University, China, Haoran Lin Nanjing University, China, Tian Tan Nanjing University, Yue Li Nanjing University | ||
10:30 - 12:15 | |||
10:30 15mTalk | Efficient Algorithms for the Uniform Tokenization Problem SPLASH OOPSLA | ||
10:45 15mTalk | REPTILE: Performant Tiling of Recurrences SPLASH OOPSLA Muhammad Usman Tariq Stanford University, Shiv Sundram Stanford University, Fredrik Kjolstad Stanford University | ||
11:00 15mTalk | SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention SPLASH OOPSLA Ahan Gupta University of Illinois at Urbana-Champaign, Yueming Yuan University of Illinois Urbana-Champaign, Devansh Jain University of Illinois at Urbana-Champaign, Yuhao Ge University of Illinois at Urbana-Champaign, David Aponte Microsoft, Yanqi Zhou Google, Charith Mendis University of Illinois at Urbana-Champaign | ||
11:15 15mTalk | Statically Analyzing the Dataflow of R Programs SPLASH OOPSLA | ||
11:30 15mTalk | Static Inference of Regular Grammars for Ad Hoc Parsers SPLASH OOPSLA Pre-print | ||
11:45 15mTalk | Syntactic Completions with Material Obligations SPLASH OOPSLA David Moon University of Michigan, Andrew Blinn University of Michigan, Thomas J. Porter University of Michigan, Cyrus Omar University of Michigan DOI Pre-print | ||
10:30 - 12:15 | |||
10:30 - 12:15 | |||
10:30 15mTalk | Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification SPLASH OOPSLA Chenghang Shi SKLP, Institute of Computing Technology, CAS, Dongjie He Chongqing University, China, Haofeng Li SKLP, Institute of Computing Technology, CAS, Jie Lu SKLP, Institute of Computing Technology, CAS, China, Lian Li Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Jingling Xue University of New South Wales | ||
10:45 15mTalk | Flexible and Expressive Typed Path Patterns for GQL SPLASH OOPSLA Wenjia Ye National University of Singapore, Matías Toro University of Chile, Tomás Diaz University of Chile, Bruno C. d. S. Oliveira University of Hong Kong, Manuel Rigger National University of Singapore, Claudio Gutierrez DCC, Universidad de Chile & IMFD, Domagoj Vrgoč Pontificia Universidad Católica de Chile & IMFD Chile | ||
11:00 15mTalk | Quantified Underapproximation via Labeled Bunches SPLASH OOPSLA Lang Liu Illinois Institute of Technology, Farzaneh Derakhshan Illinois Institute of Technology, Limin Jia Carnegie Mellon University, Gabriel A. Moreno Carnegie Mellon University Software Engineering Institute, Mark Klein Carnegie Mellon University | ||
11:15 15mTalk | HpC: A Calculus for Hybrid and Mobile Systems SPLASH OOPSLA Xiong Xu Institute of Software, Chinese Academy of Sciences, Jean-Pierre Talpin INRIA, France, Shuling Wang Institute of Software, Chinese Academy of Sciences, Bohua Zhan Huawei Technologies Co., Ltd., Xinxin Liu Institute of software, Chinese academy of sciences, Naijun Zhan Peking University | ||
11:30 15mTalk | Notions of Stack-manipulating Computation and Relative Monads SPLASH OOPSLA Yuchen Jiang University of Michigan, Runze Xue University of Michigan; University of Cambridge; Indiana University, Max S. New University of Michigan | ||
11:45 15mTalk | Peepco: Batch-Based Consistency Optimization SPLASH OOPSLA Ivan Kuraj Massachusetts Institute of Technology, Jack Feser Basis, Nadia Polikarpova University of California at San Diego, Armando Solar-Lezama Massachusetts Institute of Technology | ||
10:30 - 12:15 | |||
10:30 30mTalk | Taming the Flat Float Array Optimization: Tracking Separability in the Type System OCaml | ||
11:00 30mTalk | A Mechanically Verified Garbage Collector for OCaml OCaml Sheera Shamsu IIT Madras, Dipesh Kafle NIT Trichy, Tiruchirappalli, India, Dhruv Maroo IIT Madras, Chennai, Kartik Nagar IIT Madras, Karthikeyan Bhargavan Cryspen, France, KC Sivaramakrishnan IIT Madras and Tarides | ||
11:30 30mTalk | OCaml Package Management with (only!) Dune OCaml | ||
10:30 - 12:15 | |||
10:30 26mTalk | Beyond Cons: Purely Relational Data Structures miniKanren Rafaello Sanna Harvard University, William E. Byrd University of Alabama at Birmingham, Nada Amin Harvard University | ||
10:56 26mTalk | Committing to the bit: Relational programming with tensors and SAT solving miniKanren Dmitri Volkov Indiana University, Yafei Yang Indiana University, Chung-chieh Shan Indiana University | ||
11:22 26mTalk | An Empirical Study of Rational Tree Unification for miniKanren miniKanren Eridan Domoratskiy Saint-Petersburg State University, Dmitrii Kosarev , Dmitri Boulytchev Saint Petersburg State University | ||
11:48 26mTalk | concurrentKanren: miniKanren for parallel execution miniKanren Sjoerd Dost None | ||
10:30 - 12:15 | |||
10:30 30mTalk | What You See Is What It Does: A Structural Pattern for Legible Software SPLASH Onward! Papers | ||
11:00 30mTalk | Literate Tracing SPLASH Onward! Papers Matthew Sotoudeh Stanford University Pre-print Media Attached | ||
11:30 30mTalk | ScooPy: Enhancing Program Synthesis with Nested Example Specifications SPLASH Onward! Papers | ||
10:30 - 12:15 | |||
10:30 30mResearch paper | Rebound: Efficient, expressive, and well-scoped binding Haskell Pre-print | ||
11:00 30mResearch paper | Total Type Classes Haskell | ||
11:30 40mTalk | Talk II Haskell | ||
12:15 - 13:45 | |||
12:15 90mLunch | Lunch Catering | ||
13:45 - 15:30 | |||
13:45 15mTalk | An Empirical Evaluation of Property-Based Testing in Python SPLASH OOPSLA | ||
14:00 15mTalk | Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM SPLASH OOPSLA Ao Li Carnegie Mellon University, Byeongjee Kang Carnegie Mellon University, Vasudev Vikram Carnegie Mellon University, Isabella Laybourn Carnegie Mellon University, Samvid Dharanikota Efficient Computer, Shrey Tiwari Carnegie Mellon University, Rohan Padhye Carnegie Mellon University Pre-print Media Attached | ||
14:15 15mTalk | Fuzzing C++ Compilers via Type-Driven Mutation SPLASH OOPSLA Bo Wang Beijing Jiaotong University, Chong Chen Beijing Jiaotong University, Ming Deng Beijing Jiaotong University, Junjie Chen Tianjin University, Xing Zhang Peking University, Youfang Lin Beijing Jiaotong University, Dan Hao Peking University, Jun Sun Singapore Management University | ||
14:30 15mTalk | Interleaving Large Language Models for Compiler Testing SPLASH OOPSLA | ||
14:45 15mTalk | Model-guided Fuzzing of Distributed Systems SPLASH OOPSLA Ege Berkay Gulcan Delft University of Technology, Burcu Kulahcioglu Ozkan Delft University of Technology, Rupak Majumdar MPI-SWS, Srinidhi Nagendra IRIF, Chennai Mathematical Institute | ||
15:00 15mTalk | Tuning Random Generators: Property-Based Testing as Probabilistic Programming SPLASH OOPSLA Ryan Tjoa University of Washington; Jane Street, Poorva Garg University of California, Los Angeles, Harrison Goldstein University at Buffalo, the State University of New York at Buffalo, Todd Millstein University of California at Los Angeles, Benjamin C. Pierce University of Pennsylvania, Guy Van den Broeck University of California at Los Angeles Pre-print | ||
15:15 15mTalk | Understanding and Improving Flaky Test Classification SPLASH OOPSLA Shanto Rahman The University of Texas at Austin, Saikat Dutta Cornell University, August Shi The University of Texas at Austin | ||
13:45 - 15:30 | |||
13:45 15mTalk | A complete formal semantics of eBPF instruction set architecture for Solana SPLASH OOPSLA Shenghao Yuan Zhejiang University, Zhuoruo Zhang Zhejiang University, Jiayi Lu Zhejiang University, David Sanan Singapore Institute of Technology, Rui Chang Zhejiang University, Yongwang Zhao Zhejiang University | ||
14:00 15mTalk | Adequacy for Algebraic Effects Revisited SPLASH OOPSLA Alex Kavvos University of Bristol | ||
14:15 15mTalk | A Mechanized Semantics for Dataflow Circuits SPLASH OOPSLA Tony Law Univ Rennes, Inria, CNRS, IRISA, Delphine Demange Univ Rennes, Inria, CNRS, IRISA, Sandrine Blazy University of Rennes | ||
14:30 15mTalk | Dynamic Wind for Effect Handlers SPLASH OOPSLA David Voigt University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen Pre-print | ||
14:45 15mTalk | React-tRace: A Semantics for Understanding React Hooks SPLASH OOPSLA Jay Lee Seoul National University, Joongwon Ahn Seoul National University, Kwangkeun Yi Seoul National University Pre-print | ||
15:00 15mTalk | Semantics of Sets of Programs SPLASH OOPSLA Jinwoo Kim University of Wisconsin-Madison; Seoul National University, Shaan Nagy University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison, Loris D'Antoni University of California at San Diego | ||
15:15 15mTalk | Zero-Overhead Lexical Effect Handlers SPLASH OOPSLA Cong Ma University of Waterloo, Zhaoyi Ge University of Waterloo, Max Jung University of Waterloo, Yizhou Zhang University of Waterloo | ||
13:45 - 15:30 | |||
13:45 30mTalk | How the OCaml Community Established Its Code of ConductInvited Talk OCaml Sudha Parimala Tarides | ||
14:15 30mTalk | Embedding WebAssembly in OCaml for Safe Program Construction OCaml Hunter DeMeyer University of Illinois Urbana-Champaign | ||
14:45 30mTalk | smaws: An AWS SDK for OCaml OCaml Chris Armstrong None | ||
13:45 - 15:30 | |||
13:45 13mTalk | Designing Walrus: Relational Programming with Rich Types, On-Demand Laziness, and Structured Traces miniKanren Santiago Cuellar Princeton, Naomi Spargo Galois, Inc., Jonathan Daugherty Galois, Inc., David Darais Galois | ||
13:58 13mTalk | The CoCompiler: DSL Lifting via Relational Compilation miniKanren Naomi Spargo Galois, Inc., Santiago Cuellar Princeton, Jonathan Daugherty Galois, Inc., Chris Phifer Galois, David Darais Galois | ||
14:11 26mTalk | Typed Embedding of miniKanren for Functional Conversion miniKanren Igor Engel JetBrains Research; Constructor University Bremen, Ekaterina Verbitskaia JetBrains Research; Constructor University Bremen | ||
14:37 26mTalk | Fair intersection of seekable iterators miniKanren Michael Arntzenius None | ||
15:03 26mTalk | Encoding Numeric Computations and Infusing Heuristic Knowledge Using Integrity Constraints in stableKanren miniKanren | ||
13:45 - 15:30 | |||
13:45 40mTalk | Carving Text at Its Joints: A New Perspective on Writing and Computers SPLASH Onward! Essays Kevin Graaf Independent Researcher | ||
14:25 40mTalk | Let's Take Esoteric Programming Languages Seriously SPLASH Onward! Essays DOI Pre-print | ||
13:45 - 15:30 | |||
13:45 70mKeynote | A Tale of Two Lambdas: A Haskeller's Journey into OCamlKeynote Haskell Richard A. Eisenberg Jane Street | ||
15:00 30mResearch paper | Plinth: A Plugin-Powered Language Built on Haskell (Experience Report) Haskell Ziyang Liu Input Output, USA, Kenneth MacKenzie Input Output, United Kingdom, Roman Kireev Input Output, United Kingdom, Michael Peyton Jones Input Output, United Kingdom, Philip Wadler University of Edinburgh, Manuel M. T. Chakravarty IOHK | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | |||
16:00 15mTalk | A Flow-Sensitive Refinement Type System for Verifying eBPF Programs SPLASH OOPSLA Ameer Hamza Florida State University, Lucas Zavalia Florida State University Tallahassee, Arie Gurfinkel University of Waterloo, Jorge A. Navas Certora, Grigory Fedyukovich Florida State University | ||
16:15 15mTalk | Automatically Verifying Replication-aware Linearizability SPLASH OOPSLA Vimala Soundarapandian IIT Madras, Kartik Nagar IIT Madras, Aseem Rastogi Microsoft Research, KC Sivaramakrishnan IIT Madras and Tarides | ||
16:30 15mTalk | On the Impact of Formal Verification on Software Development SPLASH OOPSLA Eric Mugnier University of California San Diego, Zhou Yuanyuan UCSD, Ranjit Jhala University of California at San Diego, Michael Coblenz University of California, San Diego | ||
16:45 15mTalk | Towards Verifying Crash Consistency SPLASH OOPSLA Keonho Lee University of California, Irvine, Conan Truong University of California, Irvine, Brian Demsky University of California at Irvine | ||
17:00 15mTalk | TraceLinking Implementations with their Verified Designs SPLASH OOPSLA Pre-print | ||
17:15 15mTalk | Pyrosome: Verified Compilation for Modular Metatheory SPLASH OOPSLA | ||
16:00 - 17:30 | |||
16:00 15mTalk | Bennet: Randomized Specification Testing for Heap-Manipulating Programs SPLASH OOPSLA | ||
16:15 15mTalk | DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance SPLASH OOPSLA Chenyang Ma Nanjing University of Science and Technology, Wei Song Nanjing University of Science and Technology, Jeff Huang Texas A&M University | ||
16:30 15mTalk | Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines SPLASH OOPSLA Wai Kin Wong Hong Kong University of Science and Technology, Dongwei Xiao Hong Kong University of Science and Technology, Cheuk Tung LAI VX Research Limited, Yiteng Peng Hong Kong University of Science and Technology, Daoyuan Wu Lingnan University, Shuai Wang Hong Kong University of Science and Technology | ||
16:45 15mTalk | Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing SPLASH OOPSLA Qiong Feng Nanjing University of Science and Technology, Xiaotian Ma Nanjing University of Science and Technology, Ziyuan Feng Nanjing University of Science and Technology, Marat Akhin JetBrains, Wei Song Nanjing University of Science and Technology, Peng Liang Wuhan University, China | ||
17:00 15mTalk | Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools SPLASH OOPSLA | ||
16:00 - 17:30 | |||
16:00 15mTalk | Debugging WebAssembly? Put some Whamm on it! SPLASH OOPSLA Elizabeth Gilbert Carnegie Mellon University, Matthew Schneider Carnegie Mellon University, Zixi An , Suhas Thalanki Carnegie Mellon University, Wavid Bowman University of Florida, Alexander Bai New York University, Ben L. Titzer Carnegie Mellon University, Heather Miller Carnegie Mellon University and Two Sigma | ||
16:15 15mTalk | MIO: Multiverse Debugging in the face of Input/Output SPLASH OOPSLA Tom Lauwaerts Universiteit Gent, Belgium, Maarten Steevens Ghent University, Belgium, Christophe Scholliers Universiteit Gent, Belgium | ||
16:30 15mTalk | PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer SPLASH OOPSLA Linna Xie Nanjing University, Zhong Li Nanjing University, Yu Pei Hong Kong Polytechnic University, Zhongzhen Wen Nanjing University, Kui Liu Huawei, Tian Zhang Nanjing University, Xuandong Li Nanjing University | ||
16:45 15mTalk | Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison SPLASH OOPSLA Ruixin Wang Purdue University, Zhongkai Zhao National University of Singapore, Le Fang Purdue University, Nan Jiang Purdue University, Yiling Lou Fudan University, Lin Tan Purdue University, Tianyi Zhang Purdue University | ||
17:00 15mTalk | Translation Validation for LLVM's AArch64 Backend SPLASH OOPSLA Ryan Berger Nvidia, Mitch Briles University of Utah, Nader Boushehrinejad Moradi University of Utah, Nicholas Coughlin Defence Science and Technology Group, Australia, Kait Lam Defence Science and Technology Group / School of EECS, University of Queensland, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon, Stefan Mada University of Utah, Tanmay Tirpankar University of Utah, John Regehr University of Utah | ||
17:15 15mTalk | Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation SPLASH OOPSLA Maolin Sun Nanjing University, Yibiao Yang Nanjing University, Jiangchang Wu State Key Laboratory for Novel Software Technology, Nanjing University, Yuming Zhou Nanjing University | ||
16:00 - 17:30 | |||
16:00 15mTalk | A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo) SPLASH OOPSLA Kartik Chandra MIT, Tony Chen MIT, Joshua B. Tenenbaum Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology | ||
16:15 15mTalk | ROSpec: A Domain-Specific Language for ROS-based Robot Software SPLASH OOPSLA Paulo Canelas Carnegie Mellon University, Bradley Schmerl School of Computer Science, Carnegie Mellon University, Alcides Fonseca LASIGE; University of Lisbon, Christopher Steven Timperley Carnegie Mellon University DOI Pre-print Media Attached | ||
16:30 15mTalk | Large Language Model powered Symbolic Execution SPLASH OOPSLA Yihe Li National University of Singapore, Ruijie Meng National University of Singapore, Singapore, Gregory J. Duck National University of Singapore | ||
16:45 15mTalk | Multi-Language Probabilistic Programming SPLASH OOPSLA Sam Stites Northeastern University, John Li Northeastern University, Steven Holtzen Northeastern University | ||
17:00 15mTalk | Polymorphic Records for Dynamic Languages SPLASH OOPSLA | ||
16:00 - 17:30 | |||
16:00 30mTalk | Toward a More Secure OCaml EcosystemInvited Talk OCaml Maksim Grankin Bloomberg | ||
16:30 30mTalk | Three steps for OCaml to crest the AI humps OCaml Sadiq Jaffer University of Cambridge, Anil Madhavapeddy University of Cambridge, UK, Ryan Gibb University of Cambridge, Jonathan Ludlam University of Cambridge | ||
17:00 30mTalk | A New Era of OCaml Editing: Powered by Merlin, Delivered via LSP OCaml | ||
16:00 - 17:30 | |||
16:00 26mTalk | Computational Exploration of Finite Semigroupoids miniKanren | ||
16:26 26mTalk | Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics miniKanren | ||
16:52 38mPanel | Frontiers: What's next for miniKanren and Relational Programming? miniKanren Jason Hemann Seton Hall University | ||
16:00 - 17:30 | |||
16:00 30mTalk | Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities SPLASH Onward! Papers Andrew Fawcett Victoria University of Wellington, James Noble Independent. Wellington, NZ, Michael Homer Victoria University of Wellington | ||
16:30 30mTalk | Synchronous Programming for Kids: A Manifesto SPLASH Onward! Papers Jean Pichon-Pharabod Aarhus University | ||
17:30 - 18:15 | |||
17:30 15mAwards | SPLASH Awards SPLASH OOPSLA S: Alex Potanin Australian National University, S: Charles Zhang The Hong Kong University of Science and Technology | ||
Sat 18 OctDisplayed time zone: Perth change
Sat 18 Oct
Displayed time zone: Perth change
09:00 - 10:00 | |||
09:00 60mKeynote | Software Stacks for Confidential Computing Hardware SPLASH Keynotes | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:15 | |||
10:30 15mTalk | Borrowing From Session Types SPLASH OOPSLA Hannes Saffrich University of Freiburg, Janek Spaderna University of Freiburg, Germany, Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos LASIGE, University of Lisbon | ||
10:45 15mTalk | Modal Effect Types SPLASH OOPSLA Wenhao Tang The University of Edinburgh, Leo White Jane Street, Stephen Dolan Jane Street, Daniel Hillerström Category Labs and The University of Edinburgh, Sam Lindley The University of Edinburgh, Anton Lorenzen University of Edinburgh | ||
11:00 15mTalk | On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs SPLASH OOPSLA Taro Sekiyama National Institute of Informatics, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Hiroshi Unno Tohoku University | ||
11:15 15mTalk | Proof Repair across Quotient Type Equivalences SPLASH OOPSLA Cosmo Viola University of Illinois Urbana-Champaign, Max Fan Cornell University, Talia Lily Ringer University of Illinois Urbana-Champaign | ||
11:30 15mTalk | Structural Information Flow: A Fresh Look at Types for Non-Interference SPLASH OOPSLA Hemant Gouni Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA, Jonathan Aldrich Carnegie Mellon University Pre-print | ||
11:45 15mTalk | The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking SPLASH OOPSLA Pre-print | ||
12:00 15mTalk | We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators SPLASH OOPSLA Patrick LaFontaine Purdue University, Zhe Zhou Purdue University, Ashish Mishra IIT Hyderabad, Suresh Jagannathan Purdue University, Benjamin Delaware Purdue University | ||
10:30 - 12:15 | |||
10:30 15mTalk | Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations SPLASH OOPSLA Guofeng Cui Rutgers University, Yuning Wang Rutgers University, Wensen Mao Rutgers University, Yuanlin Duan Rutgers University, He Zhu Rutgers University, USA | ||
10:45 15mTalk | API-guided Dataset Synthesis to Finetune Large Code Models SPLASH OOPSLA Li Zongjie Hong Kong University of Science and Technology, Daoyuan Wu Lingnan University, Shuai Wang Hong Kong University of Science and Technology, Zhendong Su ETH Zurich | ||
11:00 15mTalk | Fast Constraint Synthesis for C++ Function Templates SPLASH OOPSLA | ||
11:15 15mTalk | Hambazi: Spatial Coordination Synthesis for Augmented Reality SPLASH OOPSLA Yi-Zhen Tsai University of California, Riverside, Jiasi Chen University of Michigan, Mohsen Lesani University of California at Santa Cruz | ||
11:30 15mTalk | Inductive Synthesis of Inductive Heap Predicates SPLASH OOPSLA | ||
11:45 15mTalk | LOUD: Synthesizing Strongest and Weakest Specifications SPLASH OOPSLA Kanghee Park University of Wisconsin-Madison, Xuanyu Peng University of California, San Diego, Loris D'Antoni University of California at San Diego | ||
12:00 15mTalk | Metamorph: Synthesizing Large Objects from Dafny Specifications SPLASH OOPSLA Aleksandr Fedchin Tufts University, Alexander Bai New York University, Jeffrey S. Foster Tufts University | ||
10:30 - 12:15 | |||
10:30 15mTalk | AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators SPLASH OOPSLA Avner Bensoussan King's College London, Elena Chachkarova Kings College London, Karine Even-Mendoza King’s College London, Sophie Fortz King's College London, Connor Lenihan King's College London | ||
10:45 15mTalk | A Language for Quantifying Quantum Network Behavior SPLASH OOPSLA Anita Buckley USI Lugano, Pavel Chuprikov Télécom Paris, Institut Polytechnique de Paris, Rodrigo Otoni USI Lugano, Robert Soulé Yale University, Robert Rand University of Chicago, Patrick Eugster USI Lugano, Switzerland | ||
11:00 15mTalk | Compositional Quantum Control Flow with Efficient Compilation in Qunity SPLASH OOPSLA Mikhail Mints California Institute of Technology, Finn Voichick University of Maryland, Leonidas Lampropoulos University of Maryland, College Park, Robert Rand University of Chicago | ||
11:15 15mTalk | Dependency-Aware Compilation for Surface Code Quantum Architectures SPLASH OOPSLA Abtin Molavi University of Wisconsin-Madison, Amanda Xu University of Wisconsin-Madison, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison | ||
11:30 15mTalk | QbC: Quantum Correctness by Construction SPLASH OOPSLA | ||
11:45 15mTalk | qblaze: An Efficient and Scalable Sparse Quantum Simulator SPLASH OOPSLA Hristo Venev INSAIT, Sofia University "St. Kliment Ohridski", Thien Udomsrirungruang University of Oxford, Dimitar Dimitrov INSAIT, Sofia University "St. Kliment Ohridski", Timon Gehr ETH Zurich, Martin Vechev ETH Zurich | ||
12:00 15mTalk | Shaking Up Quantum Simulators with Fuzzing and Rigour SPLASH OOPSLA Vasileios Klimis Queen Mary University of London, Karine Even-Mendoza King’s College London, Avner Bensoussan King's College London, Elena Chachkarova Kings College London, Sophie Fortz King's College London, Connor Lenihan King's College London | ||
10:30 - 12:15 | |||
10:30 15mTalk | FO-Complete Program Verification for Heap Logics SPLASH OOPSLA Adithya Murali University of Illinois at Urbana-Champaign, Hrishikesh Balakrishnan University of Illinois Urbana-Champaign, Aaron Councilman Univ of Illinois Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign | ||
10:45 15mTalk | Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back SPLASH OOPSLA Kevin Batz RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University, Francesca Randone Department of Mathematics, Informatics and Geosciences, University of Trieste, Italy, Tobias Winkler RWTH Aachen University | ||
11:00 15mTalk | Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification SPLASH OOPSLA | ||
11:15 15mTalk | KestRel: Relational Verification Using E-Graphs for Program Alignment SPLASH OOPSLA Robert Dickerson Purdue University, Prasita Mukherjee Purdue University, Benjamin Delaware Purdue University | ||
11:30 15mTalk | Laurel: Unblocking Automated Verification with Large Language Models SPLASH OOPSLA 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 | ||
11:45 15mTalk | Scaling Instruction-Selection Verification against Authoritative ISA Semantics SPLASH OOPSLA Michael McLoughlin Carnegie Mellon University, Ashley Sheng Wellesley College, Chris Fallin F5, Bryan Parno Carnegie Mellon University, Fraser Brown CMU, Alexa VanHattum Wellesley College | ||
12:00 15mTalk | Verification of Bit-Flip Attacks against Quantized Neural Networks SPLASH OOPSLA Yedi Zhang National University of Singapore, Lei Huang ShanghaiTech University, Pengfei Gao ByteDance, Fu Song Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software Technology, Jun Sun Singapore Management University, Jin Song Dong National University of Singapore | ||
10:30 - 12:15 | |||
10:30 35mTalk | In the Specifications We Pursue Sponsor Invited Talks Zhendong Su ETH Zurich | ||
11:05 35mTalk | To be announced Sponsor Invited Talks Xinyu Feng Nanjing University & Huawei | ||
11:40 35mTalk | Enhancing Software Engineering with Large Language Models: Insights, Challenges, and Future Directions Sponsor Invited Talks Xin Xia Zhejiang University | ||
10:30 - 12:15 | |||
10:30 30mTalk | X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering SPLASH Onward! Papers Maximilian Kodetzki Karlsruhe Institute of Technology, Tabea Bordis Karlsruhe Institute of Technology, Alex Potanin Australian National University, Ina Schaefer KIT | ||
11:00 40mTalk | Gauguin, Descartes, Bayes: A Diurnal Golem's Brain SPLASH Onward! Essays Kartik Chandra MIT, Amanda Liu Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology, Joshua B. Tenenbaum Massachusetts Institute of Technology | ||
11:40 10mTalk | Closing SPLASH Onward! Papers | ||
10:30 - 12:15 | |||
10:30 65mTalk | The Saga of Multicore OCaml REBASE | ||
11:40 35mTalk | From Facts to Theories: Deductive Databases with Mangle Datalog REBASE Burak Emir Google | ||
12:15 - 13:45 | |||
12:15 90mLunch | Lunch Catering | ||
13:45 - 15:30 | |||
13:45 15mTalk | Compositional Symbolic Execution for the Next 700 Memory Models SPLASH OOPSLA Andreas Lööw Imperial College London, Seung Hoon Park Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Opale Sjöstedt Imperial College London, Philippa Gardner Imperial College London Pre-print | ||
14:00 15mTalk | Destination calculus: A linear λ-calculus for purely functional memory writes SPLASH OOPSLA | ||
14:15 15mTalk | Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown SPLASH OOPSLA | ||
14:30 15mTalk | HeapBuffers: Why not just using a binary serialization format for your managed memory? SPLASH OOPSLA Daniele Bonetta VU Amsterdam, Júnior Löff Università della Svizzera italiana, Matteo Basso Università della Svizzera italiana (USI), Walter Binder USI Lugano | ||
14:45 15mTalk | im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach SPLASH OOPSLA Fei Chen German Research Center for Artificial Intelligence (DFKI), Saarland University, Sunita Saha German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany, Manuela Schuler German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany; Saarland University, Saarbrücken, Germany, Philipp Slusallek DFKI, Germany, Tim Dahmen Aalen University, Aalen, Germany; German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany | ||
15:00 15mTalk | SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races SPLASH OOPSLA Reese Levine , Ashley Lee University of California, Santa Cruz, Neha Abbas University of California, Santa Cruz, Kyle Little University of Utah, Tyler Sorensen Microsoft Research and University of California at Santa Cruz | ||
15:15 15mTalk | Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice SPLASH OOPSLA Jay Richards University of Kent, Daniel Wright University of Surrey, Simon Cooksey , Mark Batty University of Kent | ||
13:45 - 15:30 | |||
13:45 15mTalk | Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis SPLASH OOPSLA Guanlin Chen Peking University, Ruyi Ji Peking University, Shuhao Zhang Peking University, Yingfei Xiong Peking University | ||
14:00 15mTalk | Language-Parametric Reference Synthesis SPLASH OOPSLA Daniel A. A. Pelsmaeker Delft University of Technology, Netherlands, Aron Zwaan Delft University of Technology, Casper Bach University of Southern Denmark, Arjan J. Mooij Zürich University of Applied Sciences | ||
14:15 15mTalk | Multi-Modal Sketch-based Behavior Tree Synthesis SPLASH OOPSLA Wenmeng Zhang College of Computer Science and Technology, National University of Defense Technology, Changsha, China, Zhenbang Chen College of Computer, National University of Defense Technology, Weijiang Hong National University of Defense Technology, Changsha, China | ||
14:30 15mTalk | Synthesizing DSLs for Few-Shot Learning SPLASH OOPSLA Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign | ||
14:45 15mTalk | Synthesizing Implication Lemmas for Interactive Theorem Proving SPLASH OOPSLA Ana Brendel University of California Los Angeles, Aishwarya Sivaraman Meta, Todd Millstein University of California at Los Angeles | ||
15:00 15mTalk | Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers SPLASH OOPSLA Jacob Laurel Georgia Institute of Technology, Ignacio Laguna Lawrence Livermore National Laboratory, Jan Hueckelheim Argonne National Laboratory | ||
15:15 15mTalk | UTFix: Change Aware Unit Test Repairing using LLM SPLASH OOPSLA Shanto Rahman The University of Texas at Austin, Sachit Kuhar Amazon Web Services, Berk Cirisci Amazon Web Services, Pranav Garg AWS, Shiqi Wang AWS AI Labs, Xiaofei Ma AWS AI Labs, Anoop Deoras AWS AI Labs, Baishakhi Ray Columbia University | ||
13:45 - 15:30 | |||
13:45 15mTalk | Adaptive Shielding via Parametric Safety Proofs SPLASH OOPSLA Yao Feng Tsinghua University, Jun Zhu Nankai University, André Platzer Karlsruhe Institute of Technology (KIT), Jonathan Laurent Carnegie Mellon University / Karlsruhe Institute of Technology | ||
14:00 15mTalk | Certified Decision Procedures for Width-Independent Bitvector Predicates SPLASH OOPSLA Siddharth Bhat University of Cambridge, Leo Stefanesco University of Cambridge, Chris Hughes Independent Researcher, Tobias Grosser University of Cambridge | ||
14:15 15mTalk | Checking $\delta$-Satisfiability of Reals with Integrals SPLASH OOPSLA Cody Rivera University of Illinois, Urbana-Champaign, Bishnu Bhusal University of Missouri, Rohit Chadha University of Missouri, A. Prasad Sistla University of Illinois at Chicago, Mahesh Viswanathan University of Illinois at Urbana-Champaign | ||
14:30 15mTalk | Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge SPLASH OOPSLA John C. Kolesar Yale University, Shan Ali Yale University, Timos Antonopoulos Yale University, Ruzica Piskac Yale University | ||
14:45 15mTalk | Incremental Certified Programming SPLASH OOPSLA Tomás Diaz University of Chile, Kenji Maillard Inria – LS2N, Université de Nantes, Nicolas Tabareau Inria, Éric Tanter University of Chile | ||
15:00 15mTalk | Pathological Cases for a Class of Reachability-Based Garbage Collectors SPLASH OOPSLA Matthew Sotoudeh Stanford University Link to publication | ||
15:15 15mTalk | SafeTree: Expressive Tree Policies for Microservices SPLASH OOPSLA | ||
13:45 - 15:30 | |||
13:45 15mTalk | Automated Verification of Soundness of DNN Certifiers SPLASH OOPSLA Avaljot Singh UIUC, Yasmin Chandini Sarita UIUC, Charith Mendis University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research | ||
14:00 15mTalk | Bolt-On Strong Consistency: Specification, Implementation, and Verification SPLASH OOPSLA Nicholas V. Lewchenko University of Colorado Boulder, Gowtham Kaki University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
14:15 15mTalk | Memory-Safety Verification of Open Programs With Angelic Assumptions SPLASH OOPSLA Gourav Takhar Indian Institute of Technology - Kanpur, Baldip Bijlani Indian Institute of Technology Kanpur, Prantik Chatterjee MathWorks, Akash Lal Microsoft Research, Subhajit Roy IIT Kanpur | ||
14:30 15mTalk | Mini-Batch Robustness Verification of Deep Neural Networks SPLASH OOPSLA | ||
14:45 15mTalk | Revamping Verilog Semantics for Foundational Verification SPLASH OOPSLA | ||
15:00 15mTalk | Scalable Equivalence Checking and Verification of Shallow Quantum Circuits SPLASH OOPSLA Nengkun Yu Stony Brook University, USA, Xuan Du Trinh Stony Brook University, Thomas Reps University of Wisconsin-Madison | ||
15:15 15mTalk | Structural temporal logic for mechanized program verification SPLASH OOPSLA Lef Ioannidis University of Pennsylvania, Yannick Zakowski Inria, Steve Zdancewic University of Pennsylvania, Sebastian Angel University of Pennsylvania | ||
13:45 - 15:30 | Programming Language & CompilerSponsor Invited Talks at Peony NE Chair(s): Zhiyang Chen University of Toronto 13:45 - 15:45 (Instead of 15:30), 30 min each talk | ||
13:45 26mTalk | Programming Language Design for GPU Systems Sponsor Invited Talks Michel Steuwer Technische Universität Berlin | ||
14:11 26mTalk | CStar: Unifying Programming and Verification in C Sponsor Invited Talks Di Wang Peking University | ||
14:37 26mTalk | Python, Is It Being Killed by Incremental Improvements? Sponsor Invited Talks Stefan Marr University of Kent | ||
15:03 26mTalk | Supercharge Compiler Engineering with LLMs Sponsor Invited Talks Yongqiang Tian Monash University | ||
13:45 - 15:30 | |||
13:45 65mTalk | TBD REBASE Saam Barati Epic Games | ||
14:55 35mTalk | ZJIT: Building a New JIT Compiler for Ruby REBASE Takashi Kokubun Shopify | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | |||
16:00 15mTalk | Abstract Interpretation of Temporal Safety Effects of Higher Order Programs SPLASH OOPSLA Mihai Nicola Stevens Institute of Technology, Chaitanya Agarwal New York University, Eric Koskinen Stevens Institute of Technology, Thomas Wies New York University | ||
16:15 15mTalk | A Hoare Logic For Symmetry Properties SPLASH OOPSLA | ||
16:30 15mTalk | Efficient Abstract Interpretation via Selective Widening SPLASH OOPSLA | ||
16:45 15mTalk | Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic SPLASH OOPSLA Shushu Wu Shanghai Jiao Tong University, Xiwei Wu Shanghai Jiao Tong University, Qinxiang Cao Shanghai Jiao Tong University | ||
17:00 15mTalk | Structural Abstraction and Refinement for Probabilistic Programs SPLASH OOPSLA Guanyan Li University of Oxford, Juanen Li Beijing Normal University, Zhilei Han Tsinghua University, Peixin Wang East China Normal University, Hongfei Fu Shanghai Jiao Tong University, Fei He Tsinghua University | ||
17:15 15mTalk | Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation SPLASH OOPSLA Wenyu Zhao Australian National University, Stephen M. Blackburn Google; Australian National University, Kathryn S McKinley Google | ||
16:00 - 17:30 | |||
16:00 15mTalk | A Refinement Methodology for Distributed Programs in Rust SPLASH OOPSLA | ||
16:15 15mTalk | AutoVerus: Automated Proof Generation for Rust Code SPLASH OOPSLA Chenyuan Yang University of Illinois Urbana-Champaign, Xuheng Li Columbia University, Md Rakib Hossain Misu University of California Irvine, Jianan Yao University of Toronto, Weidong Cui Microsoft Research, Yeyun Gong Microsoft Research, Chris Hawblitzel Microsoft Research, Shuvendu K. Lahiri Microsoft Research, Jacob R. Lorch Microsoft Research, n.n., Shuai Lu Microsoft Research, Fan Yang Microsoft Research Asia, Ziqiao Zhou Microsoft Research, Shan Lu Microsoft; University of Chicago | ||
16:30 15mTalk | Carapace: Static–Dynamic Information Flow Control in Rust SPLASH OOPSLA Vincent James Beardsley , Chris Xiong Ohio State University, Ada Lamba Ohio State University, Michael D. Bond Ohio State University | ||
16:45 15mTalk | From Linearity to Borrowing SPLASH OOPSLA Andrew Wagner Northeastern University, Olek Gierczak Northeastern University, Brianna Marshall Northeastern University, John Li Northeastern University, Amal Ahmed Northeastern University, USA | ||
17:00 15mTalk | Garbage Collection for Rust: The Finalizer Frontier SPLASH OOPSLA | ||
17:15 15mTalk | Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees SPLASH OOPSLA Zachary Grannan University of British Columbia, Aurel Bílý ETH Zurich, Jonas Fiala ETH Zürich, Jasper Geer University of British Columbia, Markus de Medeiros New York University, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia | ||
16:00 - 17:30 | |||
16:00 15mTalk | (TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs SPLASH OOPSLA DOI | ||
16:15 15mTalk | (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging SPLASH OOPSLA Yaozhu Sun National Institute of Informatics, Xuejing Huang IRIF, Bruno C. d. S. Oliveira University of Hong Kong | ||
16:30 15mTalk | Detecting and explaining (in-)equivalence of context-free grammars SPLASH OOPSLA Marko Schmellenkamp Ruhr University Bochum, Thomas Zeume Ruhr University Bochum, Sven Argo Ruhr University Bochum, Sandra Kiefer University of Oxford, Cedric Siems Ruhr University Bochum, Fynn Stebel Ruhr University Bochum | ||
16:45 15mTalk | Modal Abstractions for Virtualizing Memory Addresses SPLASH OOPSLA | ||
17:00 15mTalk | Agora: Trust Less and Open More in Verification for Confidential Computing SPLASH OOPSLA Hongbo Chen Indiana University Bloomington, Quan Zhou Penn State University, Sen Yang Yale University, Dang Sixuan Duke University, Xing Han The Hong Kong University of Science and Technology, Danfeng Zhang Duke University, Fan Zhang Yale University, XiaoFeng Wang Nanyang Technological University | ||
17:15 15mTalk | QED in Context: An Observation Study of Proof Assistant Users SPLASH OOPSLA Jessica Shi University of Pennsylvania, Cassia Torczon University of Pennsylvania, Harrison Goldstein University at Buffalo, the State University of New York at Buffalo, Benjamin C. Pierce University of Pennsylvania, Andrew Head University of Pennsylvania | ||
16:00 - 17:30 | |||
16:00 15mTalk | Counterexample-Guided Inference of Modular Specifications SPLASH OOPSLA William Hallahan Binghamton, Ranjit Jhala University of California at San Diego, Ruzica Piskac Yale University | ||
16:15 15mTalk | Embedding Quantum Program Verification into Dafny SPLASH OOPSLA Feifei Cheng Iowa State University, Sushen Vangeepuram Iowa State University, Henry Allard Iowa State University, Seyed Mohammad Reza Jafari Iowa State University, Alex Potanin Australian National University, Liyi Li Iowa State University | ||
16:30 15mTalk | Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests SPLASH OOPSLA Kevin Guan Cornell University, Marcelo d'Amorim North Carolina State University, Owolabi Legunsen Cornell University | ||
16:45 15mTalk | Interactive Bit Vector Reasoning using Verified Bitblasting SPLASH OOPSLA Henrik Böving Lean FRO, Siddharth Bhat University of Cambridge, Alex Keizer University of Cambridge, Luisa Cicolini University of Cambridge, Leon Frenot ENS Lyon, Abdalrhman Mohamed Stanford University, Leo Stefanesco University of Cambridge, Harun Khan Stanford University, Josh Clune Carnegie Mellon University, Clark Barrett Stanford University, Tobias Grosser University of Cambridge | ||
17:00 15mTalk | Products of Recursive Programs for Hypersafety Verification SPLASH OOPSLA | ||
16:00 - 17:30 | |||
16:00 30mTalk | Live Program Analysis for Security-Critical Scenarios Sponsor Invited Talks Zhiqiang Zuo Nanjing University | ||
16:30 30mTalk | Automated Approaches for Software Migration and Evolution Sponsor Invited Talks Jiasi Shen The Hong Kong University of Science and Technology | ||
17:00 30mTalk | SQLancer: From Research Prototype to Industry Use Sponsor Invited Talks Manuel Rigger National University of Singapore | ||