Cosmos - PLDI 2025

VenueThe Westin Josun Seoul

Room nameCosmos

Floor2

Room InformationNo extra information available

Program

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 File Attached
09:40 25m Talk		Lightweight Semantics Engineering with Redex RPLS Matthew Flatt University of Utah File Attached

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 File Attached
10:55 25m Talk		Trusted JavaScript Language Environments with ESMeta RPLS Jihyeok Park Korea University File Attached
11:20 25m Talk		The Software Supporting the JavaScript Language Specification RPLS Michael Ficarra F5 File Attached

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 File Attached
14:30 25m Talk		P4-Based Automated Reasoning (P4-BAR) using Symbolic Execution at Google RPLS Jonathan DiLorenzo Google File Attached
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 File Attached
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

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

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

Room information: Cosmos

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

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