ICFP/SPLASH 2025 (series) / SPLASH 2025 (series) /
SPLASH 2025 Program
This is the SPLASH 2025 program - see the full program for ICFP/SPLASH 2025 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 12 OctDisplayed time zone: Perth change
Sun 12 Oct
Displayed time zone: Perth change
09:00 - 10:30 | |||
09:00 90mTalk | WebAssembly Research Tools Tutorial ICFP/SPLASH Tutorials | ||
09:00 - 10:30 | |||
09:00 90mTalk | Testing concurrent code on JVM with Lincheck ICFP/SPLASH Tutorials | ||
09:00 - 10:30 | |||
09:00 90mTalk | Compiling Quantum Circuits ICFP/SPLASH 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 90mTalk | Metaprogramming in Rhombus ICFP/SPLASH Tutorials Pre-print | ||
09:00 - 10:30 | |||
09:00 22mPaper | Type-safe Blazon - Enforcing Pedantry in Heraldic Design FARM Matthew Lutze Aarhus University | ||
09:22 22mDemonstration | How to Score in the Art Racket FARM Jared Gentner None | ||
09:45 22mDemonstration | Rocq N'Roll FARM | ||
10:07 22mDemonstration | I Am Your Co-Pilot FARM Dylan Davis Swinburne University | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break ICFP/SPLASH Catering | ||
11:00 - 12:30 | |||
11:00 90mTalk | WebAssembly Research Tools Tutorial ICFP/SPLASH Tutorials | ||
11:00 - 12:30 | |||
11:00 90mTalk | Testing concurrent code on JVM with Lincheck ICFP/SPLASH Tutorials | ||
11:00 - 12:30 | |||
11:00 90mTalk | Compiling Quantum Circuits ICFP/SPLASH 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 90mTalk | Metaprogramming in Rhombus ICFP/SPLASH Tutorials Pre-print | ||
11:00 - 12:30 | |||
11:00 22mPaper | Cellular Automata as a Model For 1-bit Synthesis in Mitosis FARM Kerry Hagan University of Illinois, Urbana-Champaign | ||
11:22 22mDemonstration | Girard's Paradox as Structure Music FARM | ||
11:45 35mDemonstration | Sonic Earth - An Algorithmic Performance Approach to Real-Time Environmental Sonification FARM Riccardo Mazza APM Saluzzo | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch ICFP/SPLASH Catering | ||
14:00 - 15:30 | |||
14:00 90mTalk | A guided tour through Oxidized OCaml ICFP/SPLASH Tutorials Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street | ||
14:00 - 15:30 | |||
14:00 90mTalk | Concurrent Algorithms under the hood of Kotlin Coroutines ICFP/SPLASH Tutorials Nikita Koval JetBrains | ||
14:00 - 15:30 | |||
14:00 90mTalk | End-to-End Compiler Infrastructure for Emerging Tensor Accelerators ICFP/SPLASH 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 Media Attached | ||
14:00 - 15:30 | |||
14:00 90mTalk | How to secure a distributed database such as OpenRiak with open-source tools ICFP/SPLASH Tutorials | ||
14:00 - 15:07 | |||
14:00 22mDemonstration | Weft—Enabling Tidal on the Web FARM | ||
14:22 22mPaper | Generalizing Turtle Geometry: An Extensible Language for Vector Graphics Drawing FARM | ||
14:44 22mDemonstration | Software-defined declarative synthesizer live-coding in a jupyter notebook FARM Stephen Sherratt Tarides | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break ICFP/SPLASH Catering | ||
16:00 - 17:30 | |||
16:00 90mTalk | A guided tour through Oxidized OCaml ICFP/SPLASH Tutorials Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street | ||
16:00 - 17:30 | |||
16:00 90mTalk | Concurrent Algorithms under the hood of Kotlin Coroutines ICFP/SPLASH Tutorials Nikita Koval JetBrains | ||
16:00 - 17:30 | |||
16:00 90mTalk | End-to-End Compiler Infrastructure for Emerging Tensor Accelerators ICFP/SPLASH 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 Media Attached | ||
16:00 - 17:30 | |||
16:00 90mTalk | How to secure a distributed database such as OpenRiak with open-source tools ICFP/SPLASH Tutorials | ||
19:00 - 21:00 | |||
19:00 2hKeynote | Computers & Music AND Computer Music— An Unlikely [Ongoing] Journey FARM Tae Hong Park Purdue University | ||
19:00 2hSocial Event | Concert: Merzmania FARM | ||
19:00 2hSocial Event | Concert: Mitosis FARM Kerry Hagan University of Illinois, Urbana-Champaign | ||
19:00 2hSocial Event | Concert: Sonic Earth FARM Riccardo Mazza APM Saluzzo | ||
19:00 2hSocial Event | Concert: Girard’s Paradox FARM | ||
19:00 2hSocial Event | Concert: RocqNRoll FARM | ||
19:00 2hSocial Event | Concert: Mirages FARM | ||
19:00 2hSocial Event | Concert: False Awakening on a Mediterranean Island FARM | ||
19:00 2hSocial Event | Concert: The River Oycus FARM | ||
Mon 13 OctDisplayed time zone: Perth change
Mon 13 Oct
Displayed time zone: Perth change
09:00 - 10:10 | Monday ICFP KeynoteICFP Papers / ICFP Keynotes at Orchid Plenary Ballroom Chair(s): Ilya Sergey National University of Singapore | ||
09:00 5mDay opening | Opening ICFP Papers | ||
09:05 5mTalk | JFP Announcement ICFP Papers Derek Dreyer MPI-SWS | ||
09:10 60mKeynote | Functional Programming for Hardware Design ICFP Keynotes Satnam Singh Independent | ||
10:10 - 10:50 | |||
10:10 40mCoffee break | Break ICFP/SPLASH 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 National University of Singapore File Attached | ||
10:50 - 12:05 | Dependent TypesICFP Papers at Orchid Plenary Ballroom Chair(s): Ambrus Kaposi ELTE Eötvös Loránd University, Budapest, Hungary | ||
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 | ImplementationICFP Papers / ICFP JFP First Papers at Orchid West Chair(s): KC Sivaramakrishnan IIT Madras and Tarides | ||
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 | |||
10:50 5mDay opening | Introductions Doctoral Symposium Conrad Watt Nanyang Technological University | ||
11:00 30mTalk | A Multi-Layer Dynamic Security Framework for DeFi Smart Contracts Doctoral Symposium Zhiyang Chen University of Toronto | ||
11:35 30mTalk | Lexical Effect Handler: Fast by Design, Correct by Proof Doctoral Symposium Cong Ma University of Waterloo | ||
12:10 - 13:40 | |||
12:10 90mLunch | Lunch ICFP/SPLASH Catering | ||
13:40 - 15:20 | |||
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 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 30mTalk | How to Synthesize Quantum-Circuit Optimizers Doctoral Symposium Amanda Xu University of Wisconsin-Madison | ||
14:15 30mTalk | Separation Logics for Probability, Concurrency, and Security Doctoral Symposium Kwing Hei Li Aarhus University | ||
14:50 30mTalk | Towards Compiler-Guided Static Analysis Doctoral Symposium Benjamin Mikek Georgia Institute of Technology | ||
15:20 - 16:00 | |||
15:20 40mCoffee break | Break ICFP/SPLASH Catering | ||
16:00 - 17:40 | Abstraction and ProofsSAS at Orchid East Chair(s): Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University | ||
16:00 20mTalk | Relating Distances and Abstractions: An Abstract Interpretation Perspective SAS Marco Campion Sorbonne Université, 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 Software Languages Lab, Vrije Universiteit Brussel, Quentin Stiévenart Université du Québec à Montréal, Coen De Roover Vrije Universiteit Brussel Pre-print | ||
16:00 - 17:40 | AlgorithmsICFP Papers / ICFP JFP First Papers at Orchid Plenary Ballroom Chair(s): Kimball Germane Brigham Young University | ||
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 | SemanticsICFP JFP First Papers / ICFP Papers at Orchid West Chair(s): Henning Urbat Friedrich-Alexander University Erlangen-Nürnberg | ||
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 Nagoya University, Takafumi Saikawa Nagoya University DOI File Attached | ||
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 30mTalk | Practical compositional diagramming Doctoral Symposium Shardul Chiplunkar EPFL | ||
16:30 50mMeeting | [Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award Doctoral Symposium Conrad Watt Nanyang Technological University, Yang Liu Nanyang Technological University, Amal Ahmed Northeastern University, USA, Philip Wadler IOG; University of Edinburgh, Alex Potanin Australian National University | ||
17:20 20mDay closing | First announcement of SIGPLAN's John Vlissides award; Closing Remarks Doctoral Symposium | ||
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 | Tuesday ICFP KeynoteICFP Keynotes at Orchid Plenary Ballroom Chair(s): Peter Thiemann University of Freiburg | ||
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 ICFP/SPLASH 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 | Gradual Typing and SecurityICFP Papers / ICFP JFP First Papers at Orchid Plenary Ballroom Chair(s): Jeremy G. Siek Indiana University | ||
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 | Clever CompilationICFP JFP First Papers / ICFP Papers at Orchid West Chair(s): John Reppy University of Chicago | ||
10:50 25mTalk | Compiling with Generating Functions ICFP Papers DOI | ||
11:15 25mTalk | Correctness Meets Performance: From Agda to FutharkRemote 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 | ||
12:10 - 13:40 | |||
12:10 90mLunch | Lunch ICFP/SPLASH Catering | ||
12:10 - 13:40 | LGBTQ LunchICFP Diversity, Equity, and Inclusion at Peony Dining Room Chair(s): Mae Milano Princeton University | ||
13:40 - 15:20 | |||
13:40 60mKeynote | Towards static analyses and abstract domains for hyperproperties SAS Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - 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 Link to publication Pre-print | ||
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 | Denotational SemanticsICFP Papers at Orchid Plenary Ballroom Chair(s): Alex Kavvos University of Bristol | ||
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:25 | Applications and SRC TalksICFP Papers / ICFP Student Research Competition at Orchid West Chair(s): Martin Elsman University of Copenhagen | ||
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 | ||
15:20 - 16:00 | |||
15:20 40mCoffee break | Break ICFP/SPLASH Catering | ||
16:00 - 18:00 | |||
16:00 15mTalk | ICFP Contest Report ICFP Papers | ||
16:15 20mAwards | Award Ceremony ICFP Papers | ||
16:35 10mAwards | SRC Awards ICFP Student Research Competition | ||
16:45 10mTalk | SIGPLAN AV Report ICFP Papers | ||
16:55 15mMeeting | PC Chair Report ICFP Papers | ||
17:10 10mTalk | General Chair Report ICFP Papers | ||
17:20 10mTalk | ICFP 2026 Announcement ICFP Papers Sam Tobin-Hochstadt Indiana University | ||
Wed 15 OctDisplayed time zone: Perth change
Wed 15 Oct
Displayed time zone: Perth change
09:00 - 10:10 | Wednesday ICFP KeynoteICFP Keynotes at Orchid Plenary Ballroom Chair(s): Dominique Devriese KU Leuven | ||
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 ICFP/SPLASH Catering | ||
10:50 - 12:05 | ParametricityICFP Papers / ICFP JFP First Papers at Orchid Plenary Ballroom Chair(s): Philip Wadler IOG; University of Edinburgh | ||
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 Media Attached | ||
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 | ||
12:10 - 13:40 | |||
12:10 90mLunch | Lunch ICFP/SPLASH Catering | ||
12:10 - 13:40 | |||
13:40 - 15:20 | Separation LogicICFP Papers at Orchid Plenary Ballroom Chair(s): Leo Stefanesco University of Cambridge | ||
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 | Types and SpecificationsICFP Papers / ICFP JFP First Papers at Orchid West Chair(s): Dominic Orchard University of Cambridge; University of Kent | ||
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)Remote 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 | ||
15:20 - 16:00 | |||
15:20 40mCoffee break | Break ICFP/SPLASH Catering | ||
19:00 - 21:00 | Women in PL DinnerICFP Diversity, Equity, and Inclusion Chair(s): Milijana Surbatovich University of Maryland The dinner’s details and logistics are here. | ||
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 ICFP/SPLASH Catering | ||
10:30 - 12:15 | |||
10:30 15mTalk | Unveiling Heisenbugs with Diversified Execution 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 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 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 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 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 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 | CodeOOPSLA at Orchid Plenary Ballroom Chair(s): Jiasi Shen The Hong Kong University of Science and Technology | ||
10:30 15mTalk | ABC: Towards a Universal Code Styler through Model Merging 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 OOPSLA | ||
11:00 15mTalk | Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations 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 OOPSLA | ||
11:30 15mTalk | Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection OOPSLA | ||
11:45 15mTalk | PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns OOPSLA | ||
12:00 15mTalk | Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes OOPSLA Mingyi Li Institute of Computing Technology, CAS, 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 10mTalk | Opening Onward! Papers | ||
10:40 30mTalk | Sharing is Scaring: Linking Cloud File-Sharing to Programming Language Semantics 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 Onward! Papers | ||
11:40 30mTalk | Foundational Design Principles and Patterns for Building Robust & Adaptive GenAI-Native Systems Onward! Papers Frederik Vandeputte Nokia Bell Labs Pre-print | ||
12:15 - 13:45 | |||
12:15 90mLunch | Lunch ICFP/SPLASH Catering | ||
13:45 - 15:30 | |||
13:45 15mTalk | A Unifying Approach to Product Constructions for Quantitative Temporal Inference 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 OOPSLA Shu-Hung You Institute of Information Science, Academia Sinica, Taiwan, Christos Dimoulas Northwestern University, Robert Bruce Findler Northwestern University | ||
14:15 15mTalk | Incremental Bidirectional Typing via Order Maintenance 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 | The Power of Regular Constraint Propagation 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 | ||
14:45 15mTalk | Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles 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 OOPSLA Ruijie Fang University of Texas at Austin, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison DOI Pre-print | ||
13:45 - 15:30 | Onward! Essays 1Onward! Essays / Onward! Papers at Peony SE Chair(s): Michael Coblenz University of California, San Diego | ||
13:45 40mShort-paper | The Proof Must Go On: Formal Methods in the Theater of Secure Software Development of the FutureRemote Onward! Essays Charles Averill University of Texas at Dallas DOI Pre-print | ||
14:25 40mTalk | The Unix Executable as a Smalltalk Method Onward! Essays Joel Jakubovic Charles University in Prague DOI Pre-print | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break ICFP/SPLASH Catering | ||
16:00 - 17:30 | |||
16:00 15mTalk | An Empirical Study of Bugs in the rustc Compiler 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 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 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 OOPSLA Julian Rosemann Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus, Deepak Garg MPI-SWS Link to publication DOI | ||
17:00 15mTalk | Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations 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 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 OOPSLA Mahdi Ghorbani University of Edinburgh, Emilien Bauer University of Edinburgh, 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 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 OOPSLA | ||
16:45 15mTalk | Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness 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 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 OOPSLA Shuyang Liu , Doug Lea State University of New York (SUNY) Oswego, Jens Palsberg University of California, Los Angeles (UCLA) Link to publication | ||
16:00 - 17:30 | Neural NetworkOOPSLA at Orchid West Chair(s): Jiasi Shen The Hong Kong University of Science and Technology | ||
16:00 15mTalk | Convex Hull Approximation for Activation Functions OOPSLA Zhongkui Ma The University of Queensland, Zihan Wang The University of Queensland and CSIRO's Data61, Guangdong Bai University of Queensland | ||
16:15 15mTalk | Cost of Soundness in Mixed-Precision Tuning OOPSLA Pre-print | ||
16:30 15mTalk | Finch: Sparse and Structured Tensor Programming with Control Flow OOPSLA Willow Ahrens Massachusetts Institute of Technology, Teodoro F. Collin MIT CSAIL, Radha Patel MIT CSAIL, Kyle Deeds University of Washington, Changwan Hong Massachusetts Institute of Technology, Saman Amarasinghe Massachusetts Institute of Technology | ||
16:45 15mTalk | MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution OOPSLA Peng Yuan Ant Group, Yan Liu Ant Group, Jianxin Lai Ant Group, Long Li Ant Group, Tianxiang Sui Ant Group, Linjie Xiao Ant Group, Xiaojing Zhang Ant Group, Qing Zhu Ant Group, Jingling Xue University of New South Wales | ||
17:00 15mTalk | Quantization with Guaranteed Floating-Point Neural Network Classifications OOPSLA | ||
17:15 15mTalk | The Continuous Tensor Abstraction: Where Indices are Real OOPSLA Jaeyeon Won MIT, Willow Ahrens Massachusetts Institute of Technology, Teodoro F. Collin MIT CSAIL, Joel S Emer MIT/NVIDIA, Saman Amarasinghe Massachusetts Institute of Technology | ||
16:00 - 17:30 | |||
16:00 30mTalk | Semantics-preserving Transformation of Context-free Grammars into LL(1) Form Onward! Papers | ||
16:30 30mTalk | An Argument for the Practicality of Entity Component Systems as the Primary Data Structure for an Interpreter or Compiler Onward! Papers | ||
17:00 30mTalk | TideScript: A Domain Specific Language for Peptide Chemistry Onward! Papers Nicholas Morris University of Glasgow, Blair Archibald University of Glasgow, S Hessam M Mehr University of Glasgow | ||
18:00 - 20:00 | |||
18:00 2hSocial Event | SPLASH SRC Poster Session Student Research Competition | ||
Fri 17 OctDisplayed time zone: Perth change
Fri 17 Oct
Displayed time zone: Perth change
09:00 - 10:00 | Friday SPLASH KeynoteSPLASH Keynotes at Orchid Plenary Ballroom Chair(s): Charles Zhang The Hong Kong University of Science and Technology | ||
09:00 60mKeynote | The Quest Toward that Perfect Compiler SPLASH Keynotes | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break ICFP/SPLASH Catering | ||
10:30 - 12:15 | Analysis 1OOPSLA at Orchid East Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
10:30 15mTalk | Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis 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 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 DOI Media Attached File Attached | ||
11:00 15mTalk | Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials OOPSLA Pre-print | ||
11:15 15mTalk | Denotational Foundations for Expected Cost Analysis OOPSLA Pedro Henrique Azevedo de Amorim Cornell University | ||
11:30 15mTalk | IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis OOPSLA | ||
11:45 15mTalk | Revealing Sources of (Memory) Errors via Backward Analysis 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 OOPSLA Chenxi Li Nanjing University, China, Haoran Lin Nanjing University, China, Tian Tan Nanjing University, Yue Li Nanjing University | ||
10:30 - 12:15 | Compilation 3OOPSLA at Orchid Plenary Ballroom Chair(s): Hidehiko Masuhara Institute of Science Tokyo | ||
10:30 15mTalk | Syntactic Completions with Material Obligations 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:45 15mTalk | REPTILE: Performant Tiling of Recurrences 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 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 OOPSLA File Attached | ||
11:30 15mTalk | Static Inference of Regular Grammars for Ad Hoc Parsers OOPSLA DOI Pre-print | ||
10:30 - 12:15 | |||
10:30 - 12:15 | |||
10:30 15mTalk | Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification 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 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 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 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 OOPSLA Yuchen Jiang University of Michigan, Runze Xue University of Michigan; University of Cambridge; Indiana University, Max S. New University of Michigan | ||
10:30 - 12:15 | |||
10:30 30mTalk | What You See Is What It Does: A Structural Pattern for Legible Software Onward! Papers | ||
11:00 30mTalk | Literate Tracing Onward! Papers Matthew Sotoudeh Stanford University Pre-print Media Attached | ||
11:30 30mTalk | ScooPy: Enhancing Program Synthesis with Nested Example Specifications Onward! Papers | ||
12:15 - 13:45 | |||
12:15 90mLunch | Lunch ICFP/SPLASH Catering | ||
13:45 - 15:30 | |||
13:45 15mTalk | An Empirical Evaluation of Property-Based Testing in Python OOPSLA Link to publication | ||
14:00 15mTalk | Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM 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 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 OOPSLA | ||
14:45 15mTalk | Model-guided Fuzzing of Distributed Systems 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 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 DOI Pre-print | ||
15:15 15mTalk | Understanding and Improving Flaky Test Classification 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 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 OOPSLA Alex Kavvos University of Bristol | ||
14:15 15mTalk | A Mechanized Semantics for Dataflow Circuits 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 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 OOPSLA Jay Lee Seoul National University, Joongwon Ahn Seoul National University, Kwangkeun Yi Seoul National University Link to publication DOI | ||
15:00 15mTalk | Semantics of Sets of Programs 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 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 | Onward! Essays 2Onward! Essays / Onward! Papers at Peony SE Chair(s): James Noble Independent. Wellington, NZ | ||
13:45 40mTalk | Carving Text at Its Joints: A New Perspective on Writing and Computers Onward! Essays Kevin Graaf Independent Researcher | ||
14:25 40mTalk | Let's Take Esoteric Programming Languages Seriously Onward! Essays DOI Pre-print | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break ICFP/SPLASH Catering | ||
16:00 - 17:30 | |||
16:00 15mTalk | Bennet: Randomized Specification Testing for Heap-Manipulating Programs OOPSLA | ||
16:15 15mTalk | DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance OOPSLA Chenyang Ma Nanjing University of Science and Technology, Wei Song Nanjing University of Science and Technology, Jeff Huang Texas A&M University DOI | ||
16:30 15mTalk | Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines 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 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 DOI | ||
17:00 15mTalk | Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools OOPSLA | ||
16:00 - 17:30 | Debugging and ValidationOOPSLA at Orchid Small Chair(s): Stefan Marr Johannes Kepler University Linz | ||
16:00 15mTalk | Debugging WebAssembly? Put some Whamm on it! 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 Link to publication DOI Pre-print | ||
16:15 15mTalk | MIO: Multiverse Debugging in the face of Input/Output OOPSLA Tom Lauwaerts Universiteit Gent, Belgium, Maarten Steevens Ghent University, Belgium, Christophe Scholliers Universiteit Gent, Belgium Link to publication DOI Pre-print | ||
16:30 15mTalk | PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer 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 OOPSLA Ruixin Wang Purdue University, Zhongkai Zhao National University of Singapore, Le Fang Purdue University, Nan Jiang Purdue University, Yiling Lou University of Illinois at Urbana-Champaign, Lin Tan Purdue University, Tianyi Zhang Purdue University Link to publication DOI Pre-print | ||
17:00 15mTalk | Translation Validation for LLVM's AArch64 Backend 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 OOPSLA Maolin Sun Nanjing University, Yibiao Yang Nanjing University, Jiangchang Wu 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) 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 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 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 OOPSLA Sam Stites Northeastern University, John Li Northeastern University, Steven Holtzen Northeastern University | ||
17:00 15mTalk | Polymorphic Records for Dynamic Languages OOPSLA | ||
16:00 - 17:30 | |||
16:00 30mTalk | Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities 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 Onward! Papers Jean Pichon-Pharabod Aarhus University | ||
17:30 - 18:15 | SPLASH Organisers Discussion and AMA (and Awards)OOPSLA at Orchid Plenary Ballroom After a quick awards session, SPLASH Steering Committee Chair (Alex Potanin) and the current OOPSLA RC Co-Chairs (Shriram Krishnamurthi and Sukyoung Ryu) will hold “Ask Me Anything” session seeking feedback from the community on the future of SPLASH, OOPSLA, and other events that form SPLASH: https://sigplan.org/Conferences/SPLASH/ | ||
17:30 10mAwards | OOPSLA Awards OOPSLA | ||
17:40 35mMeeting | SPLASH Organisers Discussion and AMA OOPSLA | ||
Sat 18 OctDisplayed time zone: Perth change
Sat 18 Oct
Displayed time zone: Perth change
09:00 - 10:00 | Saturday SPLASH KeynoteSPLASH Keynotes at Orchid Plenary Ballroom Chair(s): Shriram Krishnamurthi Brown University | ||
09:00 60mKeynote | Software Stacks for Confidential Computing Hardware SPLASH Keynotes | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break ICFP/SPLASH Catering | ||
10:30 - 12:15 | |||
10:30 15mTalk | Borrowing From Session Types OOPSLA Hannes Saffrich University of Freiburg, Janek Spaderna University of Freiburg, Germany, Peter Thiemann University of Freiburg, Vasco T. Vasconcelos LASIGE, University of Lisbon | ||
10:45 15mTalk | Modal Effect Types 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 University of Edinburgh, Anton Lorenzen University of Edinburgh | ||
11:00 15mTalk | On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs 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 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 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 OOPSLA DOI Pre-print | ||
12:00 15mTalk | We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators 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 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 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 OOPSLA | ||
11:15 15mTalk | Hambazi: Spatial Coordination Synthesis for Augmented Reality 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 OOPSLA | ||
11:45 15mTalk | LOUD: Synthesizing Strongest and Weakest Specifications 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 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 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 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 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 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 OOPSLA | ||
11:45 15mTalk | qblaze: An Efficient and Scalable Sparse Quantum Simulator 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 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 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 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 OOPSLA | ||
11:15 15mTalk | KestRel: Relational Verification Using E-Graphs for Program Alignment OOPSLA Robert Dickerson Purdue University, Prasita Mukherjee Purdue University, Benjamin Delaware Purdue University | ||
11:30 15mTalk | Laurel: Unblocking Automated Verification with Large Language Models 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 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 DOI | ||
12:00 15mTalk | Verification of Bit-Flip Attacks against Quantized Neural Networks 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 30mFull-paper | Daisy: An Exercise Environment for Learning Information Modeling SPLASH-E Jessica Belicia Cahyono Institute of Science Tokyo, Youyou Cong Institute of Science Tokyo, Hidehiko Masuhara Institute of Science Tokyo | ||
11:00 30mFull-paper | Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements SPLASH-E Shriram Krishnamurthi Brown University, Thore Thießen University of Münster, Jan Vahrenhold University of Münster | ||
11:30 20mShort-paper | Evolving How We Teach Memory Models SPLASH-E A: Pontakorn Prasertsuk , A: Jotham Wong National University of Singapore, Singapore, A: Grace Tan National University of Singapore, A: Cristina Carbunaru National University of Singapore, Singapore | ||
11:50 40mKeynote | How Computer Science Was Introduced at Yale-NUS College SPLASH-E Olivier Danvy National University of Singapore File Attached | ||
10:30 - 12:15 | Onward! Papers and EssayOnward! Papers / Onward! Essays at Peony SE Chair(s): Stephen Kell King's College London | ||
10:30 30mTalk | X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering 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 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 Onward! Papers | ||
12:15 - 13:45 | |||
12:15 90mLunch | Lunch ICFP/SPLASH Catering | ||
13:45 - 15:30 | |||
13:45 15mTalk | Compositional Symbolic Execution for the Next 700 Memory Models 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 Link to publication DOI Pre-print | ||
14:00 15mTalk | Destination calculus: A linear λ-calculus for purely functional memory writes OOPSLA Link to publication DOI Pre-print Media Attached | ||
14:15 15mTalk | Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown OOPSLA DOI Pre-print | ||
14:30 15mTalk | HeapBuffers: Why not just using a binary serialization format for your managed memory? 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 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 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 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 OOPSLA Guanlin Chen Peking University, Ruyi Ji Peking University, Shuhao Zhang Peking University, Yingfei Xiong Peking University DOI | ||
14:00 15mTalk | Language-Parametric Reference Synthesis 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 | UTFix: Change Aware Unit Test Repairing using LLM 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 | ||
14:30 15mTalk | Synthesizing DSLs for Few-Shot Learning 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 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 OOPSLA Jacob Laurel Georgia Institute of Technology, Ignacio Laguna Lawrence Livermore National Laboratory, Jan Hueckelheim Argonne National Laboratory | ||
13:45 - 15:30 | |||
13:45 15mTalk | Adaptive Shielding via Parametric Safety Proofs 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 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 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 OOPSLA John C. Kolesar Yale University, Shan Ali Yale University, Timos Antonopoulos Yale University, Ruzica Piskac Yale University | ||
14:45 15mTalk | Incremental Certified Programming 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 OOPSLA Matthew Sotoudeh Stanford University Link to publication | ||
15:15 15mTalk | SafeTree: Expressive Tree Policies for Microservices OOPSLA | ||
13:45 - 15:30 | Afternoon Paper Session 1SPLASH-E at Peony NW Chair(s): Martin Henz National University of Singapore | ||
13:50 25mFull-paper | An Interactive Learning Environment for Program Design SPLASH-E Kouta Kumamoto , Youyou Cong Institute of Science Tokyo, Hidehiko Masuhara Institute of Science Tokyo | ||
14:15 25mFull-paper | Continuations for All: Language Design Considerations for Accessible Continuations SPLASH-E Youyou Cong Institute of Science Tokyo, Filip Strömbäck Linköping University, Kazuki Ikemori Tokyo Institute of Technology | ||
14:40 25mTalk | Involving Students in Design and Implementation of ECMAScript (JavaScript) Proposals SPLASH-E Mikhail Barash University of Bergen | ||
15:05 25mFull-paper | An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course SPLASH-E Marie Salomon University of British Columbia, Kyle D. Chin , Reid Holmes University of British Columbia, Thomas Fritz University of Zurich, Gail Murphy University of British Columbia | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break ICFP/SPLASH Catering | ||
16:00 - 17:30 | AbstractionOOPSLA at Orchid East Chair(s): Steve Blackburn Google and Australian National University | ||
16:00 15mTalk | Abstract Interpretation of Temporal Safety Effects of Higher Order Programs 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 OOPSLA | ||
16:30 15mTalk | Efficient Abstract Interpretation via Selective Widening OOPSLA | ||
16:45 15mTalk | Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic 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 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 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 OOPSLA DOI | ||
16:15 15mTalk | AutoVerus: Automated Proof Generation for Rust Code 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 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 OOPSLA Andrew Wagner Northeastern University, Olek Gierczak Northeastern University, Brianna Marshall Northeastern University, John Li Northeastern University, Amal Ahmed Northeastern University, USA DOI Pre-print | ||
17:00 15mTalk | Garbage Collection for Rust: The Finalizer Frontier OOPSLA DOI Pre-print | ||
17:15 15mTalk | Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees OOPSLA Zachary Grannan University of British Columbia, Aurea 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 | TOPLAS and RemoteOOPSLA at Orchid Small Chair(s): Charles Zhang The Hong Kong University of Science and Technology | ||
16:00 15mTalk | (TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs OOPSLA DOI | ||
16:15 15mTalk | (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging 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 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 OOPSLA | ||
17:00 15mTalk | Agora: Trust Less and Open More in Verification for Confidential Computing 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 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 | Products of Recursive Programs for Hypersafety Verification OOPSLA | ||
16:15 15mTalk | Embedding Quantum Program Verification into Dafny 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 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 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 | ||
16:00 - 17:30 | |||
15:45 25mFull-paper | Derivation Visualization for Context-Free Grammar Design: Helping Students Understand Context-Free Grammars SPLASH-E | ||
16:10 25mFull-paper | Interactive Theorem Provers for Proof Education SPLASH-E | ||
16:35 25mTalk | Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs SPLASH-E Florian Sihler Ulm University, Naomi Panda , Simon Berlinger Ulm University, Germany, Matthias Tichy Ulm University Link to publication File Attached | ||
17:00 25mFull-paper | Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises SPLASH-E Tommie Lombarts Eindhoven University of Technology, Gijs Walravens Eindhoven University of Technology, Mazyar Seraj Eindhoven University of Technology, Lina Ochoa Eindhoven University of Technology, Mark van den Brand Eindhoven University of Technology | ||