The 2025 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

About

The ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM) has a history going back to 1991 and has been held in conjunction with POPL every year since 2006. The origin of PEPM is in the discoveries of practically useful automated techniques for evaluating programs with only partial input. Over time, PEPM has broadened its scope to include a variety of research areas centered around 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, analyzed, and transformed while establishing or maintaining important semantic properties.

Scope

In addition to the traditional PEPM topics (see below), PEPM 2025 welcomes submissions in new domains, in particular:

• Semantics based and machine-learning based program synthesis and program optimization.
• Modeling, analysis, and transformation techniques for distributed and concurrent protocols and programs, such as session types, linear types, and contract specifications.

More generally, topics of interest for PEPM 2024 include, but are not limited to:

• Program and model manipulation techniques such as: supercompilation, partial evaluation, fusion, on-the-fly program adaptation, active libraries, program inversion, slicing, symbolic execution, refactoring, decompilation, and obfuscation.
• Techniques that treat programs/models as data objects including metaprogramming, generative programming, embedded domain-specific languages, program synthesis by sketching and inductive programming, staged computation, and model-driven program generation and transformation.
• Program analysis techniques that are used to drive program/model manipulation such as: abstract interpretation, termination checking, binding-time analysis, constraint solving, type systems, automated testing and test case generation.
• Application of the above techniques including case studies of program manipulation in real-world (industrial, open-source) projects and software development processes, descriptions of robust tools capable of effectively handling realistic applications, benchmarking. Examples of application domains include legacy program understanding and transformation, DSL implementations, visual languages and end-user programming, scientific computing, middleware frameworks and infrastructure needed for distributed and web-based applications, embedded and resource-limited computation, and security.

This list of categories is not exhaustive, and we encourage submissions describing new theories and applications related to semantics-based program manipulation in general. If you have a question as to whether a potential submission is within the scope of the workshop, please contact the program co-chairs, Guillaume Allais (guillaume.allais@strath.ac.uk) and Annie Liu (liu@cs.stonybrook.edu).

AUTHORS TAKE NOTE: The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of the conference. The official publication date affects the deadline for any patent filings related to published work.

Call for Papers

Three kinds of submissions will be accepted:

1. Regular Research Papers should describe new results, and will be judged on originality, correctness, significance, and clarity. Regular research papers must not exceed 12 pages.

2. Short Papers may include tool demonstrations and presentations of exciting if not fully polished research, and of interesting academic, industrial, and open-source applications that are new or unfamiliar. Short papers must not exceed 6 pages.

3. Talk Proposals may propose lectures about topics of interest for PEPM, existing work representing relevant contributions, or promising contributions that are not mature enough to be proposed as papers of the other categories. Talk Proposals must not exceed 2 pages.

References and appendices are not included in page limits. Appendices may not necessarily be read by reviewers. Both kinds of submissions should be typeset using the two-column ‘sigplan’ sub-format of the new ‘acmart’ format available at:

http://sigplan.org/Resources/Author/

and submitted electronically via HotCRP: https://pepm25.hotcrp.com

Reviewing will be single-blind.

Submissions are welcome from PC members (except the two co-chairs).

Accepted regular research papers will appear in formal proceedings published by ACM, and be included in the ACM Digital Library. Accepted short papers do not constitute formal publications and will not appear in the proceedings.

At least one author of each accepted contribution must attend the workshop (physically or virtually) to present the work. In the case of tool demonstration papers, a live demonstration of the described tool is expected.

William Bowman – University of British Columbia

Brigitte Pientka – McGill University

Satnam Singh – Groq

Abstracts

The Ethical Compiler: Addressing the Is-Ought Gap in Compilation

William Bowman

The is-ought gap is a problem in moral philosophy observing that ethical judgments (“ought”) cannot be grounded purely in truth judgments (“is”): that an ought cannot be derived from an is. This gap renders the following argument invalid: “It is true that type safe languages prevent bugs and that bugs cause harm, therefore you ought to write in type safe languages.”. To validate ethical claims, we must bridge the gap between is and ought with some ethical axiom, such as “I believe one ought not cause harm.”.

But what do ethics have to do with manipulating programs? A lot! Ethics are central to correctness! For example, suppose an algorithm infers the type of e is Bool, and e is in fact a Bool; the program type checks. Is the program correct—does it behave as it ought? We cannot answer this without some ethical axioms: what does the programmer believe ought to be?

I believe one ought to design and implement languages ethically. We must give the programmer the ability to express their ethics—their values and beliefs about a program—in addition to its mere computational content, and build tools that respect the distinction between is and ought. This talk is a guide to ethical language design and implementation possibilities.

Bio

William J. Bowman is an Assistant Professor of computer science in the Software Practices Lab at University of British Columbia. Broadly speaking, he is interested in making it easier for programmers to communicate their intent to machines, and preserving that intent through compilation. More specifically, their research interests include secure and verified compilation, dependently typed programming, verification, meta-programming, and interoperability. His recent work examines type-preserving compilation of dependently typed programming languages like Coq, a technique that can enable preserving security and correctness invariants of verified software through compilation and statically enforcing those invariants in the low-level (assembly-like) code generated by compilers.

Cocon: A Type-Theoretic Framework for Meta-Programming

Brigitte Pientka

Meta-programming is the art of writing programs that produce or manipulate other programs. This allows programmers to automate error-prone or repetitive tasks, and exploit domain- specific knowledge to customize the generated code. Hence, meta-programming is widely used in a range of technologies: from cryptographic message authentication in secure network protocols to support reflection in proof environments such as Lean.

Unfortunately, writing safe meta-programs remains very challenging and sometimes frustrating, as traditionally errors in the generated code are only detected when running it, but not at the time when code is generated. To make it easier to write and maintain meta-programs, tools that allow us to detect errors during code generation - instead of when running the generated code - are essential.

This talk revisits Cocon, a framework for certified meta-programming. Cocon is a Martin-Löf dependent type theory for defining logics and proofs that allows us to represent domain-specific languages (DSL) within the logical framework LF and in addition write recursive programs and proofs about those DSLs using pattern matching. It is a two-level type theory where Martin-Löf type theory sits on top of the logical framework LF and supports a recursor over (contextual) LF objects. As a consequence, we can embed into LF STLC or System F, etc. and then write programs about those encodings using Cocon itself.

This means Cocon can serve as a target for compiling meta-programming systems -from compiling meta-programming with STLC to System F. Moreover, Cocon supports writing an evaluator for each of these sub-languages. This also allows us to reflect back our encoded sub-language and evaluate their encodings using Cocon’s evaluation strategy.

I will conclude with highlighting more recent research directions and challenges that build on the core ideas of Cocon and aim to support meta-programming and intensional code analysis directly in System F and Martin-Löf type theory.

Bio

Brigitte Pientka a Full Professor in the School of Computer Science at McGill University. Her main research interests lie in developing theoretical foundations of programming languages. A central question of her work is: How can we design programming languages that ensure that programs are safe and have fewer bugs? In 2018, her work on the Beluga programming language has received the Test of Time Award from International Symposium on Principles and Practice of Declarative Programming (PPDP).

Brigitte Pientka is a leader within the programming languages research community, and serves for example on the SIGPLAN executive committee. In particular, she is passionate about working towards overcoming systemic barriers for underrepresented groups. In 2018, she co-founded the Women in Logic workshop which provides valuable networking opportunity to female researchers and as the general chair for POPL in 2020 she introduced Mentoring Breakfasts which now are a fixture at SIGPLAN events.

The Missing Diagonal: High Level Languages for Low Level Systems

Satnam Singh

The computing community has produced many high level languages and tools for programming high level systems (e.g. Java for user interfaces) and it has produced many low level languages and tools for programming low level systems (C for operating systems, Verilog for hardware design) yet there are not many examples of high level systems that have been produced to help develop low level systems. Sometimes this is due to a suspicion that the layers of abstraction that high level systems use incur unacceptable performance overheads. However, this talk attempts to challenge that view, giving examples of high level systems that improve the designer productivity for developing low level systems which also improve the quality of verification for low level systems.

The talk will draw examples from the presenter’s own experience, as well as the work of others. Specific examples will include Lava and Bluespec for the design of hardware, the Silver Oak project for the co-design of a high assurance silicon root of trust, a Haskell-based DSL for programming machine learning chips, and recent work on the specification and verification of parts of a new silicon chip produced at Groq which makes use of the same Haskell DSL.

Bio

Satnam Singh is a Fellow at Groq where he applies the power of functional programming languages to the design of machine learning chips and their programming models. Satnam Singh previously worked at Google (machine learning chips, cluster management), Facebook (Android optimization), Microsoft (parallel and concurrent programming) and Xilinx (Lava DSL for hardware design). He started his career as an academic at the University of Glasgow (FPGA-based application acceleration and functional programming).