PEPM '25: "Algebraic Stepper for Simple ..."
Algebraic Stepper for Simple Modules
Kenichi Asai and Hinano Akiyama
(Ochanomizu University, Japan)
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.
Article Search
PEPM '25: "Characterizations of Partial ..."
Characterizations of Partial Well-Behaved Lenses
Keishi Hashiba, Keisuke Nakano, Kazuyuki Asada, and Kentaro Kikuchi
(University of Osaka, Japan; Tohoku University, Japan)
Article Search
PEPM '25: "Algebraic Stepper for Simple ..."
Algebraic Stepper for Simple Modules
Kenichi Asai and Hinano Akiyama
(Ochanomizu University, Japan)
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.
Article Search
PEPM '25: "A Type Safe Calculus for Generating ..."
A Type Safe Calculus for Generating Syntax-Directed Editors
Benjamin Bennetzen, Sune Skaaning Engtorp, Hans Hüttel, Nikolaj Rossander Kristensen, Andreas Tor Mortensen, and Peter Buus Steffensen
(Aalborg University, Denmark; University of Copenhagen, Denmark)
Editor calculi make it possible to describe the actions of syntax-directed editing and provide guarantees of safety through their specialized type system: Well-typed editor scripts produce well-formed programs. So far, such calculi have been language-specific. In this paper we present a generalized editor calculus, which can be used to specify a specialized syntax-directed editor for any language, given its abstract syntax. Moreover we show how to implement an editor generator that allows one to generate an editor calculus-based syntax-directed editor from a language specification. The generalized editor calculus can be encoded into a simply typed lambda calculus, extended with pairs, booleans, pattern matching and fixed points. This implies a general type safety result that holds for any instantiation.
Article Search
PEPM '25: "The Ethical Compiler: Addressing ..."
The Ethical Compiler: Addressing the Is-Ought Gap in Compilation (Invited Talk)
William J. Bowman
(University of British Columbia, Canada)
Article Search
PEPM '25: "A Type Safe Calculus for Generating ..."
A Type Safe Calculus for Generating Syntax-Directed Editors
Benjamin Bennetzen, Sune Skaaning Engtorp, Hans Hüttel, Nikolaj Rossander Kristensen, Andreas Tor Mortensen, and Peter Buus Steffensen
(Aalborg University, Denmark; University of Copenhagen, Denmark)
Editor calculi make it possible to describe the actions of syntax-directed editing and provide guarantees of safety through their specialized type system: Well-typed editor scripts produce well-formed programs. So far, such calculi have been language-specific. In this paper we present a generalized editor calculus, which can be used to specify a specialized syntax-directed editor for any language, given its abstract syntax. Moreover we show how to implement an editor generator that allows one to generate an editor calculus-based syntax-directed editor from a language specification. The generalized editor calculus can be encoded into a simply typed lambda calculus, extended with pairs, booleans, pattern matching and fixed points. This implies a general type safety result that holds for any instantiation.
Article Search
PEPM '25: "Characterizations of Partial ..."
Characterizations of Partial Well-Behaved Lenses
Keishi Hashiba, Keisuke Nakano, Kazuyuki Asada, and Kentaro Kikuchi
(University of Osaka, Japan; Tohoku University, Japan)
Article Search
PEPM '25: "A Type Safe Calculus for Generating ..."
A Type Safe Calculus for Generating Syntax-Directed Editors
Benjamin Bennetzen, Sune Skaaning Engtorp, Hans Hüttel, Nikolaj Rossander Kristensen, Andreas Tor Mortensen, and Peter Buus Steffensen
(Aalborg University, Denmark; University of Copenhagen, Denmark)
Editor calculi make it possible to describe the actions of syntax-directed editing and provide guarantees of safety through their specialized type system: Well-typed editor scripts produce well-formed programs. So far, such calculi have been language-specific. In this paper we present a generalized editor calculus, which can be used to specify a specialized syntax-directed editor for any language, given its abstract syntax. Moreover we show how to implement an editor generator that allows one to generate an editor calculus-based syntax-directed editor from a language specification. The generalized editor calculus can be encoded into a simply typed lambda calculus, extended with pairs, booleans, pattern matching and fixed points. This implies a general type safety result that holds for any instantiation.
Article Search
PEPM '25: "Typed Program Analysis without ..."
Typed Program Analysis without Encodings
Barry Jay
(n.n., Australia)
Article Search
PEPM '25: "Characterizations of Partial ..."
Characterizations of Partial Well-Behaved Lenses
Keishi Hashiba, Keisuke Nakano, Kazuyuki Asada, and Kentaro Kikuchi
(University of Osaka, Japan; Tohoku University, Japan)
Article Search
PEPM '25: "A Type Safe Calculus for Generating ..."
A Type Safe Calculus for Generating Syntax-Directed Editors
Benjamin Bennetzen, Sune Skaaning Engtorp, Hans Hüttel, Nikolaj Rossander Kristensen, Andreas Tor Mortensen, and Peter Buus Steffensen
(Aalborg University, Denmark; University of Copenhagen, Denmark)
Editor calculi make it possible to describe the actions of syntax-directed editing and provide guarantees of safety through their specialized type system: Well-typed editor scripts produce well-formed programs. So far, such calculi have been language-specific. In this paper we present a generalized editor calculus, which can be used to specify a specialized syntax-directed editor for any language, given its abstract syntax. Moreover we show how to implement an editor generator that allows one to generate an editor calculus-based syntax-directed editor from a language specification. The generalized editor calculus can be encoded into a simply typed lambda calculus, extended with pairs, booleans, pattern matching and fixed points. This implies a general type safety result that holds for any instantiation.
Article Search
PEPM '25: "A Type Safe Calculus for Generating ..."
A Type Safe Calculus for Generating Syntax-Directed Editors
Benjamin Bennetzen, Sune Skaaning Engtorp, Hans Hüttel, Nikolaj Rossander Kristensen, Andreas Tor Mortensen, and Peter Buus Steffensen
(Aalborg University, Denmark; University of Copenhagen, Denmark)
Editor calculi make it possible to describe the actions of syntax-directed editing and provide guarantees of safety through their specialized type system: Well-typed editor scripts produce well-formed programs. So far, such calculi have been language-specific. In this paper we present a generalized editor calculus, which can be used to specify a specialized syntax-directed editor for any language, given its abstract syntax. Moreover we show how to implement an editor generator that allows one to generate an editor calculus-based syntax-directed editor from a language specification. The generalized editor calculus can be encoded into a simply typed lambda calculus, extended with pairs, booleans, pattern matching and fixed points. This implies a general type safety result that holds for any instantiation.
Article Search
PEPM '25: "Characterizations of Partial ..."
Characterizations of Partial Well-Behaved Lenses
Keishi Hashiba, Keisuke Nakano, Kazuyuki Asada, and Kentaro Kikuchi
(University of Osaka, Japan; Tohoku University, Japan)
Article Search
PEPM '25: "A Type-Theoretic Framework ..."
A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract)
Brigitte Pientka
(McGill University, Canada)
Article Search
PEPM '25: "The Missing Diagonal: High ..."
The Missing Diagonal: High Level Languages for Low Level Systems (Invited Talk Abstract)
Satnam Singh
(Groq, USA)
Article Search
PEPM '25: "A Type Safe Calculus for Generating ..."
A Type Safe Calculus for Generating Syntax-Directed Editors
Benjamin Bennetzen, Sune Skaaning Engtorp, Hans Hüttel, Nikolaj Rossander Kristensen, Andreas Tor Mortensen, and Peter Buus Steffensen
(Aalborg University, Denmark; University of Copenhagen, Denmark)
Editor calculi make it possible to describe the actions of syntax-directed editing and provide guarantees of safety through their specialized type system: Well-typed editor scripts produce well-formed programs. So far, such calculi have been language-specific. In this paper we present a generalized editor calculus, which can be used to specify a specialized syntax-directed editor for any language, given its abstract syntax. Moreover we show how to implement an editor generator that allows one to generate an editor calculus-based syntax-directed editor from a language specification. The generalized editor calculus can be encoded into a simply typed lambda calculus, extended with pairs, booleans, pattern matching and fixed points. This implies a general type safety result that holds for any instantiation.
Article Search