PEPM 2021
who it's for
programming language researchers, compiler engineers, verification engineers, language tool developers, DSL designers, systems programmers
topics
typed trails for continuations; grammar-driven syntax completion; Coq to C code generation; partial-evaluation monomorphization; CPS translation for Featherweight Java; Coccinelle semantic patches for C; erasure inference for dependent types; latent effects and algebraic handlers; automatic differentiation via effects; type-safe structure editor calculus; closure conversion for non-strict languages; hardware domain-specific languages (Peak/Lake/Canal)
| title | author | length |
|---|---|---|
| A Functional Abstraction of Typed Trails + A Text-based Syntax Completion Method | Kenichi Asai, Youyou Cong, Chiaki Ishio, Isao Sasano, Kwanghoon Choi | 01h 01m |
Presents a new type system that models continuation invocation contexts as functional trails so control and prompt can have heterogeneous trail types it claims… | ||
| Coq to C Translation with Partial Evaluation + Counterexample Generation | Akira Tanaka, Hideto Ueno, John Toman, Naoki Kobayashi, Takeshi Tsukada | 59m |
Builds a verified Coq-to-C code generator that uses a custom codogen plugin and a partial-evaluation pipeline to monomorphize polymorphic/dependent functions… | ||
| Control Flow Obfuscation for Featherweight Java + Efficient Fair Conjunction | Kenny Zhuo Ming Lu, Petr Lozov, Dmitri Boulytchev | 01h 05m |
Two short, concrete results: a mechanical CPS translation to FJ_lambda lifts Featherweight Java (SSA input) into a library of CPS combinators (seq, if-else… | ||
| Program Manipulation of C Code | Julia Lawall | 01h 02m |
A toolchain for scripted source transformations targets large C bases with Coccinelle using its semantic patches language SmPL and metavariables plus the… | ||
| Erasure In Dependently Typed Programming | Matúš Tejiščák | 01h 07m |
Presents an erasure-inference pipeline that numbers binders and applications, emits Horn-clause constraints about retention, solves them for a minimal set of… | ||
| Latent Effects and Handlers + Automatic Differentiation via Effects and Handlers | Casper Bach Poulsen, Cas van der Rest, Tom Schrijvers, Jesse Sigal | 01h 09m |
Two papers show concrete implementations: one adds latent effects to algebraic handlers (Acta implementation) so function abstractions and staging can get… | ||
| A Type-Safe Structure Editor Calculus + Strictly Capturing Non-Strict Closures | Christian Godiksen, Thomas Herrmann, Hans Hüttel, Mikkel Korup Lauridsen, Iman Owliaie, Zachary Sullivan, Paul Downen, Zena M. Ariola | 01h 00m |
Two short papers: one builds a type-safe editor calculus with cursors, holes, breakpoints and a small-step semantics and gives a behavioral type system… | ||
| Hardware DSLs | Pat Hanrahan | 01h 10m |
Claims that domain-specific hardware DSLs let one write a single high-level spec that automatically produces simulator, RTL and SMT verification models and… | ||
| nothing matches | ||