PEPM 2023
as the organisers put it
About The ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), which has a history going back to 1991 and has co-located with POPL every year since 2006, originates in the discoveries of practically useful automated techniques for evaluating programs with only partial input. Over the years, the scope of PEPM has expanded to include a variety of research areas centred around the theme of semantics-based program manipulation — the systematic exploitation of treating programs not only as subject to black-box execution, but also as data structures that can be generated, ...
who it's for
programming language researchers, compiler engineers, formal verification engineers, partial evaluation researchers, program analysis engineers, tool builders for embedded and safety-critical systems, quantum software researchers
topics
verified cryptographic C generation; partial evaluation type debugging; semantic transformation for rewriting; symbolic execution of quantum circuits; verified polynomial multiplication generator; MATLAB to embeddable C; modular multi-sorted free extensions; memoized attribute grammars via zipper; reflection for algebraic effect handlers; normalization-by-evaluation for specialization
| title | author | length |
|---|---|---|
| Fast Cryptographic Code via Partial Evaluation | Adam Chlipala | 58m |
Generates mechanically verified, high-performance cryptographic C from Coq: a verified compiler using partial evaluation, abstract interpretation and… | ||
| Towards Type Debugging using Partial Evaluation | Kanae Tsushima, Robert Glück | 27m |
Method executes ill-typed programs by freeze likely-error sites using compiler type-inferencer error reports, then iteratively reduce frozen regions with type… | ||
| Semantic Transformation Framework for Rewriting Rules | Jihee Park, Jaemin Hong, Sukyoung Ryu | 29m |
Refines Cousot & Cousot by tailoring a semantic transformation framework to rewriting rules and builds a four-part pipeline: matcher/meter, syntactic… | ||
| Symbolic Execution of Hadamard-Toffoli Quantum Circuits | Jacques Carette, Gerardo Ortiz, Amr Sabry | 30m |
Classical symbolic evaluation models Hadamard-created superpositions as symbolic boolean variables and runs reversible parts forward and backward to produce… | ||
| Generating Programs for Polynomial Multiplication with Correctness Assurance | Ryo Tokuda, Yukiyoshi Kameyama | 23m |
Generates verified polynomial-multiplication code by driving a DSL-based program generator with stronger interval analysis and formula synthesis; finds an… | ||
| MATLAB Coder: Partial Evaluation in Practice | Denis Gurchenkov, Fred Smith | 53m |
MATLAB Coder converts MATLAB into embeddable C/C++ by using online partial evaluation and a type-driven engine that does function specialization on types and… | ||
| Modular Construction of Multi-sorted Free Extensions | Guillaume Allais, Nathan Corbyn, Ohad Kammar, Nachiappan Valliappan, Sam Lindley, Jeremy Yallop | 35m |
Defines how to build combined free extensions by composing existing frexes and gives three modular constructions: a concrete involutive algebra frex (covers… | ||
| Efficient Embedding of Strategic Attribute Grammars via Memoization | José Nuno Macedo, Emanuel Rodrigues, Marcos Viera, João Saraiva | 30m |
Memoizing attribute values inside the zipper eliminates repeated recomputation and yields a practical embedding of attribute grammars combined with strategic… | ||
| Towards a Reflection for Effect Handlers | Youyou Cong, Kenichi Asai | 19m |
Attempts to establish a reflection for algebraic effects use a simplest CPS translation (two continuations plus an aspirant construct) and a precisely… | ||
| nothing matches | ||