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 (type: Full Paper) doi:10.1145/3759427.3760362

Semantic Artifacts for "Controlling Copatterns: There and Back Again" (doi:10.5281/zenodo.16888452): The various semantic artifacts --- operational semantics, abstract machines, and continuation-passing style transformations --- for specifying the behavior of composable copatterns can be derived in a step-by-step manner using the techniques developed by Olivier Danvy. This artifact includes each step in the ...

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 (type: Full Paper) 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 (type: Full Paper) doi:10.1145/3759427.3760364

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

Publisher's Version Article: splashws25olivierfestmain-p26-p (type: Full Paper) 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 (type: Full Paper) doi:10.1145/3759427.3760366

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

Publisher's Version Article: splashws25olivierfestmain-p33-p (type: Full Paper) 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 (type: Full Paper) 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 (type: Full Paper) doi:10.1145/3759427.3760369

olivierfest-agda (doi:10.1145/3747409): The Agda code in the artifact is a lightweight formalization of the denotational semantics of the language ScmQE defined in the paper *A Compositional Semantics for `eval` in Scheme*. The artifact includes a PDF of a highlighted listing of the Agda code, generated using Agda.

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 (type: Full Paper) 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 (type: Full Paper) doi:10.1145/3759427.3760371

	Version of Record: Version of Record to "Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_core" by Julia Lawall, Keisuke Nishimura, and Jean-Pierre Lozi, Proceedings of the Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday (OLIVIERFEST ’25), 2025, ...
	Reproduction package for Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_core (doi:10.5281/zenodo.16842821): The artifact contains the code discussed in the paper. Makefiles are provided for reproducing the experiments.

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

Publisher's Version Published Artifact Artifacts Available Article: splashws25olivierfestmain-p44-p (type: Full Paper) doi:10.1145/3759427.3760372

Verified Nanopasses for Compiling Conditionals (doi:10.5281/zenodo.16890248): The LIf language includes conditionals, Booleans, let binding, and integers. The definition of the LIf language, including the interpreter, is in LIf2.agda That file includes the definition of the intermediate languages and the target x86-like language X86If. The compiler from LIf to X86If is also defined in ...

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 (type: Full Paper) doi:10.1145/3759427.3760373

Proof scripts for "What I Always Wanted to Know About Second Class Values (doi:10.5281/zenodo.16812692): Contains the full Agda source code for the theory presented in the paper.

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 (type: Full Paper) doi:10.1145/3759427.3760374

Formalization for Article "Untyped Logical Relations at Work: Control Operators, Contextual Equivalence and Full Abstraction" (doi:10.5281/zenodo.16875429): This is the Coq formalization accompanying the paper “Untyped Logical Relations at Work: Control Operators, Contextual Equivalence and Full Abstraction”. Refer to the README for a description of how the formalization corresponds to the sections of the paper.

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

Publisher's Version Article: splashws25olivierfestmain-p62-p (type: Full Paper) doi:10.1145/3759427.3760375

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

Publisher's Version Info Article: splashws25olivierfestmain-p64-p (type: Full Paper) doi:10.1145/3759427.3760376

Complete source code accompanying the article ``A Pair of Tricks': Two OCaml source code files, with the complete code for the article plus many tests. (Part of the code requires MetaOCaml}.

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

Publisher's Version Published Artifact Artifacts Available Article: splashws25olivierfestmain-p83-p (type: Full Paper) doi:10.1145/3759427.3760377

Generic Reduction-Based Interpreters - Literate Agda Files (doi:10.1145/3747407): The literate Agda files accompanying the paper "Generic Reduction-Based Interpreters". Reduction-based interpreters are traditionally defined in terms of a one-step reduction function which systematically decomposes a term into a potential redex and context, contracts the redex, and recomposes it to construct the new ...

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 (type: Full Paper) 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 (type: Full Paper) 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 (type: Full Paper) 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 (type: Full Paper) 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 (type: Full Paper) doi:10.1145/3759427.3760382

Functional Simulation Tools for Simple Quantum Systems (doi:10.1145/3747408): This is the source code for an interactive workbench containing commented Haskell functions, classes and some elementary data permitting to execute and modify the programs included in the article "Functional Programming and Computational Quantum Structures".

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 (type: Full Paper) doi:10.1145/3759427.3760383

Executable Agda Script for ‘A Tale of Two Zippers’ (doi:10.1145/3747406): Executable Agda script for ‘A Tale of Two Zippers’.

proc time: 0.05