Orchid Small - ICFP 2025

VenueMarina Bay Sands Convention Centre

Room nameOrchid Small

Floor4

Room number4201A-4201B

Capacity80

Room Information

Venue floor plan

app-screen

Program

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+08:00) Perth.

Use conference time zone: (GMT+08:00) PerthSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

You're viewing the program in a time zone which is different from your device's time zone change time zone

Tue 14 Oct
Displayed time zone: Perth change

10:50 - 12:05	Session 1HATRA at Orchid Small

10:50 25m Talk		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 25m Talk		Imperative Syntax for Dependent Types HATRA Bhakti Shah University of St. Andrews, Edwin Brady University of St. Andrews
11:40 25m Talk		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

13:40 - 15:20	Session 2HATRA at Orchid Small

13:40 25m Talk		Negative Bounds for Avoiding Conflicts in Implementing Traits in Rust HATRA Yuki Okamoto Shibaura Institute of Technology, Isao Sasano Shibaura Institute of Technology Link to publication
14:05 25m Talk		P4-SpecTec: A Language Mechanization Framework for P4 HATRA Jaehyun Lee KAIST, Seokhun Jeong KAIST, Sukyoung Ryu KAIST
14:30 25m Talk		Types as a Specification Language for Creativity HATRA Youyou Cong Institute of Science Tokyo Link to publication
14:55 25m Talk		Actema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestural Interaction HATRA Pablo Donato LIX, IPP, Benjamin Werner LIX, IPP

16:00 - 17:40	Session 3HATRA at Orchid Small

16:00 1h40m Meeting		Discussion HATRA Michael Coblenz University of California, San Diego, Jonathan Aldrich Carnegie Mellon University, Will Crichton Brown University

Wed 15 Oct
Displayed time zone: Perth change

13:40 - 15:20	LLMs for Code GenerationLMPL at Orchid Small Chair(s): Di Wang Peking University

13:40 15m Talk		W2GPU: Toward WebAssembly-to-WebGPU Program Translation via Small Language Models LMPL Mehmet Oguz Derin Unaffiliated Media Attached
13:55 15m Talk		Reasoning as a Resource: Optimizing Fast and Slow Thinking in Code Generation Models LMPL Zongjie Li The Hong Kong University of Science and Technology, Shuai Wang Hong Kong University of Science and Technology
14:10 15m Talk		Ranking Formal Specifications using LLMs LMPL Deyuan (Mike) He Princeton University, Zhendong Ang National University of Singapore, Ankush Desai Amazon Web Services, Aarti Gupta Princeton University
14:25 15m Talk		Challenges in C++ to Rust Translation with Large Language Models: A Preliminary Empirical Study LMPL Yanyan Yan Nanjing University, Yang Feng Nanjing University, Qi He Nanjing University, Jun Zeng Chongqing University, Baowen Xu Nanjing University
14:40 15m Talk		The Modular Imperative: Rethinking LLMs for Maintainable Software LMPL Anastasiya Kravchuk-Kirilyuk Harvard University, Fernanda Graciolli Midspiral, Nada Amin Harvard University
14:55 15m Talk		Programming Language Techniques for Bridging LLM Code Generation Semantic Gaps LMPL Yalong Du Harbin Institute of Technology, Shenzhen, Chaozheng Wang The Chinese University of Hong Kong, Huaijin Wang Ohio State University

16:00 - 17:40	Neuro-Symbolic Language/Agent DesignLMPL at Orchid Small Chair(s): Yang Feng Nanjing University

16:00 15m Talk		Vibe Coding Needs Vibe Reasoning – Improving Vibe Coding with Formal Verification LMPL Jacqueline Mitchell University of Southern California, Yasser Shaaban Workato
16:15 15m Talk		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 15m Talk		Composable Effect Handling for Programming LLM-integrated Scripts LMPL Di Wang Peking University Pre-print
16:45 15m Talk		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 15m Talk		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

Thu 16 Oct
Displayed time zone: Perth change

10:30 - 12:15	Session 1WebAssembly Workshop at Orchid Small Chair(s): Conrad Watt Nanyang Technological University

10:30 25m Keynote		Keynote WebAssembly Workshop Andreas Rossberg Independent
10:55 20m Talk		Implementing and Evaluating a High-Level Language with WasmGC and the Wasm Component Model: Scala’s Case WebAssembly Workshop Rikito Taniguchi VirtusLab and Institute of Science Tokyo, Sébastien Doeraene EPFL, Switzerland, Hidehiko Masuhara Institute of Science Tokyo
11:15 20m Talk		Wasmgrind: Towards Dynamic Concurrency Analysis for Multithreaded WebAssembly WebAssembly Workshop Michael Staab University of Freiburg, Peter Thiemann University of Freiburg, Germany
11:35 20m Talk		Efficient Concolic Execution of WebAssembly by Compilation and Snapshot Reuse WebAssembly Workshop Dinghong Zhong Tufts University, Alexander Bai New York University, Guannan Wei Tufts University
11:55 20m Talk		What is Fairy Dust? Universal Contracts for WebAssembly WebAssembly Workshop Jean Pichon-Pharabod Aarhus University

13:45 - 15:30	Session 2WebAssembly Workshop at Orchid Small Chair(s): Conrad Watt Nanyang Technological University

13:45 25m Keynote		Keynote WebAssembly Workshop Oscar Spencer
14:10 20m Talk		Hyperlight-Wasm: Bringing virtualisation-based security to Wasm, and using Wasm at Microsoft WebAssembly Workshop Lucy Menon Microsoft
14:30 20m Talk		On Dynamic Multimedia Pipelines for Opening Browsers to New Formats WebAssembly Workshop Jérôme Gorin GeNumEr, Maja Bystrom Bevara
14:50 20m Talk		Dynamic Analysis Extending a Shadow Runtime for Profit WebAssembly Workshop Aäron Munsters Vrije Universiteit Brussel, Angel Luis Scull Pupo Vrije Universiteit Brussel, Elisa Gonzalez Boix Vrije Universiteit Brussel File Attached
15:10 20m Talk		Iris-Wasm: reasoning formally about Wasm and Wasm extensions WebAssembly Workshop Maxime Legoupil Aarhus University

16:00 - 17:30	Session 3WebAssembly Workshop at Orchid Small Chair(s): Conrad Watt Nanyang Technological University

16:00 25m Keynote		Keynote WebAssembly Workshop Chris Woods
16:25 20m Talk		BabelBridge: A Control-Flow Graph Debugger for Microcontrollers WebAssembly Workshop Carlos Rojas Castillo Vrije Universiteit Brussel, Matteo Marra Nokia Bell Labs, Belgium, Elisa Gonzalez Boix Vrije Universiteit Brussel
16:45 20m Talk		Updating WasmCert-Isabelle to WebAssembly 2.0 WebAssembly Workshop Antanas Kalkauskas Nanyang Technological University
17:05 25m Other		Closing WebAssembly Workshop Conrad Watt Nanyang Technological University

Fri 17 Oct
Displayed time zone: Perth change

10:30 - 12:15	SRC PresentationsSPLASH Student Research Competition at Orchid Small

10:30 13m Poster		A Concurrency-Testing Approach for Detecting Isolation Level Bugs in Database Systems SPLASH Student Research Competition Arsyad Kamili
10:43 13m Poster		Automata Visualization for Validation and Verification: Helping Develop Correctness Arguments for Nondeterministic Machines SPLASH Student Research Competition David Anthony K. Fields Seton Hall University
10:56 13m Poster		Formal Verification of Graham's Scan Algorithm SPLASH Student Research Competition Yingjun Lan
11:09 13m Poster		LegoFuzz: Interleaving Large Language Models for Compiler Testing SPLASH Student Research Competition Yunbo Ni The Chinese University of Hong Kong
11:22 13m Poster		LLM-assisted Dialect-Agnostic SQL Query Parsing SPLASH Student Research Competition Junwen An
11:35 13m Poster		On A Multitier Actor Programming Language SPLASH Student Research Competition HYEONJIN LEE
11:48 13m Poster		Restoring Data Sovereignty: A Human-Centered Approach Blockchain Health Technology SPLASH Student Research Competition Polina Vinogradova
12:01 13m Poster		Siloso: Finding Logic Bugs in RDBMS via Dialect-Adaptable Reference Engine Construction SPLASH Student Research Competition Emily Ong National University of Singapore

13:45 - 15:30	SemanticsSPLASH OOPSLA at Orchid Small

13:45 15m Talk		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 15m Talk		Adequacy for Algebraic Effects Revisited SPLASH OOPSLA Alex Kavvos University of Bristol
14:15 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		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

16:00 - 17:30	Debugging and ValidationSPLASH OOPSLA at Orchid Small

16:00 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		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

Sat 18 Oct
Displayed time zone: Perth change

10:30 - 12:15	QuantumSPLASH OOPSLA at Orchid Small

10:30 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		QbC: Quantum Correctness by Construction SPLASH OOPSLA Anurudh Peduri Ruhr University Bochum, Ina Schaefer KIT, Michael Walter Ruhr-Universität Bochum
11:45 15m Talk		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 15m Talk		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

13:45 - 15:30	ProofsSPLASH OOPSLA at Orchid Small

13:45 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		Pathological Cases for a Class of Reachability-Based Garbage Collectors SPLASH OOPSLA Matthew Sotoudeh Stanford University Link to publication
15:15 15m Talk		SafeTree: Expressive Tree Policies for Microservices SPLASH OOPSLA Karuna Grewal Cornell University, Brighten Godfrey UIUC and Broadcom, Justin Hsu Cornell University

16:00 - 17:30	TOPLAS and RemoteSPLASH OOPSLA at Orchid Small

16:00 15m Talk		(TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs SPLASH OOPSLA Xusheng Zhi University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison DOI
16:15 15m Talk		(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 15m Talk		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 15m Talk		Modal Abstractions for Virtualizing Memory Addresses SPLASH OOPSLA Ismail Kuru Drexel University, Colin Gordon Drexel University
17:00 15m Talk		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 15m Talk		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

Tue 14 Oct
Displayed time zone: Perth change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Orchid Small											HATRA Session 1																																		HATRA Session 2																												HATRA Session 3

Wed 15 Oct
Displayed time zone: Perth change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Orchid Small											LMPL																																		LMPL LLMs for Code Generation																												LMPL Neuro-Symbolic Language/Agent Design

Thu 16 Oct
Displayed time zone: Perth change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Orchid Small							WebAssembly Workshop Session 1																																							WebAssembly Workshop Session 2																											WebAssembly Workshop Session 3

Fri 17 Oct
Displayed time zone: Perth change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Orchid Small							SPLASH Student Research Competition SRC Presentations																																							SPLASH OOPSLA Semantics																											SPLASH OOPSLA Debugging and Validation

Sat 18 Oct
Displayed time zone: Perth change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Orchid Small							SPLASH OOPSLA Quantum																																							SPLASH OOPSLA Proofs																											SPLASH OOPSLA TOPLAS and Remote

Tue 14 Oct
Displayed time zone: Perth change


Room	10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Orchid Small											HATRA Usability Barriers for Liquid Types (Summary of Published Work) 10:50 - 11:15					HATRA Imperative Syntax for Dependent Types 11:15 - 11:40					HATRA Decomposable Type Highlighting for Bidirectional Type and Cast Systems 11:40 - 12:05																								HATRA Negative Bounds for Avoiding Conflicts in Implementing Traits in Rust 13:40 - 14:05					HATRA P4-SpecTec: A Language Mechanization Framework for P4 14:05 - 14:30					HATRA Types as a Specification Language for Creativity 14:30 - 14:55					HATRA Actema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestur ... 14:55 - 15:20													HATRA Discussion 16:00 - 17:40

Wed 15 Oct
Displayed time zone: Perth change


Room	13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Orchid Small									LMPL W2GPU: Toward WebAssembly-to-WebGPU Program Translation via Small Langu ... 13:40 - 13:55			LMPL Reasoning as a Resource: Optimizing Fast and Slow Thinking in Code Gene ... 13:55 - 14:10			LMPL Ranking Formal Specifications using LLMs 14:10 - 14:25			LMPL Challenges in C++ to Rust Translation with Large Language Models: A Pre ... 14:25 - 14:40			LMPL The Modular Imperative: Rethinking LLMs for Maintainable Software 14:40 - 14:55			LMPL Programming Language Techniques for Bridging LLM Code Generation Semant ... 14:55 - 15:10													LMPL Vibe Coding Needs Vibe Reasoning – Improving Vibe Coding with Formal Ve ... 16:00 - 16:15			LMPL Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—a ... 16:15 - 16:30			LMPL Composable Effect Handling for Programming LLM-integrated Scripts 16:30 - 16:45			LMPL The LLM Era Demands Natural-Language-Aligned Theorem Provers for Mathem ... 16:45 - 17:00			LMPL Programming Large Language Models with Algebraic Effect Handlers and th ... 17:00 - 17:15

Thu 16 Oct
Displayed time zone: Perth change


Room	10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Orchid Small							WebAssembly Workshop Keynote 10:30 - 10:55					WebAssembly Workshop Implementing and Evaluating a High-Level Language with WasmGC and the W ... 10:55 - 11:15				WebAssembly Workshop Wasmgrind: Towards Dynamic Concurrency Analysis for Multithreaded WebAs ... 11:15 - 11:35				WebAssembly Workshop Efficient Concolic Execution of WebAssembly by Compilation and Snapshot ... 11:35 - 11:55				WebAssembly Workshop What is Fairy Dust? Universal Contracts for WebAssembly 11:55 - 12:15																						WebAssembly Workshop Keynote 13:45 - 14:10					WebAssembly Workshop Hyperlight-Wasm: Bringing virtualisation-based security to Wasm, and us ... 14:10 - 14:30				WebAssembly Workshop On Dynamic Multimedia Pipelines for Opening Browsers to New Formats 14:30 - 14:50				WebAssembly Workshop Dynamic Analysis Extending a Shadow Runtime for Profit 14:50 - 15:10				WebAssembly Workshop Iris-Wasm: reasoning formally about Wasm and Wasm extensions 15:10 - 15:30										WebAssembly Workshop Keynote 16:00 - 16:25					WebAssembly Workshop BabelBridge: A Control-Flow Graph Debugger for Microcontrollers 16:25 - 16:45				WebAssembly Workshop Updating WasmCert-Isabelle to WebAssembly 2.0 16:45 - 17:05				WebAssembly Workshop Closing 17:05 - 17:30

Fri 17 Oct
Displayed time zone: Perth change


Room	10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Orchid Small							SPLASH Student Research Competition A Concurrency-Testing Approach for Detecting Isolation Level Bugs in Da ... 10:30 - 10:43			SPLASH Student Research Competition Automata Visualization for Validation and Verification: Helping Develop ... 10:43 - 10:56		SPLASH Student Research Competition Formal Verification of Graham's Scan Algorithm 10:56 - 11:09			SPLASH Student Research Competition LegoFuzz: Interleaving Large Language Models for Compiler Testing 11:09 - 11:22		SPLASH Student Research Competition LLM-assisted Dialect-Agnostic SQL Query Parsing 11:22 - 11:35			SPLASH Student Research Competition On A Multitier Actor Programming Language 11:35 - 11:48			SPLASH Student Research Competition Restoring Data Sovereignty: A Human-Centered Approach Blockchain Health ... 11:48 - 12:01		SPLASH Student Research Competition Siloso: Finding Logic Bugs in RDBMS via Dialect-Adaptable Reference Eng ... 12:01 - 12:15																					SPLASH OOPSLA A complete formal semantics of eBPF instruction set architecture for Solana 13:45 - 14:00			SPLASH OOPSLA Adequacy for Algebraic Effects Revisited 14:00 - 14:15			SPLASH OOPSLA A Mechanized Semantics for Dataflow Circuits 14:15 - 14:30			SPLASH OOPSLA Dynamic Wind for Effect Handlers 14:30 - 14:45			SPLASH OOPSLA React-tRace: A Semantics for Understanding React Hooks 14:45 - 15:00			SPLASH OOPSLA Semantics of Sets of Programs 15:00 - 15:15			SPLASH OOPSLA Zero-Overhead Lexical Effect Handlers 15:15 - 15:30									SPLASH OOPSLA Debugging WebAssembly? Put some Whamm on it! 16:00 - 16:15			SPLASH OOPSLA MIO: Multiverse Debugging in the face of Input/Output 16:15 - 16:30			SPLASH OOPSLA PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Co ... 16:30 - 16:45			SPLASH OOPSLA Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repai ... 16:45 - 17:00			SPLASH OOPSLA Translation Validation for LLVM's AArch64 Backend 17:00 - 17:15			SPLASH OOPSLA Validating SMT Rewriters via Rewrite Space Exploration Supported by Gen ... 17:15 - 17:30

Sat 18 Oct
Displayed time zone: Perth change


Room	10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Orchid Small							SPLASH OOPSLA AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Qu ... 10:30 - 10:45			SPLASH OOPSLA A Language for Quantifying Quantum Network Behavior 10:45 - 11:00			SPLASH OOPSLA Compositional Quantum Control Flow with Efficient Compilation in Qunity 11:00 - 11:15			SPLASH OOPSLA Dependency-Aware Compilation for Surface Code Quantum Architectures 11:15 - 11:30			SPLASH OOPSLA QbC: Quantum Correctness by Construction 11:30 - 11:45			SPLASH OOPSLA qblaze: An Efficient and Scalable Sparse Quantum Simulator 11:45 - 12:00			SPLASH OOPSLA Shaking Up Quantum Simulators with Fuzzing and Rigour 12:00 - 12:15																					SPLASH OOPSLA Adaptive Shielding via Parametric Safety Proofs 13:45 - 14:00			SPLASH OOPSLA Certified Decision Procedures for Width-Independent Bitvector Predicates 14:00 - 14:15			SPLASH OOPSLA Checking $\delta$-Satisfiability of Reals with Integrals 14:15 - 14:30			SPLASH OOPSLA Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge 14:30 - 14:45			SPLASH OOPSLA Incremental Certified Programming 14:45 - 15:00			SPLASH OOPSLA Pathological Cases for a Class of Reachability-Based Garbage Collectors 15:00 - 15:15			SPLASH OOPSLA SafeTree: Expressive Tree Policies for Microservices 15:15 - 15:30									SPLASH OOPSLA (TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs 16:00 - 16:15			SPLASH OOPSLA (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging 16:15 - 16:30			SPLASH OOPSLA Detecting and explaining (in-)equivalence of context-free grammars 16:30 - 16:45			SPLASH OOPSLA Modal Abstractions for Virtualizing Memory Addresses 16:45 - 17:00			SPLASH OOPSLA Agora: Trust Less and Open More in Verification for Confidential Computing 17:00 - 17:15			SPLASH OOPSLA QED in Context: An Observation Study of Proof Assistant Users 17:15 - 17:30

Room information: Orchid Small

This program is tentative and subject to change.

Tue 14 Oct
Displayed time zone: Perth change

Wed 15 Oct
Displayed time zone: Perth change

Thu 16 Oct
Displayed time zone: Perth change

Fri 17 Oct
Displayed time zone: Perth change

Sat 18 Oct
Displayed time zone: Perth change

Tue 14 Oct
Displayed time zone: Perth change

HATRA

HATRA

HATRA

Wed 15 Oct
Displayed time zone: Perth change

LMPL

LMPL

LMPL

Thu 16 Oct
Displayed time zone: Perth change

WebAssembly Workshop

WebAssembly Workshop

WebAssembly Workshop

Fri 17 Oct
Displayed time zone: Perth change

SPLASH Student Research Competition

SPLASH OOPSLA

SPLASH OOPSLA

Sat 18 Oct
Displayed time zone: Perth change

SPLASH OOPSLA

SPLASH OOPSLA

SPLASH OOPSLA

Tue 14 Oct
Displayed time zone: Perth change

Wed 15 Oct
Displayed time zone: Perth change

Thu 16 Oct
Displayed time zone: Perth change

Fri 17 Oct
Displayed time zone: Perth change

Sat 18 Oct
Displayed time zone: Perth change

Tracks

ICFP/SPLASH 2025

Co-hosted Conferences

Workshops

Co-hosted Symposia

Room information: Orchid Small

This program is tentative and subject to change.

Program Display Configuration

Tue 14 OctDisplayed time zone: Perth change

Wed 15 OctDisplayed time zone: Perth change

Thu 16 OctDisplayed time zone: Perth change

Fri 17 OctDisplayed time zone: Perth change

Sat 18 OctDisplayed time zone: Perth change

Tue 14 OctDisplayed time zone: Perth change

HATRA

HATRA

HATRA

Wed 15 OctDisplayed time zone: Perth change

LMPL

LMPL

LMPL

Thu 16 OctDisplayed time zone: Perth change

WebAssembly Workshop

WebAssembly Workshop

WebAssembly Workshop

Fri 17 OctDisplayed time zone: Perth change

SPLASH Student Research Competition

SPLASH OOPSLA

SPLASH OOPSLA

Sat 18 OctDisplayed time zone: Perth change

SPLASH OOPSLA

SPLASH OOPSLA

SPLASH OOPSLA

Tue 14 OctDisplayed time zone: Perth change

Wed 15 OctDisplayed time zone: Perth change

Thu 16 OctDisplayed time zone: Perth change

Fri 17 OctDisplayed time zone: Perth change

Sat 18 OctDisplayed time zone: Perth change

Tue 14 Oct
Displayed time zone: Perth change

Wed 15 Oct
Displayed time zone: Perth change

Thu 16 Oct
Displayed time zone: Perth change

Fri 17 Oct
Displayed time zone: Perth change

Sat 18 Oct
Displayed time zone: Perth change

Tue 14 Oct
Displayed time zone: Perth change

Wed 15 Oct
Displayed time zone: Perth change

Thu 16 Oct
Displayed time zone: Perth change

Fri 17 Oct
Displayed time zone: Perth change

Sat 18 Oct
Displayed time zone: Perth change

Tue 14 Oct
Displayed time zone: Perth change

Wed 15 Oct
Displayed time zone: Perth change

Thu 16 Oct
Displayed time zone: Perth change

Fri 17 Oct
Displayed time zone: Perth change

Sat 18 Oct
Displayed time zone: Perth change