POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

An algebraic stepper is a pedagogical tool for showing the

intermediate steps of program execution.

This paper presents an algebraic stepper for OCaml that supports

simple modules with hierarchical reference to variables

(but without functors or signature sealing).

When we program with modules,

we can refer to a variable declared in a parent module directly,

whereas we need to specify a module path to refer to a

variable declared in a child module.

Therefore, when we build the stepper,

we attach a level to each variable (bound by let statement

without in)

and use it to maintain correct reference regardless of

where a variable is used.

In this paper, we present and formalize our stepper that implements

delayed substitution of variables, and discuss the interplay

between the stepper semantics and the level maintenance.

We further show that the execution in the stepper semantics is

consistent with the one in the standard small-step semantics.

The resulting stepper is implemented, supporting most of the basic

constructs of OCaml, and is used in an introductory OCaml course in

the authors' institution.

Tue 21 Jan

Displayed time zone: Mountain Time (US & Canada) change

11:00 - 12:30
Language design, pedagogical tool, and staged interpreterPEPM at Scissors
Chair(s): Michael Hanus Kiel University
11:00
45m
Keynote
The Ethical Compiler: Addressing the Is-Ought Gap in Compilation (Invited Talk)
PEPM
William J. Bowman University of British Columbia
DOI Pre-print File Attached
11:45
30m
Research paper
Algebraic Stepper for Simple Modules
PEPM
Kenichi Asai Ochanomizu University, Hinano Akiyama Ochanomizu University
DOI
12:15
15m
Short-paper
Collapsing Towers for Side-Channel Security (Short Paper)
PEPM
Cameron Wong Harvard SEAS, Muhammad Abdullah MIT, Yuheng Yang MIT, Mengjia Yan MIT, Adam Chlipala Massachusetts Institute of Technology, Nada Amin Harvard University
File Attached