Orchid West - ICFP 2025

VenueMarina Bay Sands Convention Centre

Room nameOrchid West

Floor4

Room number4302-4303

Capacity180

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

Mon 13 Oct
Displayed time zone: Perth change

10:50 - 12:05	ImplementationICFP Papers / JFP First Papers at Orchid West

10:50 25m Talk		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 25m Talk		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 25m Paper		OCaml Blockly JFP First Papers Kenichi Asai Ochanomizu University DOI

16:00 - 17:40	SemanticsJFP First Papers / ICFP Papers at Orchid West

16:00 25m Paper		A contextual formalization of structural coinduction JFP First Papers Paul Downen University of Massachusetts at Lowell, Zena M. Ariola University of Oregon DOI
16:25 25m Paper		A practical formalization of monadic equational reasoning in dependent-type theory JFP First Papers Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan, Jacques Garrigue , Takafumi Saikawa Nagoya University DOI
16:50 25m Talk		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 25m Talk		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

Tue 14 Oct
Displayed time zone: Perth change

10:50 - 12:05	Clever CompilationJFP First Papers / ICFP Papers at Orchid West

10:50 25m Talk		Compiling with Generating Functions ICFP Papers Jianlin Li University of Waterloo, Yizhou Zhang University of Waterloo DOI
11:15 25m Talk		Correctness Meets Performance: From Agda to Futhark ICFP Papers Artjoms Šinkarovs University of Southampton, Troels Henriksen University of Copenhagen DOI
11:40 25m Paper		Domain-specific tensor languages JFP First Papers Jean-Philippe Bernardy University of Gothenburg, Sweden, Patrik Jansson Chalmers University of Technology and University of Gothenbrug DOI

13:40 - 15:25	Applications and SRC TalksICFP Papers / ICFP Student Research Competition at Orchid West

13:40 25m Talk		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 25m Talk		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 25m Talk		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 30m Talk		SRC Talks ICFP Student Research Competition

Wed 15 Oct
Displayed time zone: Perth change

10:50 - 12:05	ConcurrencyICFP Papers at Orchid West

10:50 25m Talk		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 25m Talk		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 25m Talk		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

13:40 - 15:20	Types and SpecificationsICFP Papers / JFP First Papers at Orchid West

13:40 25m Talk		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 25m Talk		Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl) ICFP Papers Maximilian Doré University of Oxford DOI Pre-print
14:30 25m Paper		Binary search—think positive JFP First Papers Alexander Dinges RPTU Kaiserslautern-Landau, Ralf Hinze RPTU Kaiserslautern-Landau DOI
14:55 25m Talk		Teaching Software Specification (Experience Report) ICFP Papers Cameron Moy Northeastern University, Daniel Patterson Northeastern University DOI

Thu 16 Oct
Displayed time zone: Perth change

10:30 - 12:15	TheorySPLASH OOPSLA at Orchid West

10:30 15m Talk		Automated Discovery of Tactic Libraries for Interactive Theorem Proving SPLASH OOPSLA Yutong Xin The University of Texas at Austin, Jimmy Xin The University of Texas at Austin, Gabriel Poesia Stanford University, Noah D. Goodman Stanford University, Jocelyn Qiaochu Chen New York University, University of Alberta, Işıl Dillig University of Texas at Austin
10:45 15m Talk		Choreographic Quick Changes: First-Class Location (Set) Polymorphism SPLASH OOPSLA Ashley Samuelson University of Wisconsin-Madison, Andrew K. Hirsch University at Buffalo, SUNY, Ethan Cecchetti University of Wisconsin-Madison
11:00 15m Talk		Divide and Conquer: A Compositional Approach to Game-Theoretic Security SPLASH OOPSLA Ivana Bocevska TU Wien, Anja Petković Komel TU Wien, Vienna, Austria, Laura Kovács TU Wien, Sophie Rain Argot Collective, Michael Rawson University of Southampton
11:15 15m Talk		Efficient Decrease-And-Conquer Linearizability Monitoring SPLASH OOPSLA Zheng Han Lee National University of Singapore, Singapore, Umang Mathur National University of Singapore Pre-print
11:30 15m Talk		Liberating Merges via Apartness and Guarded Subtyping SPLASH OOPSLA Han Xu Princeton University, Xuejing Huang IRIF, Bruno C. d. S. Oliveira University of Hong Kong
11:45 15m Talk		The Simple Essence of Monomorphization SPLASH OOPSLA Matthew Lutze Aarhus University, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
12:00 15m Talk		What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures SPLASH OOPSLA Yichen Xu EPFL, Oliver Bračevac EPFL, LAMP, Nguyen Pham EPFL, LAMP, Martin Odersky EPFL Pre-print

13:45 - 15:30	ReasoningSPLASH OOPSLA at Orchid West

13:45 15m Talk		Characterizing Implementability of Global Protocols with Infinite States and Data SPLASH OOPSLA Elaine Li NYU, Felix Stutz University of Luxembourg, Luxembourg, Thomas Wies New York University, Damien Zufferey SonarSource
14:00 15m Talk		Checking Observational Correctness of Database Systems SPLASH OOPSLA Lauren Pick The Chinese University of Hong Kong, Amanda Xu University of Wisconsin-Madison, Ankush Desai Amazon Web Services, Sanjit A. Seshia University of California, Berkeley, Aws Albarghouthi University of Wisconsin-Madison
14:15 15m Talk		Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation SPLASH OOPSLA Radosław Jan Rowicki Technical University of Denmark, Adrian Francalanza University of Malta, Alceste Scalas Technical University of Denmark DOI Pre-print
14:30 15m Talk		Correct-By-Construction: Certified Individual Fairness through Neural Network Training SPLASH OOPSLA Ruihan Zhang Singapore Management University (SMU), Jun Sun Singapore Management University
14:45 15m Talk		Modular Reasoning about Global Variables and Their Initialization SPLASH OOPSLA João Pereira ETH Zurich, Isaac van Bakel ETH Zurich, Patricia Firlejczyk ETH Zurich, Marco Eilers ETH Zurich, Peter Müller ETH Zurich
15:00 15m Talk		P³: Reasoning about Patches via Product Programs SPLASH OOPSLA Arindam Sharma Imperial College London, Daniel Schemmel Imperial College London, Cristian Cadar Imperial College London
15:15 15m Talk		Reasoning about External Calls SPLASH OOPSLA Julian Mackay Kry10 Ltd, Sophia Drossopoulou Imperial College London, James Noble Independent. Wellington, NZ, Susan Eisenbach Imperial College London

16:00 - 17:30	Neural NetworkSPLASH OOPSLA at Orchid West

16:00 15m Talk		Convex Hull Approximation for Activation Functions SPLASH OOPSLA Zhongkui Ma The University of Queensland, Zihan Wang The University of Queensland and CSIRO's Data61, Guangdong Bai University of Queensland
16:15 15m Talk		Cost of Soundness in Mixed-Precision Tuning SPLASH OOPSLA Anastasia Isychev TU Wien, Debasmita Lohar Karlsruhe Institute of Technology
16:30 15m Talk		Finch: Sparse and Structured Tensor Programming with Control Flow SPLASH 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 15m Talk		MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution SPLASH 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 15m Talk		Quantization with Guaranteed Floating-Point Neural Network Classifications SPLASH OOPSLA Anan Kabaha Technion, Israel Institute of Technology, Dana Drachsler Cohen Technion
17:15 15m Talk		The Continuous Tensor Abstraction: Where Indices are Real SPLASH 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

Fri 17 Oct
Displayed time zone: Perth change

10:30 - 12:15	CalculusSPLASH OOPSLA at Orchid West

10:30 15m Talk		Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification SPLASH 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 15m Talk		Flexible and Expressive Typed Path Patterns for GQL SPLASH 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 15m Talk		Homomorphism Calculus for User-Defined Aggregations SPLASH OOPSLA Ziteng Wang University of Texas at Austin, Ruijie Fang University of Texas at Austin, Linus Zheng University of Texas at Austin, Dixin Tang University of Texas Austin, Işıl Dillig University of Texas at Austin Pre-print
11:15 15m Talk		HpC: A Calculus for Hybrid and Mobile Systems SPLASH 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 15m Talk		Notions of Stack-manipulating Computation and Relative Monads SPLASH OOPSLA Yuchen Jiang University of Michigan, Runze Xue University of Michigan; University of Cambridge; Indiana University, Max S. New University of Michigan
11:45 15m Talk		Peepco: Batch-Based Consistency Optimization SPLASH OOPSLA Ivan Kuraj Massachusetts Institute of Technology, Jack Feser Basis, Nadia Polikarpova University of California at San Diego, Armando Solar-Lezama Massachusetts Institute of Technology
12:00 15m Talk		Quantified Underapproximation via Labeled Bunches SPLASH 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

13:45 - 15:30	Type 1SPLASH OOPSLA at Orchid West

13:45 15m Talk		A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation With Constraint-Based Subtype Inference SPLASH OOPSLA Cunyuan Gao HKUST, Lionel Parreaux HKUST (The Hong Kong University of Science and Technology)
14:00 15m Talk		Meaning-Typed Programming: Language Abstraction and Runtime for Model-Integrated Applications SPLASH OOPSLA Jayanaka L. Dantanarayana University of Michigan, Yiping Kang University of Michigan, Kugesan Sivasothynathan Jaseci Labs, Christopher Clarke University of Michigan, Baichuan Li University of Michigan, Savini Kashmira University of Michigan, Krisztian Flautner University of Michigan, Lingjia Tang University of Michigan, Jason Mars University of Michigan
14:15 15m Talk		Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory SPLASH OOPSLA Yuyan Bao Augusta University, Songlin Jia Purdue University, USA, Guannan Wei Tufts University, Oliver Bračevac EPFL, LAMP, Tiark Rompf Purdue University
14:30 15m Talk		Qualified Types with Boolean Algebras SPLASH OOPSLA Edward Lee University of Waterloo; University of Toronto Scarborough, Jonathan Lindegaard Starup , Ondřej Lhoták University of Waterloo, Magnus Madsen Aarhus University
14:45 15m Talk		RestPi: Path-Sensitive Type Inference for REST APIs SPLASH OOPSLA Mark W. Aldrich Tufts University, Kyla H. Levin University of Massachusetts Amherst, USA, Michael Coblenz University of California, San Diego, Jeffrey S. Foster Tufts University
15:00 15m Talk		Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for Nominal Object-Oriented Generics SPLASH OOPSLA Ross Tate Independent Researcher and Consultant DOI Pre-print
15:15 15m Talk		Type-Preserving Flat Closure Optimization SPLASH OOPSLA Adam Geller Computer Science, University of British Columbia, Sean Bocirnea University of British Columbia, Chester Gould University of British Columbia, Paulette Koronkevich University of British Columbia, William J. Bowman University of British Columbia DOI

16:00 - 17:30	LanguagesSPLASH OOPSLA at Orchid West

16:00 15m Talk		A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo) SPLASH OOPSLA Kartik Chandra MIT, Tony Chen MIT, Joshua B. Tenenbaum Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology
16:15 15m Talk		Flix: A Design for Language-Integrated Datalog SPLASH OOPSLA Magnus Madsen Aarhus University, Ondřej Lhoták University of Waterloo
16:30 15m Talk		Large Language Model powered Symbolic Execution SPLASH OOPSLA Yihe Li National University of Singapore, Ruijie Meng National University of Singapore, Singapore, Gregory J. Duck National University of Singapore
16:45 15m Talk		Multi-Language Probabilistic Programming SPLASH OOPSLA Sam Stites Northeastern University, John Li Northeastern University, Steven Holtzen Northeastern University
17:00 15m Talk		Polymorphic Records for Dynamic Languages SPLASH OOPSLA Giuseppe Castagna CNRS; Université Paris Cité, Loïc Peyrot IMDEA Software Institute
17:15 15m Talk		ROSpec: A Domain-Specific Language for ROS-based Robot Software SPLASH 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 Media Attached

Sat 18 Oct
Displayed time zone: Perth change

10:30 - 12:15	Verification 2SPLASH OOPSLA at Orchid West

10:30 15m Talk		FO-Complete Program Verification for Heap Logics SPLASH 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 15m Talk		Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back SPLASH 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 15m Talk		Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification SPLASH OOPSLA Anan Kabaha Technion, Israel Institute of Technology, Dana Drachsler Cohen Technion
11:15 15m Talk		KestRel: Relational Verification Using E-Graphs for Program Alignment SPLASH OOPSLA Robert Dickerson Purdue University, Prasita Mukherjee Purdue University, Benjamin Delaware Purdue University
11:30 15m Talk		Laurel: Unblocking Automated Verification with Large Language Models SPLASH 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 15m Talk		Scaling Instruction-Selection Verification against Authoritative ISA Semantics SPLASH 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
12:00 15m Talk		Verification of Bit-Flip Attacks against Quantized Neural Networks SPLASH 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

13:45 - 15:30	Verification 3SPLASH OOPSLA at Orchid West

13:45 15m Talk		Automated Verification of Soundness of DNN Certifiers SPLASH OOPSLA Avaljot Singh UIUC, Yasmin Chandini Sarita UIUC, Charith Mendis University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research
14:00 15m Talk		Bolt-On Strong Consistency: Specification, Implementation, and Verification SPLASH OOPSLA Nicholas V. Lewchenko University of Colorado Boulder, Gowtham Kaki University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon
14:15 15m Talk		Memory-Safety Verification of Open Programs With Angelic Assumptions SPLASH OOPSLA Gourav Takhar Indian Institute of Technology - Kanpur, Baldip Bijlani Indian Institute of Technology Kanpur, Prantik Chatterjee MathWorks, Akash Lal Microsoft Research, Subhajit Roy IIT Kanpur
14:30 15m Talk		Mini-Batch Robustness Verification of Deep Neural Networks SPLASH OOPSLA Saar Tzour-Shaday Technion – Israel Institute of Technology, Dana Drachsler Cohen Technion
14:45 15m Talk		Revamping Verilog Semantics for Foundational Verification SPLASH OOPSLA Joonwon Choi Amazon Web Services, Jaewoo Kim KAIST, Jeehoon Kang FuriosaAI
15:00 15m Talk		Scalable Equivalence Checking and Verification of Shallow Quantum Circuits SPLASH OOPSLA Nengkun Yu Stony Brook University, USA, Xuan Du Trinh Stony Brook University, Thomas Reps University of Wisconsin-Madison
15:15 15m Talk		Structural temporal logic for mechanized program verification SPLASH OOPSLA Lef Ioannidis University of Pennsylvania, Yannick Zakowski Inria, Steve Zdancewic University of Pennsylvania, Sebastian Angel University of Pennsylvania

16:00 - 17:30	Verification 4SPLASH OOPSLA at Orchid West

16:00 15m Talk		Counterexample-Guided Inference of Modular Specifications SPLASH OOPSLA William Hallahan Binghamton, Ranjit Jhala University of California at San Diego, Ruzica Piskac Yale University
16:15 15m Talk		Embedding Quantum Program Verification into Dafny SPLASH 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 15m Talk		Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests SPLASH OOPSLA Kevin Guan Cornell University, Marcelo d'Amorim North Carolina State University, Owolabi Legunsen Cornell University
16:45 15m Talk		Interactive Bit Vector Reasoning using Verified Bitblasting SPLASH 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
17:00 15m Talk		Products of Recursive Programs for Hypersafety Verification SPLASH OOPSLA Ruotong Cheng University of Toronto, Azadeh Farzan University of Toronto

Mon 13 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 West											ICFP Papers + JFP First Papers Implementation																																		ICFP Papers																												JFP First Papers + ICFP Papers Semantics

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 West											JFP First Papers + ICFP Papers Clever Compilation																																		ICFP Papers + ICFP Student Research Competition Applications and SRC Talks																												ICFP Papers

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 West											ICFP Papers Concurrency																																		ICFP Papers + JFP First Papers Types and Specifications																												ICFP Papers

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 West							SPLASH OOPSLA Theory																																							SPLASH OOPSLA Reasoning																											SPLASH OOPSLA Neural Network

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 West							SPLASH OOPSLA Calculus																																							SPLASH OOPSLA Type 1																											SPLASH OOPSLA Languages

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 West							SPLASH OOPSLA Verification 2																																							SPLASH OOPSLA Verification 3																											SPLASH OOPSLA Verification 4

Mon 13 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 West											ICFP Papers Environment-Sharing Analysis and Caller-Provided Environments for Highe ... 10:50 - 11:15					ICFP Papers Multiple Resumptions and Local Mutable State, Directly 11:15 - 11:40					ICFP JFP First Papers OCaml Blockly 11:40 - 12:05																																																				ICFP JFP First Papers A contextual formalization of structural coinduction 16:00 - 16:25					ICFP JFP First Papers A practical formalization of monadic equational reasoning in dependent- ... 16:25 - 16:50					ICFP Papers Almost Fair Simulations 16:50 - 17:15					ICFP Papers Big Steps in Higher-Order Mathematical Operational Semantics 17:15 - 17:40

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
Orchid West											ICFP Papers Compiling with Generating Functions 10:50 - 11:15					ICFP Papers Correctness Meets Performance: From Agda to Futhark 11:15 - 11:40					ICFP JFP First Papers Domain-specific tensor languages 11:40 - 12:05																								ICFP Papers A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Qua ... 13:40 - 14:05					ICFP Papers Functional Networking for Millions of Docker Desktops (Experience Report) 14:05 - 14:30					ICFP Papers Polynomial-Time Program Equivalence for Machine Knitting 14:30 - 14:55					ICFP Student Research Competition SRC Talks 14:55 - 15:25

Wed 15 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
Orchid West											ICFP Papers Fusing Session-Typed Concurrent Programming into Functional Programming 10:50 - 11:15					ICFP Papers Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs 11:15 - 11:40					ICFP Papers Relax! The Semilenient Core of Choreographic Programming (Functional Pearl) 11:40 - 12:05																								ICFP Papers McTT: A Verified Kernel for a Proof Assistant 13:40 - 14:05					ICFP Papers Linear Types with Dynamic Multiplicities in Dependent Type Theory (Func ... 14:05 - 14:30					ICFP JFP First Papers Binary search—think positive 14:30 - 14:55					ICFP Papers Teaching Software Specification (Experience Report) 14:55 - 15:20

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 West							SPLASH OOPSLA Automated Discovery of Tactic Libraries for Interactive Theorem Proving 10:30 - 10:45			SPLASH OOPSLA Choreographic Quick Changes: First-Class Location (Set) Polymorphism 10:45 - 11:00			SPLASH OOPSLA Divide and Conquer: A Compositional Approach to Game-Theoretic Security 11:00 - 11:15			SPLASH OOPSLA Efficient Decrease-And-Conquer Linearizability Monitoring 11:15 - 11:30			SPLASH OOPSLA Liberating Merges via Apartness and Guarded Subtyping 11:30 - 11:45			SPLASH OOPSLA The Simple Essence of Monomorphization 11:45 - 12:00			SPLASH OOPSLA What's in the Box: Ergonomic and Expressive Capture Tracking over Gener ... 12:00 - 12:15																					SPLASH OOPSLA Characterizing Implementability of Global Protocols with Infinite State ... 13:45 - 14:00			SPLASH OOPSLA Checking Observational Correctness of Database Systems 14:00 - 14:15			SPLASH OOPSLA Correct Black-Box Monitors for Distributed Deadlock Detection: Formalis ... 14:15 - 14:30			SPLASH OOPSLA Correct-By-Construction: Certified Individual Fairness through Neural N ... 14:30 - 14:45			SPLASH OOPSLA Modular Reasoning about Global Variables and Their Initialization 14:45 - 15:00			SPLASH OOPSLA P³: Reasoning about Patches via Product Programs 15:00 - 15:15			SPLASH OOPSLA Reasoning about External Calls 15:15 - 15:30									SPLASH OOPSLA Convex Hull Approximation for Activation Functions 16:00 - 16:15			SPLASH OOPSLA Cost of Soundness in Mixed-Precision Tuning 16:15 - 16:30			SPLASH OOPSLA Finch: Sparse and Structured Tensor Programming with Control Flow 16:30 - 16:45			SPLASH OOPSLA MetaKernel: Enabling Efficient Encrypted Neural Network Inference Throu ... 16:45 - 17:00			SPLASH OOPSLA Quantization with Guaranteed Floating-Point Neural Network Classifications 17:00 - 17:15			SPLASH OOPSLA The Continuous Tensor Abstraction: Where Indices are Real 17:15 - 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 West							SPLASH OOPSLA Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simp ... 10:30 - 10:45			SPLASH OOPSLA Flexible and Expressive Typed Path Patterns for GQL 10:45 - 11:00			SPLASH OOPSLA Homomorphism Calculus for User-Defined Aggregations 11:00 - 11:15			SPLASH OOPSLA HpC: A Calculus for Hybrid and Mobile Systems 11:15 - 11:30			SPLASH OOPSLA Notions of Stack-manipulating Computation and Relative Monads 11:30 - 11:45			SPLASH OOPSLA Peepco: Batch-Based Consistency Optimization 11:45 - 12:00			SPLASH OOPSLA Quantified Underapproximation via Labeled Bunches 12:00 - 12:15																					SPLASH OOPSLA A Lightweight Type-and-Effect System for Invalidation Safety: Tracking ... 13:45 - 14:00			SPLASH OOPSLA Meaning-Typed Programming: Language Abstraction and Runtime for Model-I ... 14:00 - 14:15			SPLASH OOPSLA Modeling Reachability Types with Logical Relations -- Semantic Type Sou ... 14:15 - 14:30			SPLASH OOPSLA Qualified Types with Boolean Algebras 14:30 - 14:45			SPLASH OOPSLA RestPi: Path-Sensitive Type Inference for REST APIs 14:45 - 15:00			SPLASH OOPSLA Type-Outference with Label-Listeners: Foundations for Decidable Type-Co ... 15:00 - 15:15			SPLASH OOPSLA Type-Preserving Flat Closure Optimization 15:15 - 15:30									SPLASH OOPSLA A Domain-Specific Probabilistic Programming Language for Reasoning abou ... 16:00 - 16:15			SPLASH OOPSLA Flix: A Design for Language-Integrated Datalog 16:15 - 16:30			SPLASH OOPSLA Large Language Model powered Symbolic Execution 16:30 - 16:45			SPLASH OOPSLA Multi-Language Probabilistic Programming 16:45 - 17:00			SPLASH OOPSLA Polymorphic Records for Dynamic Languages 17:00 - 17:15			SPLASH OOPSLA ROSpec: A Domain-Specific Language for ROS-based Robot Software 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 West							SPLASH OOPSLA FO-Complete Program Verification for Heap Logics 10:30 - 10:45			SPLASH OOPSLA Foundations for Deductive Verification of Continuous Probabilistic Prog ... 10:45 - 11:00			SPLASH OOPSLA Guarding the Privacy of Label-Only Access to Neural Network Classifiers ... 11:00 - 11:15			SPLASH OOPSLA KestRel: Relational Verification Using E-Graphs for Program Alignment 11:15 - 11:30			SPLASH OOPSLA Laurel: Unblocking Automated Verification with Large Language Models 11:30 - 11:45			SPLASH OOPSLA Scaling Instruction-Selection Verification against Authoritative ISA Se ... 11:45 - 12:00			SPLASH OOPSLA Verification of Bit-Flip Attacks against Quantized Neural Networks 12:00 - 12:15																					SPLASH OOPSLA Automated Verification of Soundness of DNN Certifiers 13:45 - 14:00			SPLASH OOPSLA Bolt-On Strong Consistency: Specification, Implementation, and Verification 14:00 - 14:15			SPLASH OOPSLA Memory-Safety Verification of Open Programs With Angelic Assumptions 14:15 - 14:30			SPLASH OOPSLA Mini-Batch Robustness Verification of Deep Neural Networks 14:30 - 14:45			SPLASH OOPSLA Revamping Verilog Semantics for Foundational Verification 14:45 - 15:00			SPLASH OOPSLA Scalable Equivalence Checking and Verification of Shallow Quantum Circuits 15:00 - 15:15			SPLASH OOPSLA Structural temporal logic for mechanized program verification 15:15 - 15:30									SPLASH OOPSLA Counterexample-Guided Inference of Modular Specifications 16:00 - 16:15			SPLASH OOPSLA Embedding Quantum Program Verification into Dafny 16:15 - 16:30			SPLASH OOPSLA Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verif ... 16:30 - 16:45			SPLASH OOPSLA Interactive Bit Vector Reasoning using Verified Bitblasting 16:45 - 17:00			SPLASH OOPSLA Products of Recursive Programs for Hypersafety Verification 17:00 - 17:15

Room information: Orchid West

This program is tentative and subject to change.

Program Display Configuration

Mon 13 OctDisplayed time zone: Perth change

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

Mon 13 OctDisplayed time zone: Perth change

ICFP Papers + JFP First Papers

ICFP Papers

JFP First Papers + ICFP Papers

Tue 14 OctDisplayed time zone: Perth change

JFP First Papers + ICFP Papers

ICFP Papers + ICFP Student Research Competition

ICFP Papers

Wed 15 OctDisplayed time zone: Perth change

ICFP Papers

ICFP Papers + JFP First Papers

ICFP Papers

Thu 16 OctDisplayed time zone: Perth change

SPLASH OOPSLA

SPLASH OOPSLA

SPLASH OOPSLA

Fri 17 OctDisplayed time zone: Perth change

SPLASH OOPSLA

SPLASH OOPSLA

SPLASH OOPSLA

Sat 18 OctDisplayed time zone: Perth change

SPLASH OOPSLA

SPLASH OOPSLA

SPLASH OOPSLA

Mon 13 OctDisplayed time zone: Perth change

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

Mon 13 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

Mon 13 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

Mon 13 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