Haskell 2025
Sun 12 - Sat 18 October 2025
Singapore
co-located with
ICFP/SPLASH 2025
Toggle navigation
Attending
Venue (Sunday Workshops): NUS School of Computing
Venue (FARM Performance): Yong Siew Toh Conservatory
Venue (Main Conference): Marina Bay Sands Convention Centre
Hotels: Concorde Hotel Singapore
Hotels: Wyndham Singapore Hotel
Hotels: Rendezvous Hotel Singapore
Program
Haskell Program
Your Program
Filter by Day
Sun 12 Oct
Mon 13 Oct
Tue 14 Oct
Wed 15 Oct
Thu 16 Oct
Fri 17 Oct
Sat 18 Oct
Track/Call
Organization
Haskell 2025 Committees
Track Committees
Program Committee
Contributors
People Index
Search
Series
Series
Haskell 2025
Haskell 2024
Haskell 2023
Haskell 2022
Haskell 2021
Haskell 2020
Haskell 2019
Haskell 2018
Haskell 2017
Haskell 2016
Sign in
Sign up
ICFP/SPLASH 2025
(
series
) /
Haskell 2025 (
series
) /
Marina Bay Sands Convention Centre
/
Room information: Orchid Small
Venue
Marina Bay Sands Convention Centre
Room name
Orchid Small
Floor
4
Room number
4201A-4201B
Capacity
80
Room Information
Venue floor plan
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT+08:00) Perth
.
Use conference time zone: (GMT+08:00) Perth
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
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 program
Specify 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 1
HATRA
at
Orchid Small
Chair(s):
Michael Coblenz
University of California, San Diego
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
Link to publication
11:15
25m
Talk
Imperative Syntax for Dependent Types
HATRA
Bhakti Shah
University of St. Andrews
,
Edwin Brady
University of St. Andrews
Link to publication
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
Link to publication
13:40 - 15:20
Session 2
HATRA
at
Orchid Small
Chair(s):
Cyrus Omar
University of Michigan
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
Link to publication
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
Remote
HATRA
Pablo Donato
LIX, IPP
,
Benjamin Werner
LIX, IPP
Link to publication
16:00 - 17:40
Session 3
HATRA
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 Generation
LMPL
at
Orchid Small
Chair(s):
Guannan Wei
Tufts 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
recorded
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
remote
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
remote
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 Design
LMPL
at
Orchid Small
Chair(s):
Yang Feng
Nanjing University
16:00
15m
Talk
Vibe Coding Needs Vibe Reasoning – Improving Vibe Coding with Formal Verification
remote
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 1
WebAssembly Workshop
at
Orchid Small
Chair(s):
Conrad Watt
Nanyang Technological University
10:30
45m
Keynote
[Keynote] Keynote and SpecTec demo
WebAssembly Workshop
Andreas Rossberg
Independent
11:15
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:35
20m
Talk
Wasmgrind: Towards Dynamic Concurrency Analysis for Multithreaded WebAssembly
WebAssembly Workshop
Michael Staab
University of Freiburg
,
Peter Thiemann
University of Freiburg
11:55
20m
Talk
What is Fairy Dust? Universal Contracts for WebAssembly
WebAssembly Workshop
Jean Pichon-Pharabod
Aarhus University
13:45 - 15:30
Session 2
WebAssembly Workshop
at
Orchid Small
Chair(s):
Conrad Watt
Nanyang Technological University
13:45
25m
Keynote
[Keynote] Wasm GC and the Future of High-Level Language Compilation
WebAssembly Workshop
Oscar Spencer
14:10
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
14:30
20m
Talk
On Dynamic Multimedia Pipelines for Opening Browsers to New Formats
remote
WebAssembly Workshop
Jérôme Gorin
GeNumEr
,
Maja Bystrom
Bevara
14:50
20m
Talk
Hyperlight-Wasm: Bringing virtualisation-based security to Wasm, and using Wasm at Microsoft
WebAssembly Workshop
Lucy Menon
Microsoft
15:10
20m
Talk
Iris-Wasm: reasoning formally about Wasm and Wasm extensions
remote
WebAssembly Workshop
Maxime Legoupil
Aarhus University
16:00 - 17:30
Session 3
WebAssembly Workshop
at
Orchid Small
Chair(s):
Conrad Watt
Nanyang Technological University
16:00
25m
Keynote
[Keynote] “Codename: Tunahead” aka Software Engineering Economics for Runtimes
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
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
17:25
5m
Day closing
Closing
WebAssembly Workshop
Conrad Watt
Nanyang Technological University
Fri 17 Oct
Displayed time zone:
Perth
change
10:30 - 12:15
SRC Presentations
SPLASH Student Research Competition
at
Orchid Small
13:45 - 15:30
Semantics
SPLASH OOPSLA
at
Orchid Small
Chair(s):
Hakjoo Oh
Korea University
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
Link to publication
DOI
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 Validation
SPLASH OOPSLA
at
Orchid Small
Chair(s):
Stefan Marr
Johannes Kepler University Linz
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
Link to publication
DOI
Pre-print
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
Link to publication
DOI
Pre-print
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
University of Illinois at Urbana-Champaign
,
Lin Tan
Purdue University
,
Tianyi Zhang
Purdue University
Link to publication
DOI
Pre-print
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
Nanjing University
,
Yuming Zhou
Nanjing University
Sat 18 Oct
Displayed time zone:
Perth
change
10:30 - 12:15
Quantum
SPLASH OOPSLA
at
Orchid Small
Chair(s):
Jens Palsberg
University of California, Los Angeles (UCLA)
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
Proofs
SPLASH OOPSLA
at
Orchid Small
Chair(s):
Peter Thiemann
University of Freiburg
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 Remote
SPLASH OOPSLA
at
Orchid Small
Chair(s):
Charles Zhang
The Hong Kong University of Science and Technology
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
Remote
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
recorded
Reasoning as a Resource: Optimizing Fast and Slow Thinking in Code Gene ...
13:55 - 14:10
LMPL
remote
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
remote
Programming Language Techniques for Bridging LLM Code Generation Semant ...
14:55 - 15:10
LMPL
remote
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] Keynote and SpecTec demo
10:30 - 11:15
WebAssembly Workshop
Implementing and Evaluating a High-Level Language with WasmGC and the W ...
11:15 - 11:35
WebAssembly Workshop
Wasmgrind: Towards Dynamic Concurrency Analysis for Multithreaded WebAs ...
11:35 - 11:55
WebAssembly Workshop
What is Fairy Dust? Universal Contracts for WebAssembly
11:55 - 12:15
WebAssembly Workshop
[Keynote] Wasm GC and the Future of High-Level Language Compilation
13:45 - 14:10
WebAssembly Workshop
Dynamic Analysis Extending a Shadow Runtime for Profit
14:10 - 14:30
WebAssembly Workshop
remote
On Dynamic Multimedia Pipelines for Opening Browsers to New Formats
14:30 - 14:50
WebAssembly Workshop
Hyperlight-Wasm: Bringing virtualisation-based security to Wasm, and us ...
14:50 - 15:10
WebAssembly Workshop
remote
Iris-Wasm: reasoning formally about Wasm and Wasm extensions
15:10 - 15:30
WebAssembly Workshop
[Keynote] “Codename: Tunahead” aka Software Engineering Economics for R ...
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
Efficient Concolic Execution of WebAssembly by Compilation and Snapshot ...
17:05 - 17:25
WebAssembly Workshop
Closing
17:25 - 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 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
x
Mon 27 Oct 05:31