PEPM 2022
who it's for
programming language researchers, compiler engineers, language implementers, formal methods engineers, performance engineers, security engineers
topics
dependent tagless-final embedding; quantitative type theory; Idris metaprogramming; baseline and tracing JITs; Futamura projections and partial evaluation; semi-interleaved ladder code; let(rec) insertion semantics; type-directed program transformation; modal types for staging; incrementalization transformation; parallel algebraic effect handlers; staged symbolic interpreters
| title | author | length |
|---|---|---|
| Dependent tagless final | Nicolas Biri | 31m |
Proposes a dependent tagless‑final embedding implemented in Idris using quantitative type theory and Elab/TT‑imp metaprogramming to compose three concrete… | ||
| Two-level Just-in-Time Compilation with One Interpreter and One Engine | Carl Friedrich Bolz-Tereick, Jonathan Immanuel Brachthäuser, Yusuke Izawa | 45m |
Adaptive RPython generates both a baseline (threaded-code) JIT and a tracing JIT from one interpreter and one engine by producing multiple interpreter variants… | ||
| A partial history of partial evaluation | Peter Sestoft, Julia Lawall | 01h 01m |
The 1984–85 work realizes non‑trivial self‑application of a partial evaluator, achieving the second and third Futamura projections by turning a specializer… | ||
| Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Depe | Christopher Brown, Adam D. Barwell, Yoann Marquer, Olivier Zendra, Tania Richmond, Chen Gu | 29m |
A semi-automatic Eclipse-based refactoring tool rewrites a subset of C into semi-interleaved ladder code, using a backend written in Idris so dependent types… | ||
| let (rec) insertion without Effects, Lights or Magic | Oleg Kiselyov, Jonathan Blow | 32m |
Claims a denotational semantics for let(rec)-insertion that avoids delimited control and other effects, models insertion as composable annotations (sticky… | ||
| On Type-Based Techniques for Program Manipulation | Naoki Kobayashi | 56m |
Type-directed transformations formalize program rewrites as typing judgments and prove soundness by preservation under reduction plus soundness for values. Two… | ||
| Modal Logics and Types: Looking Back and Looking Forward | Frank Pfenning | 01h 03m |
Shows that modal types make runtime code generation, staging and partial evaluation precise by decomposing S4 into up/down shifts (quotation = box as up then… | ||
| From meta frameworks and transformations to distributed computing and more | Annie Liu, William J. Bowman | 01h 05m |
Overview of concrete results and tools: partial evaluation plus systematic specialization and the incrementalization transformation turn high‑level specs into… | ||
| Parallel Algebraic Effect Handlers | Daniel Johnson, Antonina Nepelyova | 36m |
Paper formalizes lambda^p, an untyped calculus that adds a novel traverse clause so handlers can rewrite a for-expression into a parallel form. It proves… | ||
| Partially Evaluating Symbolic Interpreters for All | Shangyin Tan, Guannan Wei, Tiark Rompf | 29m |
Builds staged symbolic interpreters with Lightweight Modular Staging (LMS) to compile concolic and call‑chain backward symbolic execution for an LLVM‑style IR… | ||
| Why are partial evaluation and supercompilation still not widely used in practic | Andrew Tolmach, Sam Lindley | 01h 06m |
Argues that partial evaluation and supercompilation repeatedly show concrete wins in research—Russian work produces prototypes (including a Novosibirsk… | ||
| nothing matches | ||