Cosmos - PLDI 2025

VenueThe Westin Josun Seoul

Room nameCosmos

Floor2

Room InformationNo extra information available

Program

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+09:00) Seoul.

Use conference time zone: (GMT+09:00) SeoulSelect 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

Mon 16 Jun
Displayed time zone: Seoul change

09:00 - 10:10	Session 1Sparse at Cosmos Chair(s): Amir Shaikhha University of Edinburgh

09:00 20m Talk		Insum: Sparse GPU Kernels Simplified and Optimized with Indirect Einsums Sparse Saman Amarasinghe Massachusetts Institute of Technology
09:20 20m Talk		Intelligent Auto-Tuning for High-Performance Sparse Tensor Algebra Sparse Jiajia Li North Carolina State University
09:40 20m Talk		Loop Fusion in Matrix Multiplications with Sparse Dependence Sparse Kazem Cheshmi McMaster University
10:00 10m Talk		Panel 1 Sparse Saman Amarasinghe Massachusetts Institute of Technology, Kazem Cheshmi McMaster University, Jiajia Li North Carolina State University

10:30 - 12:00	Session 2Sparse at Cosmos Chair(s): Willow Ahrens Massachusetts Institute of Technology

10:30 20m Talk		Optimizations and abstractions for sparse machine learningRecorded Sparse Charith Mendis University of Illinois at Urbana-Champaign
10:50 20m Talk		Distributed Sparse Computing with Legate Sparse Sparse Rohan Yadav Stanford University
11:10 20m Talk		Optimizing Recursive Sparse Computations Sparse Amir Shaikhha University of Edinburgh
11:30 20m Talk		Panel 2 Sparse Charith Mendis University of Illinois at Urbana-Champaign, Rohan Yadav Stanford University, Amir Shaikhha University of Edinburgh

14:00 - 15:20	Session 3Sparse at Cosmos Chair(s): Rohan Yadav Stanford University

14:00 20m Talk		PyData/Sparse & Finch: extending sparse computing in the Python ecosystem Sparse Hameer Abbasi Quansight, Mateusz Sokol Quansight Labs
14:20 20m Talk		Compiling and Compressing Structured TensorsRecorded Sparse Emilien Bauer
14:40 20m Talk		Sparsity-Aware Autoscheduling for Numpy with Finch and Galley Sparse Willow Ahrens Massachusetts Institute of Technology
15:00 20m Talk		Panel 3 Sparse Hameer Abbasi Quansight, Emilien Bauer , Willow Ahrens Massachusetts Institute of Technology, Mateusz Sokol Quansight Labs

15:40 - 17:00	Session 4Sparse at Cosmos Chair(s): Kazem Cheshmi McMaster University

15:40 20m Talk		Hyperreal Specifications for Continuous Sparse Data Computations Sparse Vladimir Gladshtein
16:00 20m Talk		Quantum Simulation with Sparse Tensors Sparse Meisam Tarabkhah University of Edinburgh
16:20 20m Talk		Sparse Computing Drives Energy-Efficient Computation for Artificial Intelligence Sparse Guohao Dai
16:40 20m Talk		Panel 4 Sparse Meisam Tarabkhah University of Edinburgh, Vladimir Gladshtein , Guohao Dai

Tue 17 Jun
Displayed time zone: Seoul change

09:00 - 10:10	Session 1RPLS at Cosmos K and Redex

09:15 25m Talk		Programming Languages Must Have Formal Semantics. Period. RPLS Xiaohong Chen University of Illinois at Urbana-Champaign
09:40 25m Talk		Lightweight Semantics Engineering with Redex RPLS Matthew Flatt University of Utah

10:30 - 12:00	Session 2RPLS at Cosmos Mechanized Specifications for WebAssembly and JavaScript

10:30 25m Talk		SpecTec, a Single Source of Truth RPLS Sukyoung Ryu KAIST
10:55 25m Talk		Trusted JavaScript Language Environments with ESMeta RPLS Jihyeok Park Korea University
11:20 25m Talk		The Software Supporting the JavaScript Language Specification RPLS Michael Ficarra F5

14:00 - 15:20	Session 3RPLS at Cosmos Verification and Reasoning

14:05 25m Talk		Lightweight Hypervisor Verification: Putting the Hardware Burger on a DietRemote RPLS Nate Foster Cornell University; Jane Street
14:30 25m Talk		P4-Based Automated Reasoning (P4-BAR) using Symbolic Execution at Google RPLS Jonathan DiLorenzo Google
14:55 25m Talk		Verification of WebAssembly Features RPLS Philippa Gardner Imperial College London, Conrad Watt Nanyang Technological University

15:40 - 17:30	Session 4RPLS at Cosmos Specifications for Real-World Programming Languages

15:40 25m Talk		MiniRust: A Core Language for Specifying Rust RPLS Ralf Jung ETH Zurich
16:05 25m Talk		Production Language Specification - Requirements for Multiple UsagesRemote RPLS Peter Sewell University of Cambridge
16:30 60m Panel		Panel: Mechanized Specifications for Real-World Programming Languages RPLS M: Sukyoung Ryu KAIST, P: Xiaohong Chen University of Illinois at Urbana-Champaign, P: Jonathan DiLorenzo Google, P: Michael Ficarra F5, P: Ralf Jung ETH Zurich

19:30 - 21:30	LCTES Committee DinnerLCTES / Catering at Cosmos

19:30 2h Dinner		Dinner Catering

Hide past events

Mon 16 Jun
Displayed time zone: Seoul change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30
Cosmos	Sparse Session 1																		Sparse Session 2																																										Sparse Session 3																				Sparse Session 4

Tue 17 Jun
Displayed time zone: Seoul change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30						19:00						30						20:00						30						21:00						30
Cosmos	RPLS Session 1																		RPLS Session 2																																										RPLS Session 3																				RPLS Session 4																																														LCTES + Catering LCTES Committee Dinner

Hide past events

Mon 16 Jun
Displayed time zone: Seoul change


Room	9:00			15			30			45			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
Cosmos	Sparse Insum: Sparse GPU Kernels Simplified and Optimized with Indirect Einsums 09:00 - 09:20				Sparse Intelligent Auto-Tuning for High-Performance Sparse Tensor Algebra 09:20 - 09:40				Sparse Loop Fusion in Matrix Multiplications with Sparse Dependence 09:40 - 10:00				Sparse Panel 1 10:00 - 10:10						SparseRecorded Optimizations and abstractions for sparse machine learning 10:30 - 10:50				Sparse Distributed Sparse Computing with Legate Sparse 10:50 - 11:10				Sparse Optimizing Recursive Sparse Computations 11:10 - 11:30				Sparse Panel 2 11:30 - 11:50																														Sparse PyData/Sparse & Finch: extending sparse computing in the Python ecosystem 14:00 - 14:20				SparseRecorded Compiling and Compressing Structured Tensors 14:20 - 14:40				Sparse Sparsity-Aware Autoscheduling for Numpy with Finch and Galley 14:40 - 15:00				Sparse Panel 3 15:00 - 15:20								Sparse Hyperreal Specifications for Continuous Sparse Data Computations 15:40 - 16:00				Sparse Quantum Simulation with Sparse Tensors 16:00 - 16:20				Sparse Sparse Computing Drives Energy-Efficient Computation for Artificial Int ... 16:20 - 16:40				Sparse Panel 4 16:40 - 17:00

Tue 17 Jun
Displayed time zone: Seoul change


Room	9:00			15			30			45			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			18:00			15			30			45			19:00			15			30			45			20:00			15			30			45			21:00			15			30			45
Cosmos				RPLS Programming Languages Must Have Formal Semantics. Period. 09:15 - 09:40					RPLS Lightweight Semantics Engineering with Redex 09:40 - 10:05										RPLS SpecTec, a Single Source of Truth 10:30 - 10:55					RPLS Trusted JavaScript Language Environments with ESMeta 10:55 - 11:20					RPLS The Software Supporting the JavaScript Language Specification 11:20 - 11:45																																	RPLSRemote Lightweight Hypervisor Verification: Putting the Hardware Burger on a Diet 14:05 - 14:30					RPLS P4-Based Automated Reasoning (P4-BAR) using Symbolic Execution at Google 14:30 - 14:55					RPLS Verification of WebAssembly Features 14:55 - 15:20									RPLS MiniRust: A Core Language for Specifying Rust 15:40 - 16:05					RPLSRemote Production Language Specification - Requirements for Multiple Usages 16:05 - 16:30					RPLS Panel: Mechanized Specifications for Real-World Programming Languages 16:30 - 17:30																																				PLDI Catering Dinner 19:30 - 21:30

Hide past events

Room information: Cosmos

This program is tentative and subject to change.

Mon 16 Jun
Displayed time zone: Seoul change

Tue 17 Jun
Displayed time zone: Seoul change

Mon 16 Jun
Displayed time zone: Seoul change

Sparse

Sparse

Sparse

Sparse

Tue 17 Jun
Displayed time zone: Seoul change

RPLS

RPLS

RPLS

RPLS

LCTES + Catering

Mon 16 Jun
Displayed time zone: Seoul change

Tue 17 Jun
Displayed time zone: Seoul change

Tracks

Co-hosted Conferences

Workshops

Room information: Cosmos

This program is tentative and subject to change.

Program Display Configuration

Mon 16 JunDisplayed time zone: Seoul change

Tue 17 JunDisplayed time zone: Seoul change

Mon 16 JunDisplayed time zone: Seoul change

Sparse

Sparse

Sparse

Sparse

Tue 17 JunDisplayed time zone: Seoul change

RPLS

RPLS

RPLS

RPLS

LCTES + Catering

Mon 16 JunDisplayed time zone: Seoul change

Tue 17 JunDisplayed time zone: Seoul change

Information for Participants

Mon 16 Jun
Displayed time zone: Seoul change

Tue 17 Jun
Displayed time zone: Seoul change

Mon 16 Jun
Displayed time zone: Seoul change

Tue 17 Jun
Displayed time zone: Seoul change

Mon 16 Jun
Displayed time zone: Seoul change

Tue 17 Jun
Displayed time zone: Seoul change