Workshop PEPM 2024 – Author Index 
Contents 
Abstracts 
Authors

A B C D E F G H K L M N P S T V
Allais, Guillaume 
PEPM '24: "Scoped and Typed Staging by ..."
Scoped and Typed Staging by Evaluation
Guillaume Allais (University of Strathclyde, UK) Using a dependently typed host language, we give a well scopedandtyped by construction presentation of a minimal two level simply typed calculus with a static and a dynamic stage. The staging function partially evaluating the parts of a term that are static is obtained by a model construction inspired by normalisation by evaluation. We then go on to demonstrate how this minimal language can be extended to provide additional metaprogramming capabilities, and to define a higher order functional language evaluating to digital circuit descriptions. @InProceedings{PEPM24p83, author = {Guillaume Allais}, title = {Scoped and Typed Staging by Evaluation}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {8393}, doi = {10.1145/3635800.3636964}, year = {2024}, } Publisher's Version 

Berezun, Daniil 
PEPM '24: "A Case Study in Functional ..."
A Case Study in Functional Conversion and Mode Inference in miniKanren
Ekaterina Verbitskaia, Igor Engel, and Daniil Berezun (JetBrains Research, Serbia; Constructor University Bremen, Germany; JetBrains Research, Germany; JetBrains Research, Netherlands) Many programs which solve complicated problems can be seen as inversions of other, much simpler, programs. One particular example is transforming verifiers into solvers, which can be achieved with low effort by implementing the verifier in a relational language and then executing it in the backward direction. Unfortunately, as it is common with inverse computations, interpretation overhead may lead to subpar performance compared to direct program inversion. In this paper we discuss functional conversion aimed at improving relational miniKanren specifications with respect to a known fixed direction. Our preliminary evaluation demonstrates a significant performance increase for some programs which exemplify the approach. @InProceedings{PEPM24p107, author = {Ekaterina Verbitskaia and Igor Engel and Daniil Berezun}, title = {A Case Study in Functional Conversion and Mode Inference in miniKanren}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {107118}, doi = {10.1145/3635800.3636966}, year = {2024}, } Publisher's Version 

Bjørner, Dines 
PEPM '24: "The 0'th PEPM Event: October ..."
The 0'th PEPM Event: October 1987—and Andrei Petrovich Ershov: 1977–1988 (Invited Contribution)
Dines Bjørner (DTU, Denmark) An attempt is made to record events leading up to the The 0'th PEPM Event: the October 1987 Partial Evaluation and Mixed Computation IFIP TC2 Working Conference at Gl. Avernæs, Denmark. @InProceedings{PEPM24p53, author = {Dines Bjørner}, title = {The 0'th PEPM Event: October 1987—and Andrei Petrovich Ershov: 1977–1988 (Invited Contribution)}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {5356}, doi = {10.1145/3635800.3637448}, year = {2024}, } Publisher's Version 

Cong, Youyou 
PEPM '24: "An Intrinsically Typed Compiler ..."
An Intrinsically Typed Compiler for Algebraic Effect Handlers
Syouki Tsuyama, Youyou Cong, and Hidehiko Masuhara (Tokyo Institute of Technology, Japan) A typepreserving compiler converts a welltyped input program into a welltyped output program. Previous studies have developed typepreserving compilers for various source languages, including the simplytyped lambda calculus and calculi with control constructs. Our goal is to realize typepreserving compilation of languages that have facilities for manipulating firstclass continuations. In this paper, we focus on algebraic effects and handlers, a generalization of exceptions and their handlers with resumable continuations. Specifically, we choose an effect handler calculus and a typed stackmachinebased assembly language as the source and the target languages, respectively, and formalize the target language and a type preserving compiler. The main challenge posed by firstclass continuation is how to ensure safety of continuation capture and resumption, which involves concatenation of unknown stacks. We solve this challenge by incorporating stack polymorphism, a technique that has been used for compilation from a language without firstclass continuations to a stackbased assembly language. To prove that our compiler is type preserving, we implemented the compiler in Agda as a function between intrinsically typed ASTs. We believe that our contributions could lead to correct and efficient compilation of continuationmanipulating facilities in general. @InProceedings{PEPM24p134, author = {Syouki Tsuyama and Youyou Cong and Hidehiko Masuhara}, title = {An Intrinsically Typed Compiler for Algebraic Effect Handlers}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {134145}, doi = {10.1145/3635800.3636968}, year = {2024}, } Publisher's Version 

De Angelis, Emanuele 
PEPM '24: "A Historical Perspective on ..."
A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)
Alberto Pettorossi, Maurizio Proietti, Fabio Fioravanti, and Emanuele De Angelis (University of Rome Tor Vergata, Italy; IASICNR, Italy; University of ChietiPescara, Italy) This paper presents some ideas concerning program manipulation and program transformation from the early days of their development. Particular emphasis will be given to program transformation techniques in the area of functional programming and constraint logic programming. We will also indicate current applications of program transformation techniques to the verification of program properties and program synthesis. @InProceedings{PEPM24p16, author = {Alberto Pettorossi and Maurizio Proietti and Fabio Fioravanti and Emanuele De Angelis}, title = {A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {1638}, doi = {10.1145/3635800.3637446}, year = {2024}, } Publisher's Version 

Engel, Igor 
PEPM '24: "A Case Study in Functional ..."
A Case Study in Functional Conversion and Mode Inference in miniKanren
Ekaterina Verbitskaia, Igor Engel, and Daniil Berezun (JetBrains Research, Serbia; Constructor University Bremen, Germany; JetBrains Research, Germany; JetBrains Research, Netherlands) Many programs which solve complicated problems can be seen as inversions of other, much simpler, programs. One particular example is transforming verifiers into solvers, which can be achieved with low effort by implementing the verifier in a relational language and then executing it in the backward direction. Unfortunately, as it is common with inverse computations, interpretation overhead may lead to subpar performance compared to direct program inversion. In this paper we discuss functional conversion aimed at improving relational miniKanren specifications with respect to a known fixed direction. Our preliminary evaluation demonstrates a significant performance increase for some programs which exemplify the approach. @InProceedings{PEPM24p107, author = {Ekaterina Verbitskaia and Igor Engel and Daniil Berezun}, title = {A Case Study in Functional Conversion and Mode Inference in miniKanren}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {107118}, doi = {10.1145/3635800.3636966}, year = {2024}, } Publisher's Version 

Fioravanti, Fabio 
PEPM '24: "A Historical Perspective on ..."
A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)
Alberto Pettorossi, Maurizio Proietti, Fabio Fioravanti, and Emanuele De Angelis (University of Rome Tor Vergata, Italy; IASICNR, Italy; University of ChietiPescara, Italy) This paper presents some ideas concerning program manipulation and program transformation from the early days of their development. Particular emphasis will be given to program transformation techniques in the area of functional programming and constraint logic programming. We will also indicate current applications of program transformation techniques to the verification of program properties and program synthesis. @InProceedings{PEPM24p16, author = {Alberto Pettorossi and Maurizio Proietti and Fabio Fioravanti and Emanuele De Angelis}, title = {A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {1638}, doi = {10.1145/3635800.3637446}, year = {2024}, } Publisher's Version 

Fukaishi, Ren 
PEPM '24: "Productivity Verification ..."
Productivity Verification for Functional Programs by Reduction to Termination Verification
Ren Fukaishi, Naoki Kobayashi, and Ryosuke Sato (University of Tokyo, Japan) A program generating a coinductive data structure is called productive if the program eventually generates all the elements of the data structure. We propose a new method for verifying the productivity, which transforms a coinductive data structure into a function that takes a path as an argument and returns the corresponding element. For example, an infinite binary tree is converted to a function that takes a sequence consisting of 0 (left) and 1 (right), and returns the element in the specified position, and a stream is converted into a function that takes a sequence of the form 0^n (or, simply a natural number n) and returns the nth element of the stream. A streamgenerating program is then productive just if the function terminates for every n. The transformation allows us to reduce the productivity verification problem to the termination problem for callbyname higherorder functional programs without coinductive data structures. We formalize the transformation and prove its correctness. We have implemented an automated productivity checker based on the proposed method, by extending an automated HFL(Z) validity checker, which can be used as a termination checker. @InProceedings{PEPM24p70, author = {Ren Fukaishi and Naoki Kobayashi and Ryosuke Sato}, title = {Productivity Verification for Functional Programs by Reduction to Termination Verification}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {7082}, doi = {10.1145/3635800.3636963}, year = {2024}, } Publisher's Version 

Glück, Robert 
PEPM '24: "Partial Evaluation of Reversible ..."
Partial Evaluation of Reversible Flowchart Programs
Louis Marott Normann and Robert Glück (University of Copenhagen, Denmark) Flowchart languages are traditionally used to study the foundations of partial evaluation. This article presents a systematic and formal development of a method for partial evaluation of a reversible flowchart language. The results confirm that partial evaluation in this unconventional computing paradigm shows effects consistent with traditional partial evaluation. Experiments include specializing a symmetric encryption algorithm and a reversible interpreter for Bennett's reversible Turing machines. A defining feature of reversible languages is their invertibility. This study reports the first experiments composing program inversion and partial evaluation. The presented method is fully implemented. It is potentially of interest because reversible computing has found applications in areas as diverse as lowpower computing, debugging, robotics, and quantuminspired computing. @InProceedings{PEPM24p119, author = {Louis Marott Normann and Robert Glück}, title = {Partial Evaluation of Reversible Flowchart Programs}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {119133}, doi = {10.1145/3635800.3636967}, year = {2024}, } Publisher's Version 

Henglein, Fritz 
PEPM '24: "In memoriam Neil Deaton Jones ..."
In memoriam Neil Deaton Jones
Fritz Henglein (University of Copenhagen, Denmark) Neil Deaton Jones, professor emeritus at DIKU, the Department of Computer Science at the University of Copenhagen, passed away March 27th, 2023, shortly after his 82nd birthday. He is remembered for his seminal contributions to programming language research and theory of computation and for the impact his visions and his work have had on an entire generation of researchers, students and collaborators. @InProceedings{PEPM24p14, author = {Fritz Henglein}, title = {In memoriam Neil Deaton Jones}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {1415}, doi = {10.1145/3635800.3639464}, year = {2024}, } Publisher's Version 

Kiselyov, Oleg 
PEPM '24: "Complete Stream Fusion for ..."
Complete Stream Fusion for SoftwareDefined Radio
Tomoaki Kobayashi and Oleg Kiselyov (Tohoku University, Japan) Strymonas is a codegenerationbased library (embedded DSL) for fast, bulk, singlethread inmemory stream processing  with the declarative description of stream pipelines and yet achieving the speed and memory efficiency of handwritten state machines. It guarantees complete stream fusion in all cases. So far, strymonas has been used on small examples and microbenchmarks. In this work, we evaluate strymonas on a large, reallife application of SoftwareDefined Radio  FM Radio reception,  contrasting and benchmarking it against the synchronous dataflow system StreamIt, and the stateofthe art: GNU Radio. Strymonas, despite being declarative, singlethread singlecore with no explicit support for SIMD, no builtin windowing or convolution, turns out to offer portable high performance, well enough for realtime FM Radio reception. It is on par with (or, on Raspberry Pi Zero, outstripping) GNU Radio, while providing static guarantees of complete fusion and type safety. @InProceedings{PEPM24p57, author = {Tomoaki Kobayashi and Oleg Kiselyov}, title = {Complete Stream Fusion for SoftwareDefined Radio}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {5769}, doi = {10.1145/3635800.3636962}, year = {2024}, } Publisher's Version Info 

Kobayashi, Naoki 
PEPM '24: "Ownership Types for Verification ..."
Ownership Types for Verification of Programs with Pointer Arithmetic
Izumi Tanaka, Ken Sakayori, and Naoki Kobayashi (University of Tokyo, Japan) Toman et al. have proposed a type system for automatic verification of lowlevel programs, which combines ownership types and refinement types to enable strong updates of refinement types in the presence of pointer aliases. We extend their type system to support pointer arithmetic, and prove its soundness. Based on the proposed type system, we have implemented a prototype tool for automated verification of the lack of assertion errors of lowlevel programs with pointer arithmetic, and confirmed its effectiveness through experiments. @InProceedings{PEPM24p94, author = {Izumi Tanaka and Ken Sakayori and Naoki Kobayashi}, title = {Ownership Types for Verification of Programs with Pointer Arithmetic}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {94106}, doi = {10.1145/3635800.3636965}, year = {2024}, } Publisher's Version PEPM '24: "Productivity Verification ..." Productivity Verification for Functional Programs by Reduction to Termination Verification Ren Fukaishi, Naoki Kobayashi, and Ryosuke Sato (University of Tokyo, Japan) A program generating a coinductive data structure is called productive if the program eventually generates all the elements of the data structure. We propose a new method for verifying the productivity, which transforms a coinductive data structure into a function that takes a path as an argument and returns the corresponding element. For example, an infinite binary tree is converted to a function that takes a sequence consisting of 0 (left) and 1 (right), and returns the element in the specified position, and a stream is converted into a function that takes a sequence of the form 0^n (or, simply a natural number n) and returns the nth element of the stream. A streamgenerating program is then productive just if the function terminates for every n. The transformation allows us to reduce the productivity verification problem to the termination problem for callbyname higherorder functional programs without coinductive data structures. We formalize the transformation and prove its correctness. We have implemented an automated productivity checker based on the proposed method, by extending an automated HFL(Z) validity checker, which can be used as a termination checker. @InProceedings{PEPM24p70, author = {Ren Fukaishi and Naoki Kobayashi and Ryosuke Sato}, title = {Productivity Verification for Functional Programs by Reduction to Termination Verification}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {7082}, doi = {10.1145/3635800.3636963}, year = {2024}, } Publisher's Version 

Kobayashi, Tomoaki 
PEPM '24: "Complete Stream Fusion for ..."
Complete Stream Fusion for SoftwareDefined Radio
Tomoaki Kobayashi and Oleg Kiselyov (Tohoku University, Japan) Strymonas is a codegenerationbased library (embedded DSL) for fast, bulk, singlethread inmemory stream processing  with the declarative description of stream pipelines and yet achieving the speed and memory efficiency of handwritten state machines. It guarantees complete stream fusion in all cases. So far, strymonas has been used on small examples and microbenchmarks. In this work, we evaluate strymonas on a large, reallife application of SoftwareDefined Radio  FM Radio reception,  contrasting and benchmarking it against the synchronous dataflow system StreamIt, and the stateofthe art: GNU Radio. Strymonas, despite being declarative, singlethread singlecore with no explicit support for SIMD, no builtin windowing or convolution, turns out to offer portable high performance, well enough for realtime FM Radio reception. It is on par with (or, on Raspberry Pi Zero, outstripping) GNU Radio, while providing static guarantees of complete fusion and type safety. @InProceedings{PEPM24p57, author = {Tomoaki Kobayashi and Oleg Kiselyov}, title = {Complete Stream Fusion for SoftwareDefined Radio}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {5769}, doi = {10.1145/3635800.3636962}, year = {2024}, } Publisher's Version Info 

Liu, Yanhong A. 
PEPM '24: "Incremental Computation: What ..."
Incremental Computation: What Is the Essence? (Invited Contribution)
Yanhong A. Liu (Stony Brook University, USA) Incremental computation aims to compute more efficiently on changed input by reusing previously computed results. We give a highlevel overview of works on incremental computation, and highlight the essence underlying all of them, which we call incrementalizationthe discrete counterpart of differentiation in calculus. We review the gist of a systematic method for incrementalization, and a systematic method centered around it, called IterateIncrementalizeImplement, for program design and optimization, as well as algorithm design and optimization. At a metalevel, with historical contexts and for future directions, we stress the power of highlevel data, control, and module abstractions in developing new and better algorithms and programs as well as their precise complexities. @InProceedings{PEPM24p39, author = {Yanhong A. Liu}, title = {Incremental Computation: What Is the Essence? (Invited Contribution)}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {3952}, doi = {10.1145/3635800.3637447}, year = {2024}, } Publisher's Version 

Masuhara, Hidehiko 
PEPM '24: "An Intrinsically Typed Compiler ..."
An Intrinsically Typed Compiler for Algebraic Effect Handlers
Syouki Tsuyama, Youyou Cong, and Hidehiko Masuhara (Tokyo Institute of Technology, Japan) A typepreserving compiler converts a welltyped input program into a welltyped output program. Previous studies have developed typepreserving compilers for various source languages, including the simplytyped lambda calculus and calculi with control constructs. Our goal is to realize typepreserving compilation of languages that have facilities for manipulating firstclass continuations. In this paper, we focus on algebraic effects and handlers, a generalization of exceptions and their handlers with resumable continuations. Specifically, we choose an effect handler calculus and a typed stackmachinebased assembly language as the source and the target languages, respectively, and formalize the target language and a type preserving compiler. The main challenge posed by firstclass continuation is how to ensure safety of continuation capture and resumption, which involves concatenation of unknown stacks. We solve this challenge by incorporating stack polymorphism, a technique that has been used for compilation from a language without firstclass continuations to a stackbased assembly language. To prove that our compiler is type preserving, we implemented the compiler in Agda as a function between intrinsically typed ASTs. We believe that our contributions could lead to correct and efficient compilation of continuationmanipulating facilities in general. @InProceedings{PEPM24p134, author = {Syouki Tsuyama and Youyou Cong and Hidehiko Masuhara}, title = {An Intrinsically Typed Compiler for Algebraic Effect Handlers}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {134145}, doi = {10.1145/3635800.3636968}, year = {2024}, } Publisher's Version 

Normann, Louis Marott 
PEPM '24: "Partial Evaluation of Reversible ..."
Partial Evaluation of Reversible Flowchart Programs
Louis Marott Normann and Robert Glück (University of Copenhagen, Denmark) Flowchart languages are traditionally used to study the foundations of partial evaluation. This article presents a systematic and formal development of a method for partial evaluation of a reversible flowchart language. The results confirm that partial evaluation in this unconventional computing paradigm shows effects consistent with traditional partial evaluation. Experiments include specializing a symmetric encryption algorithm and a reversible interpreter for Bennett's reversible Turing machines. A defining feature of reversible languages is their invertibility. This study reports the first experiments composing program inversion and partial evaluation. The presented method is fully implemented. It is potentially of interest because reversible computing has found applications in areas as diverse as lowpower computing, debugging, robotics, and quantuminspired computing. @InProceedings{PEPM24p119, author = {Louis Marott Normann and Robert Glück}, title = {Partial Evaluation of Reversible Flowchart Programs}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {119133}, doi = {10.1145/3635800.3636967}, year = {2024}, } Publisher's Version 

Pettorossi, Alberto 
PEPM '24: "A Historical Perspective on ..."
A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)
Alberto Pettorossi, Maurizio Proietti, Fabio Fioravanti, and Emanuele De Angelis (University of Rome Tor Vergata, Italy; IASICNR, Italy; University of ChietiPescara, Italy) This paper presents some ideas concerning program manipulation and program transformation from the early days of their development. Particular emphasis will be given to program transformation techniques in the area of functional programming and constraint logic programming. We will also indicate current applications of program transformation techniques to the verification of program properties and program synthesis. @InProceedings{PEPM24p16, author = {Alberto Pettorossi and Maurizio Proietti and Fabio Fioravanti and Emanuele De Angelis}, title = {A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {1638}, doi = {10.1145/3635800.3637446}, year = {2024}, } Publisher's Version 

Proietti, Maurizio 
PEPM '24: "A Historical Perspective on ..."
A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)
Alberto Pettorossi, Maurizio Proietti, Fabio Fioravanti, and Emanuele De Angelis (University of Rome Tor Vergata, Italy; IASICNR, Italy; University of ChietiPescara, Italy) This paper presents some ideas concerning program manipulation and program transformation from the early days of their development. Particular emphasis will be given to program transformation techniques in the area of functional programming and constraint logic programming. We will also indicate current applications of program transformation techniques to the verification of program properties and program synthesis. @InProceedings{PEPM24p16, author = {Alberto Pettorossi and Maurizio Proietti and Fabio Fioravanti and Emanuele De Angelis}, title = {A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {1638}, doi = {10.1145/3635800.3637446}, year = {2024}, } Publisher's Version 

Sakayori, Ken 
PEPM '24: "Ownership Types for Verification ..."
Ownership Types for Verification of Programs with Pointer Arithmetic
Izumi Tanaka, Ken Sakayori, and Naoki Kobayashi (University of Tokyo, Japan) Toman et al. have proposed a type system for automatic verification of lowlevel programs, which combines ownership types and refinement types to enable strong updates of refinement types in the presence of pointer aliases. We extend their type system to support pointer arithmetic, and prove its soundness. Based on the proposed type system, we have implemented a prototype tool for automated verification of the lack of assertion errors of lowlevel programs with pointer arithmetic, and confirmed its effectiveness through experiments. @InProceedings{PEPM24p94, author = {Izumi Tanaka and Ken Sakayori and Naoki Kobayashi}, title = {Ownership Types for Verification of Programs with Pointer Arithmetic}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {94106}, doi = {10.1145/3635800.3636965}, year = {2024}, } Publisher's Version 

Sato, Ryosuke 
PEPM '24: "Productivity Verification ..."
Productivity Verification for Functional Programs by Reduction to Termination Verification
Ren Fukaishi, Naoki Kobayashi, and Ryosuke Sato (University of Tokyo, Japan) A program generating a coinductive data structure is called productive if the program eventually generates all the elements of the data structure. We propose a new method for verifying the productivity, which transforms a coinductive data structure into a function that takes a path as an argument and returns the corresponding element. For example, an infinite binary tree is converted to a function that takes a sequence consisting of 0 (left) and 1 (right), and returns the element in the specified position, and a stream is converted into a function that takes a sequence of the form 0^n (or, simply a natural number n) and returns the nth element of the stream. A streamgenerating program is then productive just if the function terminates for every n. The transformation allows us to reduce the productivity verification problem to the termination problem for callbyname higherorder functional programs without coinductive data structures. We formalize the transformation and prove its correctness. We have implemented an automated productivity checker based on the proposed method, by extending an automated HFL(Z) validity checker, which can be used as a termination checker. @InProceedings{PEPM24p70, author = {Ren Fukaishi and Naoki Kobayashi and Ryosuke Sato}, title = {Productivity Verification for Functional Programs by Reduction to Termination Verification}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {7082}, doi = {10.1145/3635800.3636963}, year = {2024}, } Publisher's Version 

Sestoft, Peter 
PEPM '24: "The Genesis of Mix: Early ..."
The Genesis of Mix: Early Days of SelfApplicable Partial Evaluation (Invited Contribution)
Peter Sestoft and Harald Søndergaard (IT University of Copenhagen, Denmark; University of Melbourne, Australia) Forty years ago development started on Mix, a partial evaluator designed specifically for the purpose of selfapplication. The effort, led by Neil D. Jones at the University of Copenhagen, eventually demonstrated that nontrivial compilers could be generated automatically by applying a partial evaluator to itself. The possibility, in theory, of such selfapplication had been known for more than a decade, but remained unrealized by the start of 1984. We describe the genesis of Mix, including the research environment, the challenges, and the main insights that led to success. We emphasize the critical role played by program annotation as a preprocessing step, later automated in the form of bindingtime analysis. @InProceedings{PEPM24p1, author = {Peter Sestoft and Harald Søndergaard}, title = {The Genesis of Mix: Early Days of SelfApplicable Partial Evaluation (Invited Contribution)}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {113}, doi = {10.1145/3635800.3637445}, year = {2024}, } Publisher's Version 

Søndergaard, Harald 
PEPM '24: "The Genesis of Mix: Early ..."
The Genesis of Mix: Early Days of SelfApplicable Partial Evaluation (Invited Contribution)
Peter Sestoft and Harald Søndergaard (IT University of Copenhagen, Denmark; University of Melbourne, Australia) Forty years ago development started on Mix, a partial evaluator designed specifically for the purpose of selfapplication. The effort, led by Neil D. Jones at the University of Copenhagen, eventually demonstrated that nontrivial compilers could be generated automatically by applying a partial evaluator to itself. The possibility, in theory, of such selfapplication had been known for more than a decade, but remained unrealized by the start of 1984. We describe the genesis of Mix, including the research environment, the challenges, and the main insights that led to success. We emphasize the critical role played by program annotation as a preprocessing step, later automated in the form of bindingtime analysis. @InProceedings{PEPM24p1, author = {Peter Sestoft and Harald Søndergaard}, title = {The Genesis of Mix: Early Days of SelfApplicable Partial Evaluation (Invited Contribution)}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {113}, doi = {10.1145/3635800.3637445}, year = {2024}, } Publisher's Version 

Tanaka, Izumi 
PEPM '24: "Ownership Types for Verification ..."
Ownership Types for Verification of Programs with Pointer Arithmetic
Izumi Tanaka, Ken Sakayori, and Naoki Kobayashi (University of Tokyo, Japan) Toman et al. have proposed a type system for automatic verification of lowlevel programs, which combines ownership types and refinement types to enable strong updates of refinement types in the presence of pointer aliases. We extend their type system to support pointer arithmetic, and prove its soundness. Based on the proposed type system, we have implemented a prototype tool for automated verification of the lack of assertion errors of lowlevel programs with pointer arithmetic, and confirmed its effectiveness through experiments. @InProceedings{PEPM24p94, author = {Izumi Tanaka and Ken Sakayori and Naoki Kobayashi}, title = {Ownership Types for Verification of Programs with Pointer Arithmetic}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {94106}, doi = {10.1145/3635800.3636965}, year = {2024}, } Publisher's Version 

Tsuyama, Syouki 
PEPM '24: "An Intrinsically Typed Compiler ..."
An Intrinsically Typed Compiler for Algebraic Effect Handlers
Syouki Tsuyama, Youyou Cong, and Hidehiko Masuhara (Tokyo Institute of Technology, Japan) A typepreserving compiler converts a welltyped input program into a welltyped output program. Previous studies have developed typepreserving compilers for various source languages, including the simplytyped lambda calculus and calculi with control constructs. Our goal is to realize typepreserving compilation of languages that have facilities for manipulating firstclass continuations. In this paper, we focus on algebraic effects and handlers, a generalization of exceptions and their handlers with resumable continuations. Specifically, we choose an effect handler calculus and a typed stackmachinebased assembly language as the source and the target languages, respectively, and formalize the target language and a type preserving compiler. The main challenge posed by firstclass continuation is how to ensure safety of continuation capture and resumption, which involves concatenation of unknown stacks. We solve this challenge by incorporating stack polymorphism, a technique that has been used for compilation from a language without firstclass continuations to a stackbased assembly language. To prove that our compiler is type preserving, we implemented the compiler in Agda as a function between intrinsically typed ASTs. We believe that our contributions could lead to correct and efficient compilation of continuationmanipulating facilities in general. @InProceedings{PEPM24p134, author = {Syouki Tsuyama and Youyou Cong and Hidehiko Masuhara}, title = {An Intrinsically Typed Compiler for Algebraic Effect Handlers}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {134145}, doi = {10.1145/3635800.3636968}, year = {2024}, } Publisher's Version 

Verbitskaia, Ekaterina 
PEPM '24: "A Case Study in Functional ..."
A Case Study in Functional Conversion and Mode Inference in miniKanren
Ekaterina Verbitskaia, Igor Engel, and Daniil Berezun (JetBrains Research, Serbia; Constructor University Bremen, Germany; JetBrains Research, Germany; JetBrains Research, Netherlands) Many programs which solve complicated problems can be seen as inversions of other, much simpler, programs. One particular example is transforming verifiers into solvers, which can be achieved with low effort by implementing the verifier in a relational language and then executing it in the backward direction. Unfortunately, as it is common with inverse computations, interpretation overhead may lead to subpar performance compared to direct program inversion. In this paper we discuss functional conversion aimed at improving relational miniKanren specifications with respect to a known fixed direction. Our preliminary evaluation demonstrates a significant performance increase for some programs which exemplify the approach. @InProceedings{PEPM24p107, author = {Ekaterina Verbitskaia and Igor Engel and Daniil Berezun}, title = {A Case Study in Functional Conversion and Mode Inference in miniKanren}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {107118}, doi = {10.1145/3635800.3636966}, year = {2024}, } Publisher's Version 
25 authors
proc time: 6.56