| name | popl-topic-selection |
| description | Use when deciding whether a project is POPL-shaped — a principle about programming languages carried by definitions and theorems — or better aimed at PLDI's implementation bar, OOPSLA's breadth, ICFP's paradigm focus, or LICS, CAV, CPP, ESOP, and journal outlets, judged by what the decisive evidence is. |
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
- 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.
- 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.
- 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>
