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>
Source: brycewang-stanford/Awesome-Journal-Skills → POPL-Skills/skills/popl-topic-selection/SKILL.md
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---567# POPL Topic Selection89POPL's full name is the routing test: *Principles* of Programming Languages. The10venue's center of gravity is a *general truth about languages* — a semantics, a type11discipline, a program logic, a proof technique — established by definition and12theorem. Both theoretical and experimental papers are welcome under the posted13scope, but an experimental POPL paper still orbits a principle. (Scope wording per14the POPL series pages, read 2026-07-08.)1516## Three questions before committing17181. **What sentence do you most want reviewers to believe?** If it starts "we prove"19 or "we give a semantics/logic/type system such that ..." — POPL. If it starts20 "our compiler/analyzer achieves ..." — PLDI. If it starts "developers using our21 language ..." — OOPSLA.222. **Could a skeptic check the claim without running anything?** POPL's decisive23 evidence is re-derivable: proofs, mechanizations, counterexample-freedom by24 construction. If the truth of your claim lives in measurements, route toward the25 implementation venues.263. **Does the idea outlive your artifact?** POPL rewards machinery others can27 instantiate on their languages. A theorem inseparable from one codebase is a28 tool paper wearing a theorem.2930## Routing table3132| Project signature | Better venue | Reason |33|---|---|---|34| New program logic + soundness proof + small case studies | **POPL** | Principle first, evidence supporting |35| Compiler optimization with 1.4x speedups, proofs optional | PLDI | Benchmark-carried claim, implementor jury |36| Language design evaluated by user study or corpus mining | OOPSLA | Broader empirical evidence culture |37| Typed FP abstraction, elegant library, paradigm-native | ICFP | The functional-programming home crowd |38| Pure model/automata/logic result, thin language connection | LICS / CSL / FSCD | Logic-side siblings want it more |39| Decision procedure, model checker, solver improvement | CAV / TACAS | Verification-algorithm reviewers |40| Proof-engineering technique, assistant infrastructure | CPP / ITP | Mechanization-first audience (CPP co-locates with POPL) |41| Solid but regional-scale PL result, or needs journal length | ESOP / TOPLAS / JFP / LMCS | Right bar, right format |4243All of POPL, PLDI, OOPSLA, and ICFP publish in PACMPL, so the archival venue is44identical — choose by **reviewer community and evidence shape**, never by deadline45proximity.4647## POPL-fit smells, both directions4849- *Good signs:* the abstract states a theorem; the motivating example breaks an50 existing system's metatheory; reviewers from three different PL subareas would51 each recognize the machinery.52- *Warning signs:* the "formal" section restates the implementation in Greek53 letters; the theorem is routine and the contribution is engineering; the paper54 needs performance numbers to matter.5556```text57Fit test (fill honestly):58 Central claim: ..............................................59 Decisive evidence: [ ] proof [ ] mechanization [ ] measurements [ ] study60 Who must believe it: [ ] semanticists [ ] implementors [ ] tool users61 Survives artifact deletion? [ ] yes [ ] no62 => POPL only if column one dominates and the answer is "yes".63```6465## Output format6667```text68[POPL fit] strong / plausible with reframing / route elsewhere69[Central claim] <the one-sentence version>70[Evidence shape] <proof / mechanization / empirical mix>71[Reframe path] <what to foreground if staying at POPL>72[Alternative] <venue + one-line reason, if routing away>73```7475---7677**Source:** [`brycewang-stanford/Awesome-Journal-Skills`](https://github.com/brycewang-stanford/Awesome-Journal-Skills) → `POPL-Skills/skills/popl-topic-selection/SKILL.md`
thedixitjain