Algebraic Stepper for Simple Modules
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
11:00 - 12:30 | Language design, pedagogical tool, and staged interpreterPEPM at Room 6 Chair(s): Sam Lindley The University of Edinburgh | ||
11:00 45mKeynote | The Ethical Compiler: Addressing the Is-Ought Gap in Compilation (Invited Talk) PEPM William J. Bowman University of British Columbia DOI Pre-print | ||
11:45 30mResearch paper | Algebraic Stepper for Simple Modules PEPM | ||
12:15 15mShort-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 |