OLIVIERFEST 2025 – Proceedings

Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday (OLIVIERFEST 2025)

Controlling Copatterns: There and Back Again
Paul Downen
(University of Massachusetts at Lowell, USA)

Publisher's Version Published Artifact Info Artifacts Available Article: splashws25olivierfestmain-p3-p doi:10.1145/3759427.3760362

Danvy’s Mystery Functions in Slang
Stefan Hallerstede, Robby, and John Hatcliff
(Aarhus University, Denmark; Kansas State University, USA)

Publisher's Version Article: splashws25olivierfestmain-p14-p doi:10.1145/3759427.3760363

Defining Algebraic Effects and Handlers via Trails and Metacontinuations
Kenichi Asai and Maika Fujii
(Ochanomizu University, Japan)

Publisher's Version Article: splashws25olivierfestmain-p22-p doi:10.1145/3759427.3760364

Simple Closure Analysis Revisited
Fritz Henglein
(University of Copenhagen, Denmark)

Publisher's Version Article: splashws25olivierfestmain-p26-p doi:10.1145/3759427.3760365

Redundancy Checking in Reversible Flowcharts via Logic-Based Operational Semantics
Robert Glück and Maurizio Proietti
(University of Copenhagen, Denmark; IASI-CNR, Italy)

Publisher's Version Article: splashws25olivierfestmain-p28-p doi:10.1145/3759427.3760366

Continuations in Music
Youyou Cong
(Institute of Science Tokyo, Japan)

Publisher's Version Article: splashws25olivierfestmain-p33-p doi:10.1145/3759427.3760367

On the Structure of Abstract Interpreters
Wonyeol Lee, Matthieu Lemerre, Xavier Rival, and Hongseok Yang
(POSTECH, Republic of Korea; Université Paris-Saclay - CEA List, France; Inria - CNRS - Ecole Normale Superieure de Paris - PSL University, France; KAIST, Republic of Korea)

Publisher's Version Article: splashws25olivierfestmain-p35-p doi:10.1145/3759427.3760368

A Compositional Semantics for eval in Scheme
Peter D. Mosses
(Delft University of Technology, Netherlands; Swansea University, UK)

Publisher's Version Published Artifact Artifacts Available Article: splashws25olivierfestmain-p38-p doi:10.1145/3759427.3760369

How to Fold a Tree: Programming Exercises on Calder’s Mobiles
Thibaut Balabonski
(Université Paris-Saclay - CNRS - ENS Paris-Saclay - LMF, France)

Publisher's Version Article: splashws25olivierfestmain-p39-p doi:10.1145/3759427.3760370

Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_core
Julia Lawall, Keisuke Nishimura, and Jean-Pierre Lozi
(Inria, France)

Publisher's Version Published Artifact Artifacts Available Article: splashws25olivierfestmain-p43-p doi:10.1145/3759427.3760371

Verified Nanopasses for Compiling Conditionals
Jeremy G. Siek
(Indiana University, USA)

Publisher's Version Published Artifact Artifacts Available Article: splashws25olivierfestmain-p44-p doi:10.1145/3759427.3760372

What I Always Wanted to Know about Second Class Values
Peter Thiemann
(University of Freiburg, Germany)

Publisher's Version Published Artifact Artifacts Available Article: splashws25olivierfestmain-p50-p doi:10.1145/3759427.3760373

Untyped Logical Relations at Work: Control Operators, Contextual Equivalence and Full Abstraction
Patrycja Balik, Dariusz Biernacki, and Piotr Polesiuk
(University of Wrocław, Poland)

Publisher's Version Published Artifact Artifacts Available Article: splashws25olivierfestmain-p52-p doi:10.1145/3759427.3760374

Encoding Product Types
Sam Lindley
(University of Edinburgh, UK)

Publisher's Version Article: splashws25olivierfestmain-p62-p doi:10.1145/3759427.3760375

A Pair of tricks
Oleg Kiselyov
(Tohoku University, Japan)

Publisher's Version Info Article: splashws25olivierfestmain-p64-p doi:10.1145/3759427.3760376

Generic Reduction-Based Interpreters
Casper Bach
(University of Southern Denmark, Denmark)

Publisher's Version Published Artifact Artifacts Available Article: splashws25olivierfestmain-p83-p doi:10.1145/3759427.3760377

Property-Based Testing of OCaml 5’s Runtime System: Fun and Segfaults with Interpreters and State Transition Functions
Jan Midtgaard
(Independent, Denmark)

Publisher's Version Article: splashws25olivierfestmain-p84-p doi:10.1145/3759427.3760378

Safe-for-Space Linked Environments
Matthew Flatt and Robert Bruce Findler
(University of Utah, USA; Northwestern University, USA)

Publisher's Version Article: splashws25olivierfestmain-p86-p doi:10.1145/3759427.3760379

Towards Metaprogramming Defunctionalization in Rocq
Chantal Keller and Camille Noûs
(LMF - University Paris-Saclay, France; Laboratoire Cogitamus - Université Publique, France)

Publisher's Version Article: splashws25olivierfestmain-p88-p doi:10.1145/3759427.3760380

Invertible Syntax without the Tuples (Functional Pearl)
Mathieu Boespflug and Arnaud Spiwack
(Tweag, France)

Publisher's Version Article: splashws25olivierfestmain-p89-p doi:10.1145/3759427.3760381

Functional Programming and Computational Quantum Structures
Jerzy Karczmarczuk
(University of Caen, France)

Publisher's Version Published Artifact Artifacts Available Article: splashws25olivierfestmain-p91-p doi:10.1145/3759427.3760382

A Tale of Two Zippers
Philip Wadler, Ramsay Taylor, and Jacco O.G. Krijnen
(IOG, UK; University of Edinburgh, UK; Utrecht University, Netherlands)

Publisher's Version Published Artifact Artifacts Available Article: splashws25olivierfestmain-p94-p doi:10.1145/3759427.3760383

proc time: 0.03