PEPM 2024
who it's for
programming language researchers, compiler developers, functional programmers, formal methods engineers, verification engineers, DSL designers
topics
DPella Haskell eDSL; privacy-cost static analysis; mu HFL termination encoding; complete stream fusion; SDR pipeline specialization; functional conversion for miniKanren; mode inference for relations; reversible-flowchart specialization; intrinsically typed compiler in Agda; ownership types for pointer arithmetic; scoped typed staging with NbE; one-pass CPS for dependent types
| title | author | length |
|---|---|---|
| Opening | Meng Wang, Gabriele Keller | 01m |
Conference opens with housekeeping and a schedule note: organizers mark 30 years of PEPM with a special session at the end of the day devoted to that… | ||
| From Theory to Practice: Crafting Differential Privacy Systems with Haskell | Alejandro Russo | 01h 01m |
A Haskell eDSL called DPella eDSL in Haskell provides runnable queries that statically report privacy cost and accuracy: a symbolic interpreter computes a… | ||
| Productivity Verification for Functional Programs by Reduction to Termination Ve... | Ren Fukaishi, Naoki Kobayashi, Ryosuke Sato | 23m |
Method translates coinductive values into functions that take a path (integer list) and returns the element, turning productivity into reduction to termination… | ||
| Complete Stream Fusion for Software-Defined Radio | Tomoaki Kobayashi, Oleg Kiselyov | 22m |
Strymonas compiles declarative pipelines to generated C with a single main loop, no dynamic allocation, and complete stream fusion, and it implements a… | ||
| A Case Study in Functional Conversion and Mode Inference in miniKanren | Ekaterina Verbitskaia, Igor Engel, Daniil Berezun | 22m |
Claims a concrete pipeline that turns miniKanren relations into deterministic functions via functional conversion plus mode inference, implemented as a… | ||
| Partial Evaluation of Reversible Flowchart Programs | Louis Marott Normann, Robert Glück | 27m |
Presents a fully formalized specializer for a reversible flowchart language (RL), implemented and published on GitHub, with concrete fixes: uniform… | ||
| Towards a Language-parametric DSL for Refactoring (Short Paper) | Casper Bach Poulsen, Xulei Liu, Luka Miljak | 18m |
Prototype DSL implements language‑parametric refactorings by deriving full name‑binding info from scope graphs, performing concise traversals via a borrowed… | ||
| An Intrinsically Typed Compiler for Algebraic Effect Handlers | Syouki Tsuyama, Youyou Cong, Hidehiko Masuhara | 16m |
Implements a type preserving compiler from an algebraic effect handler calculus to a stack‑machine assembly and proves type preservation by writing the… | ||
| Ownership Types for Verification of Programs with Pointer Arithmetic | Izumi Tanaka, Ken Sakayori, Naoki Kobayashi | 29m |
Extends Toman et al.’s refinement-plus-ownership type system to handle pointer arithmetic, proves soundness, and implements a prototype tool that verifies… | ||
| Scoped and Typed Staging by Evaluation | Guillaume Allais | 24m |
Dependently typed host language constructs a minimal two‑level simply typed calculus that is well scoped and typed by construction, using an NbE‑style model to… | ||
| One-Pass CPS Translation of Dependent Types (Talk Proposal) | Youyou Cong | 13m |
Claims a one-pass CPS translation of Calculus of Constructions with Sigma (dependent pair) types that preserves dependent typing while producing no… | ||
| In memoriam Neil Deaton Jones | Fritz Henglein | 22m |
A 2024 memorial records Neil Deaton Jones’s death (March 27, 2023, age 82) and catalogs concrete contributions: partial evaluation that leads to… | ||
| The Genesis of Mix: Early Days of Self-Applicable Partial Evaluation (Invited Co... | Peter Sestoft, Harald Sondergaard | 31m |
Forty years ago a small team builds Mix, a Lisp-based partial evaluator, and by late 1984 finally achieves practical self-application, proving the second and… | ||
| A Historical Perspective on Program Transformation and Recent Developments (Invi... | Alberto Pettorossi, Maurizio Proietti, Fabio Fioravanti, Emanuele De Angelis | 33m |
Historical survey ties classic transformation techniques to concrete outcomes: rule-based unfolding/folding rules plus strategies produce a linear-time… | ||
| Incremental Computation: What Is the Essence? (Invited Contribution) | Yanhong A. Liu | 24m |
Argues that the core idea is incrementalization = discrete differentiation: transform programs to reuse previous results and treat input changes explicitly… | ||
| nothing matches | ||