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>
1---2name: popl-topic-selection3description: 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.4---56# POPL Topic Selection78POPL's full name is the routing test: *Principles* of Programming Languages. The9venue's center of gravity is a *general truth about languages* — a semantics, a type10discipline, a program logic, a proof technique — established by definition and11theorem. Both theoretical and experimental papers are welcome under the posted12scope, but an experimental POPL paper still orbits a principle. (Scope wording per13the POPL series pages, read 2026-07-08.)1415## Three questions before committing16171. **What sentence do you most want reviewers to believe?** If it starts "we prove"18 or "we give a semantics/logic/type system such that ..." — POPL. If it starts19 "our compiler/analyzer achieves ..." — PLDI. If it starts "developers using our20 language ..." — OOPSLA.212. **Could a skeptic check the claim without running anything?** POPL's decisive22 evidence is re-derivable: proofs, mechanizations, counterexample-freedom by23 construction. If the truth of your claim lives in measurements, route toward the24 implementation venues.253. **Does the idea outlive your artifact?** POPL rewards machinery others can26 instantiate on their languages. A theorem inseparable from one codebase is a27 tool paper wearing a theorem.2829## Routing table3031| Project signature | Better venue | Reason |32|---|---|---|33| New program logic + soundness proof + small case studies | **POPL** | Principle first, evidence supporting |34| Compiler optimization with 1.4x speedups, proofs optional | PLDI | Benchmark-carried claim, implementor jury |35| Language design evaluated by user study or corpus mining | OOPSLA | Broader empirical evidence culture |36| Typed FP abstraction, elegant library, paradigm-native | ICFP | The functional-programming home crowd |37| Pure model/automata/logic result, thin language connection | LICS / CSL / FSCD | Logic-side siblings want it more |38| Decision procedure, model checker, solver improvement | CAV / TACAS | Verification-algorithm reviewers |39| Proof-engineering technique, assistant infrastructure | CPP / ITP | Mechanization-first audience (CPP co-locates with POPL) |40| Solid but regional-scale PL result, or needs journal length | ESOP / TOPLAS / JFP / LMCS | Right bar, right format |4142All of POPL, PLDI, OOPSLA, and ICFP publish in PACMPL, so the archival venue is43identical — choose by **reviewer community and evidence shape**, never by deadline44proximity.4546## POPL-fit smells, both directions4748- *Good signs:* the abstract states a theorem; the motivating example breaks an49 existing system's metatheory; reviewers from three different PL subareas would50 each recognize the machinery.51- *Warning signs:* the "formal" section restates the implementation in Greek52 letters; the theorem is routine and the contribution is engineering; the paper53 needs performance numbers to matter.5455```text56Fit test (fill honestly):57 Central claim: ..............................................58 Decisive evidence: [ ] proof [ ] mechanization [ ] measurements [ ] study59 Who must believe it: [ ] semanticists [ ] implementors [ ] tool users60 Survives artifact deletion? [ ] yes [ ] no61 => POPL only if column one dominates and the answer is "yes".62```6364## Output format6566```text67[POPL fit] strong / plausible with reframing / route elsewhere68[Central claim] <the one-sentence version>69[Evidence shape] <proof / mechanization / empirical mix>70[Reframe path] <what to foreground if staying at POPL>71[Alternative] <venue + one-line reason, if routing away>72```
brycewang-stanford