popl-topic-selection

POPL Topic Selection

POPL's full name is the routing test: Principles of Programming Languages. The

venue's center of gravity is a general truth about languages — a semantics, a type

discipline, a program logic, a proof technique — established by definition and

theorem. Both theoretical and experimental papers are welcome under the posted

scope, but an experimental POPL paper still orbits a principle. (Scope wording per

the POPL series pages, read 2026-07-08.)

Three questions before committing

1. What sentence do you most want reviewers to believe? If it starts "we prove"

or "we give a semantics/logic/type system such that ..." — POPL. If it starts

"our compiler/analyzer achieves ..." — PLDI. If it starts "developers using our

language ..." — OOPSLA.

1. Could a skeptic check the claim without running anything? POPL's decisive

evidence is re-derivable: proofs, mechanizations, counterexample-freedom by

construction. If the truth of your claim lives in measurements, route toward the

implementation venues.

1. Does the idea outlive your artifact? POPL rewards machinery others can

instantiate on their languages. A theorem inseparable from one codebase is a

tool paper wearing a theorem.

Routing table

| Project signature | Better venue | Reason |

|---|---|---|

| New program logic + soundness proof + small case studies | POPL | Principle first, evidence supporting |

| Compiler optimization with 1.4x speedups, proofs optional | PLDI | Benchmark-carried claim, implementor jury |

| Language design evaluated by user study or corpus mining | OOPSLA | Broader empirical evidence culture |

| Typed FP abstraction, elegant library, paradigm-native | ICFP | The functional-programming home crowd |

| Pure model/automata/logic result, thin language connection | LICS / CSL / FSCD | Logic-side siblings want it more |

| Decision procedure, model checker, solver improvement | CAV / TACAS | Verification-algorithm reviewers |

| Proof-engineering technique, assistant infrastructure | CPP / ITP | Mechanization-first audience (CPP co-locates with POPL) |

| Solid but regional-scale PL result, or needs journal length | ESOP / TOPLAS / JFP / LMCS | Right bar, right format |

All of POPL, PLDI, OOPSLA, and ICFP publish in PACMPL, so the archival venue is

identical — choose by reviewer community and evidence shape, never by deadline

proximity.

POPL-fit smells, both directions

• Good signs: the abstract states a theorem; the motivating example breaks an

existing system's metatheory; reviewers from three different PL subareas would

each recognize the machinery.

• Warning signs: the "formal" section restates the implementation in Greek

letters; the theorem is routine and the contribution is engineering; the paper

needs performance numbers to matter.

Fit test (fill honestly):
  Central claim: ..............................................
  Decisive evidence:      [ ] proof   [ ] mechanization   [ ] measurements   [ ] study
  Who must believe it:    [ ] semanticists  [ ] implementors  [ ] tool users
  Survives artifact deletion?  [ ] yes  [ ] no
  => POPL only if column one dominates and the answer is "yes".

Output format

[POPL fit] strong / plausible with reframing / route elsewhere
[Central claim] <the one-sentence version>
[Evidence shape] <proof / mechanization / empirical mix>
[Reframe path] <what to foreground if staying at POPL>
[Alternative] <venue + one-line reason, if routing away>