ARLI @ ICFP/SPLASH 2025
We have a LOT of work at ICFP/OOPSLA this year! Here’s a quick run-down of that work.
|
|
First time at a conference? Confused and unsure how it’s going to go, or what to do? Come to this talk to hear some advice on how to make the most out of your limited time at a conference. You’ll get concrete ideas and practice on creating connections, scheduling your time, and listening to talks. |
|
00:00 Sun, October 12 |
|
||||
|
|
|
|
|||||||
|
|
Unsure about the trade-offs between different methods for deciding definitional equality? We present preliminary work on a platform for comparing the run-time performance of type-directed vs syntax-directed definitional equality decision procedures, and some performance numbers that give hope for type-directed methods. |
|
00:00 Sun, October 12 |
|
||||
|
|
|
|
|||||||
|
|
We deconstruct the space of mutable higher-order references, and in turn deconstruct your mind. Come see the weird connection between a type universe hierarchy, à la dependent type theory, and Kripke worlds, used in possible-worlds models of mutable references. We find that type universes are a lightweight syntactic mechanism to design and restrict heap shapes. Find the details here: https://icfp25.sigplan.org/details/icfp-2025-papers/28/Type-Universes-as-Kripke-Worlds |
|
14:55 Tue, October 14 |
|
||||
|
|
|
|
|||||||
|
|
An extended version of the Type Universes as Kripke Worlds ICFP talk, with a focus on discussing whether type universes are a promising alternative to region type and effect systems for static memory management. |
|
00:00 Tue, October 14 |
|
||||
|
|
|
|
|||||||
|
|
Introducing the Flat Closure Calculus (FCC), a typed intermediate language that admits many state-of-the-art practical closure optimizations (notably, an optimized closure representation) not permitted by past work on typed closure conversion. Find the details here: https://2025.splashcon.org/details/OOPSLA/34/Type-Preserving-Flat-Closure-Optimization |
|
15:15 Fri, October 17 |
|
||||
|
|
|
|
|||||||
|
|
Building new languages requires iteration, so researchers built language workbenches that made it easy to extend and iterate upon language implementations. But, for new languages to be useful, they need to be performant too. With micro embeddings, we can build languages which are both performant and extensible. Find the details here: https://conf.researchr.org/details/icfp-splash-2025/scheme-2025-papers/9/Fast-and-Extensible-Hybrid-Embeddings-with-Micros |
|
14:10 Thu, October 16 |
|
