PEPM 2025
who it's for
programming language researchers, language designers, compiler engineers, formal methods researchers, proof assistant developers, programming tools implementers, programming educators
topics
two-level type theory; LF for code embedding; Martin-Lof meta-programming; triage calculus for analysis; breadth-first self-evaluator; fuelled self-reducer for System T; algebraic stepper for modules; type-sensitive algebraic macros; semantics-based program manipulation with LLMs; ethical considerations in compilation; timing and cache side-channel verification; partial well-behaved lenses
| title | author | length |
|---|---|---|
| A Type-Theoretic Framework for Certified Meta-programming | Brigitte Pientka | 50m |
Claims a two-level type theory where LF encodes object languages and Martin-Löf type theory runs meta-programs, so generated code is typed and manipulable… | ||
| Typed Program Analysis Without Encodings | Barry Jay | 32m |
Claims a direct, unencoded program-analysis model using unlabeled binary trees and a new triage calculus with five reduction rules, where each reduction… | ||
| A Fuelled Self-Reducer for System T | Greg Brown | 15m |
Implements a fuelled self-reducer for System T that actually runs: uses Kiselyov and Longley and Normann encodings for products, sums and some inductive types… | ||
| Algebraic Stepper for Simple Modules | Kenichi Asai, Hinano Akiyama | 29m |
An OCaml algebraic stepper is implemented for simple hierarchical modules (no functors or signature sealing) that shows execution by delayed substitution of… | ||
| Semantics-based program manipulation in the age of LLMs | William J. Bowman, Brigitte Pientka, Satnam Singh, Sam Lindley | 53m |
Panel records concrete experiments and workflows: VS Code + Copilot generates SystemVerilog that is iteratively checked and fixed against model checking… | ||
| Type-Sensitive Algebraic Macros | April Gonçalves, Robert Atkey | 14m |
Claims a type-sensitive algebraic theory that directly encodes typechecking and elaboration for STλC, plus concrete variants: Bidirectional STλC and… | ||
| The Ethical Compiler: Addressing the Is-Ought Gap in Compilation | William J. Bowman | 46m |
Paper argues that compilers should be ethical not merely correct and presents six metaethical dictums: let programmers express what ought to hold, ensure… | ||
| Collapsing Towers for Side-Channel Security | Cameron Wong, Muhammad Abdullah, Yuheng Yang, Mengjia Yan, Adam Chlipala, Nada Amin | 14m |
A technique uses staging to turn an instrumented interpreter into a compilerlike residue program that exposes a runtime step counter and cache effects as… | ||
| Characterizations of Partial Well-Behaved Lenses | Keishi Hashiba, Keisuke Nakano, Kazuyuki Asada, Kentaro Kikuchi | 28m |
Defines five lens laws for partial functions, proves implication maps among them, and characterizes two concrete cases: when only put is partial the Fischer et… | ||
| Welcome | Y. Annie Liu | 06m |
Conference opening lists three sessions: high-level abstraction and automation, language design, logical tools and staged interpreters with types and… | ||
| A type safe calculus for generating syntax-directed editors | Benjamin Bennetzen, Nikolaj Rossander Kristensen, Andreas Tor Mortensen, Peter Buus Steffensen, Sune Skaanning Engtorp, Hans Hüttel | 29m |
A generalized editor calculus is presented that guarantees that well-typed editor scripts produce well-formed programs by encoding the calculus into a simply… | ||
| nothing matches | ||